{{interfaces | imports = Interface:Symmetric point | exports = Interface:Midpoint }}
This is part of a series of modules which prove a variety of geometrical theorems starting with Tarski's axioms for geometry. We follow the formalization of Julien Narboux<ref>The formal proofs are at http://www.lix.polytechnique.fr/Labo/Julien.Narboux/tarski.html Formalization of Tarski's geometry in the Coq proof assistant and are described in Julien Narboux (2007), "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8614 Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156</ref> which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.<ref>W. Schwabhäuser, W Szmielew, and A. Tarski (1983), ''Metamathematische Methoden in der Geometrie'', ISBN 0387129588</ref>
This page proves various results involving the midpoint of a line segment. We don't yet prove the existence of a midpoint (that's in the next chapter).
We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:
This is the proposition that equals can be substituted for equals, in the context of is-midpoint-of. It follows directly from the builders for betweenness and line segment congruence.<ref>not in Narboux</ref>
The midpoint of a line segment is unique.<ref>l7_17 in Narboux</ref>
thumb|right To prove it, start with a line segment P P′ which has two midpoints A and B. Our aim is to show that A = B. First construct B′, the symmetric point of B through the point A. Because reflecting through a symmetric point preserves distances, the line segments P B′ and B′ P′ are congruent to P B and B P′.
Applying BetweennessTwoDistanceUniqueness gives us B = B′. And since B B′ is an empty line segment and A is one of its midpoints, then A = B.
To formalize this proof, first we construct the point B′.
Because reflecting about the point A preserves distances, P B ≡ P′ B′.
Similarly, P′ B ≡ P B′.
Because A is between two points which end up being equal (B and B′), we can conclude that A = B.
A point which is equidistant to the two distinct endpoints of a line segment, and on the same line as them, is the midpoint of that line segment. In symbols, collinear A M B ∧ M A ≡ M B → A = B ∨ M is-midpoint-of A B.<ref>l7_20 in Narboux</ref>
There are three cases based on collinear A M B. The first is between A M B which trivially satisfies the definition of midpoint.
The second case is between M B A. Because B and A are the same distance from M, they must be the same point. To formalize this, apply inner three segment to between M B A and between M B B, which produces B A ≡ B B.
The third case is between B A M. Because A and B can be interchanged, it can be proven from the between M B A case.
Combining the cases finishes the proof.
220px|The proof constructs P′ and shows that P = P′ Given a "parallelogram" (that is, a quadrilateral with opposite sides congruent; we haven't yet developed any theory of parallel lines), the diagonals bisect each other.
First we construct a point p′ which is like P but as far from D as P is from B. That is, B D P ≅ D B P′
The point P′ is on the line B D. The proof is by CollinearityDegenerateTriangle, which in this case is collinear B D P ∧ B D P ≅ D B P′ → collinear D B P′.
We're ready for P = P′. The proof is by LineIntersection, which in this case expands to ¬ collinear A C B ∧ B ≠ D ∧ collinear A C P ∧ collinear A C P′ ∧ collinear B D P ∧ collinear B D P′ → P = P′.
Now that we have P = P′ we are mostly there. The next step is showing P is-midpoint-of A C
The proof of P is-midpoint-of B D is similar.
Now we are ready to combine this with the construction of P′ to produce our result.
thumb|right This one may be hard to describe in a single sentence. The theorem is that given the configuration shown in the diagram, the point C is on the line segment connecting the midpoints M1 and M2. In symbols, between A1 C A2 ∧ between B1 C B2 ∧ C A1 ≡ C B1 ∧ C A2 ≡ C B2 ∧ M1 is-midpoint-of A1 B1 ∧ M2 is-midpoint-of A2 B2 → between M1 C M2{{{.<ref>l7_22 in Narboux</ref> The proof starts by assuming, without loss of generality, that {{{C A1 ≤ C A2.<ref>l7_22_aux in Narboux</ref>
For now, we omit the (lengthy) proof here, as we don't yet need it.
If there is a point equidistant from the endpoints of a line segment, there exists a midpoint of the line segment. In symbols, C A ≡ C B → ∃ x x is-midpoint-of A B{{{. <ref>l7_25 in Narboux</ref> In a future chapter, we will be able to remove the hypothesis and just prove that the midpoint always exists, but this result is one of the steps on the way towards that proof. First, we take care of a trivial case, in which {{{A, B, and C are collinear. This case has two cases, the first of which is A = B.
The other collinear case is C is-midpoint-of A B, which is even simpler (C is the desired midpoint).
Now we are ready for the collinear case itself.
construction of {{{P}}}, {{{Q}}}, {{{R}}}, and {{{X}}} We have already handled the case in which A, B, and C are collinear, so assume they are non-collinear for the rest of the proof. Next extend line segment C A to a distinct point P and extend line segment C B{{{ by the same distance to a point {{{Q. Let R be the intersection of A Q and B P. Then let X be the intersection of A B and C R.
Our plan is to show that X is the midpoint of A B. To do so, we'll prove A R ≡ B R, so EquidistantLine will give us A X ≡ B X.
We first construct P and Q.
P B ≡ Q A The next step is showing that P B ≡ Q A. This by outer five segment on baselines C A P and C B Q and points B and A.
Now we construct a point r′ which is at a point along the line segment A Q corresponding to where R is along B P. We'll be trying to show that r′{{{ in fact equals {{{R, but first we need to construct it.
We next prove R A ≡ R′ B via inner five segment with baselines B R P and A R′ Q and points A and B.
Because we will re-use the same baselines a little later, it is convenient to move the portion of the proof regarding the baselines into a lemma.
Next we apply inner five segment with baselines B R P and A R′ Q and points Q and P to give Q R ≡ P R′.
Proving collinear B R′ P gets us close to R = R′ The last two congruences gives us what we need for A R Q ≅ B R′ P, which in turn implies collinear B R′ P{{{. Looking at the diagram it should be clear that {{{R′ has little hope of remaining different from R, although we are still a few steps from proving that R = R′.
We're getting closer to proving R = R′ via LineIntersection (which says that the intersection of two lines is unique, if we rule out some degenerate cases). Next we need B ≠ P.
The last thing we need to be ready to apply LineIntersection is ¬ collinear A Q B. We will show collinear A Q B → collinear A B C by CollinearityOuterTransitivity on B Q C and B Q A. Here our proof seems to be streamlined from Narboux's, which applies CollinearityOuterTransitivity four times, not just one (TODO: re-check this statement when we're done with MidpointExistsGivenEquidistant).
The first part is B ≠ Q.
It is now time for R = R′.
Now that we have R = R′ we are in the home stretch. A R ≡ R B is next.
since {{{C}}} and {{{R}}} are equidistant from {{{A}}} and {{{B}}}, so is {{{X}}} We're almost ready to apply EquidistantLine. We still need C ≠ R, though. If C were equal to R, then between R X C would imply that C = X, and between A X B would imply collinear A B C, which is a contradiction.
We're now ready to conclude X is-midpoint-of A B.
A bit of logic finishes the proof.
We now export to Interface:Midpoint.
Also, we export to Interface:Basic geometry since it hasn't yet been updated for anything after this point.
<references/>
{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)