# Out lines

Used interfaces |
---|

Imports |

Interface:Line segment inequality |

Exports |

Interface:Out lines |

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^{[1]} which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.^{[2]}

This page gets its name from *out lines*, that is a predicate `(P is-outside A B)`

which means that `P`

is on the line `A B`

outside the segment `A B`

. We prove a number of results based on that concept, which in turn lead to a number of theorems involving collinearity.

We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:

import (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())

import (START Interface:Line_segment_inequality (CLASSICAL FIRSTORDER) () Unable to import parameter START(Interface:Line_segment_inequality)[CLASSICAL(Interface:Classical_propositional_calculus)[]+, FIRSTORDER(Interface:First-order_logic_with_quantifiability)[CLASSICAL(Interface:Classical_propositional_calculus)[]+]+]+: Unable to load module Interface:Line_segment_inequality

## Contents

## Out lines defined[edit]

A point `P`

is on the line `A B`

outside the line segment `A B`

if and only if one of those points is between `P`

and the other and `P`

is not equal to either one.^{[3]}

We also state this definition as a theorem.

### Relating out lines to existence of a point beyond the outside point[edit]

This section (and the next one) have to do with relating `P is-outside A B`

to a point `C`

for which `between A P C`

and `between B P C`

. The first result says that if `between A P C`

, then `between B P C`

is equivalent to `P is-outside A B`

.^{[4]}

We first tackle the `between B P C → P is-outside A B`

case. This is a straightforward application of `BetweennessMiddleConnectivity`

, which in this case says basically that `between A P C`

and `between B P C`

imply `between A B P ∨ between B A P`

.

The first two parts of the `P is-outside A B`

definition are the inequalities `A ≠ P`

and `B ≠ P`

which we just carry over from the antecedent.

To apply `BetweennessMiddleConnectivity`

, we first need `C ≠ P`

.

Next we need `between C P A`

.

The last thing we will need for `BetweennessMiddleConnectivity`

is `between C P B`

.

Now we apply connectivity to get `between P A B ∨ between P B A`

, which is the only remaining part of the definition of `is-outside`

.

In the other direction, `P is-outside A B`

tells us that either `between P A B`

or `between P B A`

. In the either case, we can apply transitivity with `between A P C`

to get `between B P C`

.

We'll arrange this proof by first rearranging the disjunction and conjunctions, before we worry about transitivity.

First we pick out `A ≠ P ∧ between A P C`

.

Next we take `P is-outside A B`

, unfold the definition, and extract `between P A B ∨ between P B A`

.

Applying distributivity of conjunction over disjunction finishes the job.

Our first transitivity invocation is `between B A P ∧ between A P C ∧ A ≠ P → between B P C`

.

Our second transitivity invocation is `between A B P ∧ between A P C → B P C`

Now we combine the two.

### The existence of a point beyond the outside point[edit]

In this section we show that a point is outside a line segment if and only if there exists a point beyond the outside point. In symbols, `P is-outside A B`

is equivalent to `A ≠ P ∧ B ≠ P ∧ ∃ c (C ≠ P ∧ between A P C ∧ between B P C)`

.

We start with the forward implication. Extend `A P`

to a distinct point `c`

(that is, a point for which `P ≠ c ∧ between A P c`

. We can then apply `BeyondOut`

to show that `between B P c`

.^{[5]} Below we present the formal version of this proof, broken down into several lemmas.

At the end of the proof we'll need a copy of `P is-outside A B`

, so we stick it on the proof stack.

Most of the proof of this lemma consists of an application of `BeyondOut`

. The first thing we need is `A ≠ P`

.

Next is `B ≠ P`

Next is `C ≠ P`

Last is `between A P C`

.

Applying `BeyondOut`

gives us `between B P C ↔ P is-outside A B`

Now we detach the `P is-outside A B`

part so we just have `between B P C`

.

The next lemma is just `PointConstructionDifferent`

, together with some rearrangements via commutativity and symmetry.

We now have `P is-outside A B → ∀ c (c ≠ P ∧ between A P c → between B P c)`

. Combining this with the previous result gives `P is-outside A B → ∃ c (c ≠ P ∧ between A P c ∧ (c ≠ P ∧ between A P c → between B P c))`

.

To get `between B P c`

is just a matter of modus ponens. The one complication is that we want to keep `c ≠ P ∧ between A P c`

around in addition, so we apply idempotence, associativity, and modus ponens, in that order.

First is `P is-outside A B → A ≠ P`

Next is `P is-outside A B → B ≠ P`

Next is the remainder.

We now turn to the reverse direction.^{[6]}

This proof is basically an application of middle connectivity for betweenness, which in this case is `c ≠ P ∧ between c P A ∧ between c P B → between P A B ∨ between P B A`

. First we need `c ≠ P`

Next is `between c P A`

.

Next is `between c P B`

.

We apply connectivity, remove the quantifier from the consequent, and assemble the result.

### Alternate definition in terms of collinearity[edit]

A point is outside a line segment if and only if it is collinear with the endpoints of the segment but not between them. That is, `P is-outside A B ↔ collinear A P B ∧ ¬ between A P B`

.

We first tackle the forward direction.^{[7]} The first lemma is `P ≠ A ∧ P ≠ B ∧ between P A B → ¬ between A P B`

.

First we pick out and rearrange the parts we need, specifically we prove `P ≠ A ∧ P ≠ B ∧ between P A B → between P A B ∧ P ≠ A`

The geometrical content of this proof is `between P A B ∧ between A P B → A = P`

.

Applying some propositional logic, we rearrange this to `between P A B ∧ A ≠ P → ¬ between A P B`

Combining this with our first rearrangement, we get the desired result.

The second lemma, `A ≠ P ∧ B ≠ P ∧ between P B A → ¬ between A P B`

, is very similar.

Combining the two previous lemmas we get `P is-outside A B → ¬ between A P B`

.

Collinearity is straightforward.

Combining the last two results gives the forward direction.

Turning our attention to the reverse direction,^{[8]} we have two tasks. The first is to show that `P ≠ A`

and P ≠ B, each of which follows from `¬ between A P B`

(because either equality holding would make `between A P B`

hold trivially).

Next we show `A = P → (between A P B ↔ between P P B)`

, and from it `A = P → between A P B`

.

Proving `B = P → between A P B`

is similar (via `B = P → (between A P B ↔ between A P P)`

.

Our other task is to show `between P A B ∨ between P B A`

.

First we show `collinear A P B ∧ ¬ between A P B → between P B A ∨ between P A B`

That gives us `between P B A ∨ between B A P`

. We just need to rearrange a bit and we are done.

Combining our tasks proves the reverse direction, and combining forward and reverse directions proves the equivalence.

## Reflexive, symmetric, and transitive[edit]

Here we present versions of reflexivity, symmetry, and transitivity. You can think of this as dividing a line (excluding the point `P`

itself) into two equivalence classes: those to the left of `P`

and those to the right (we certainly don't have the machinery to say it quite that way, but that is the rough idea).

### Reflexivity[edit]

### Symmetry[edit]

### Transitivity[edit]

Expanding the definitions of the antecedent, we start with

A ≠ P ∧ B ≠ P ∧ (between P A B ∨ between P B A) ∧ B ≠ P ∧ C ≠ P ∧ (between P B C ∨ between P C B)

Looking at the betweenness part of that, there are four cases (`between P A B ∧ between P B C`

being the first, `between P A B ∧ between P C B`

, being the second, and so on).

The interesting part is a lemma which handles those four cases; there is also a fair bit of rearranging (in the lemma and in the proof of the actual theorem).

First we break down the four cases.

Now we distribute the `B ≠ P`

into each of the cases.

The first case is `B ≠ P ∧ between P A B ∧ between P B C`

. In all four cases we are showing that the case in question implies `between P A C ∨ between P C A`

. In the current case, `between P A C`

follows from transitivity.

The second case is `B ≠ P ∧ between P A B ∧ between P C B`

. Here we apply inner connectivity for betweenness.

The third case is `B ≠ P ∧ between P B A ∧ between P B C`

. Here we apply outer connectivity for betweenness.

The fourth case is `B ≠ P ∧ between P B A ∧ between P C B`

. In this one `between P C A`

follows from betweenness transitivity.

First we pick out `A ≠ P`

.

Secondly we pick out `C ≠ P`

.

Next we assemble `B ≠ P ∧ ((between P A B ∨ between P B A) ∧ (between P B C ∨ between P C B))`

and apply our lemma to turn this into `between P A C ∨ between P C A`

.

## Line segment construction[edit]

From a given point, in the direction of a second given point, we construct a segment congruent to a given line segment. This is similar to `InnerSegmentConstruction`

but is expressed in terms of `is-outside`

.

### Existence[edit]

In this section we prove the existence of such a point. That is, `R ≠ A ∧ B ≠ C → ∃ e (A is-outside e R ∧ A e ≡ B C)`

.

The proof consists of applying `InnerSegmentConstruction`

, rearranging, and applying the definition of `is-outside`

. The following lemma expresses most of the rearrangements.^{[9]}

To apply the definition of `A is-outside E R`

, first we need `E ≠ A`

. This follows from `B ≠ C`

and `A E ≡ B C`

, and the first step is picking out those two formulas.

The next step in getting to `E ≠ A`

is to show that `B ≠ C ∧ A E ≡ B C → A ≠ E`

.

Combining that with the previous result and flipping the two sides of the not-equals sign gives us `E ≠ A`

.

Next we need `R ≠ A`

.

Then we need `between A E R ∨ between A R E`

That's all for `A is-outside E R`

. So the only remaining step is `A E ≡ B C`

### Uniqueness[edit]

The point that we construct this way is also unique. In symbols, `R ≠ A ∧ B ≠ C ∧ A is-outside X R ∧ A X ≡ B C ∧ A is-outside Y R ∧ A Y ≡ B C → X = Y`

.^{[10]}

The proof of uniqueness is more involved than the existence proof. Start by expanding the definitions of `is-outside`

(and removing the redundant copies of `R ≠ A`

) so we now have

R ≠ A ∧ B ≠ C ∧ X ≠ A ∧ (between A X R ∨ between A R X) ∧ A X ≡ B C ∧ Y ≠ A ∧ (between A Y R ∨ between A R Y) ∧ A Y ≡ B C

By congruence transitivity, we derive `A X ≡ A Y`

. Then we look at the betweenness relationships. Specifically we want to conclude `between A X Y ∨ between A Y X`

. There are four cases: `between A X R ∧ between A Y R → between A X Y ∨ between A Y X`

by inner connectivity, `between A X R ∧ between A R Y → between A X Y`

by transitivity, `between A R X ∧ between A Y R → between A Y X`

by transitivity, and `A ≠ R ∧ between A R X ∧ between A R Y → between A X Y ∨ between A Y X`

by outer connectivity.

Once we have `A X ≡ A Y`

and `between A X Y ∨ between A Y X`

, `X = Y`

follows from `BetweennessOneDistanceUniqueness`

(applied twice, once to each of the betweenness formulas).

Our first lemma just spells out the four cases.

First is `A ≠ R`

.

Next is `between A X R ∨ between A R X`

Next is `between A Y R ∨ between A R Y`

Now we apply distributivity to expand the four cases.

Now we distribute the `A ≠ R`

into each of the cases.

Now we remove `A ≠ R`

from the first three cases, and apply associativity to the fourth.

The first of the four cases is `between A X R ∧ between A Y R`

.

The second case is `between A X R ∧ between A R Y`

.

The third case is `between A R X ∧ between A Y R`

.

The fourth case is `A ≠ R ∧ between A R X ∧ between A R Y`

.

We first arrange the results of the two previous lemmas to get `(between A X Y ∧ A X ≡ A Y) ∨ (between A Y X ∧ A X ≡ A Y)`

.

The result for the first half is `between A X Y ∧ A X ≡ A Y → X = Y`

, which follows directly from `BetweennessOneDistanceUniqueness`

.

The second half result, `between A Y X ∧ A X ≡ A Y → X = Y`

, is basically the same thing, but we need to rearrange slightly.

Now we combine the two halves.

## The closer point is between[edit]

If `A`

and `B`

are on a line with `P`

, both on the same side of `P`

, and `A`

is closer to `P`

than `B`

is, then `A`

is between `P`

and `B`

. That is, `P is-outside A B ∧ P A ≤ P B → between P A B`

.^{[11]}

The proof begins by expanding `P A ≤ P B`

to `∃ y (between P y B ∧ P A ≡ P y)`

. From `P is-outside A B`

and `P A ≡ P y`

we can conclude `P ≠ y`

. We will then be applying `OutSegmentConstructionUniqueness`

which in this case expands to:

B ≠ P ∧ P ≠ y ∧ P is-outside y B ∧ P y ≡ P y ∧ P is-outside A B ∧ P A ≡ P y → y = A

Each piece of this is something we already have, or readily follows from things we have. Once we have `y = A`

we just substitute it into `between P y B`

and we are done.

The first lemma constructs the point `y`

.

The next lemma is `P ≠ y`

First we pick out `P ≠ A`

.

Next is `P A ≡ P Y`

.

Next is `P = Y ∧ P A ≡ P Y → P = A`

(from `CongruenceIdentityFromEquality`

), which we then rearrange to give `P ≠ A ∧ P A ≡ P Y → P ≠ Y`

Combining that with the previous result finishes the proof.

The next lemma is `P is-outside Y B`

.

First we need `Y ≠ P`

.

Then we need `B ≠ P`

.

Finally we need `between P Y B ∨ between P B Y`

.

The next lemma applies `OutSegmentConstructionUniqueness`

to give `Y = A`

.

First we need `B ≠ P`

.

Next we need `P ≠ Y`

.

Next we need `P is-outside Y B`

.

Next is `P Y ≡ P Y`

.

Next is `P is-outside A B`

.

Next is `P A ≡ P Y`

.

Now that we have all the hypotheses, we'll apply `OutSegmentConstructionUniqueness`

to give `Y = A`

.

Now that we have `Y = A`

, we just substitute that into `between P Y B`

to get `between P A B`

.

First we get out `Y = A`

and `between P Y B`

.

The substitution is `Y = A → (between P Y B ↔ between P A B)`

.

### The point which is between is closer[edit]

The converse also holds: `P is-outside A B ∧ between P A B → P A ≤ P B`

.^{[12]} To prove `P A ≤ P B`

, we need `∃ c (between P c B ∧ P A ≡ P c)`

, and the point `A`

suffices for the choice of `c`

. In fact, we don't need the hypothesis `P is-outside A B`

, so unlike Narboux we state the theorem without it.

Now we apply a substitution `c = A → (between P c B ∧ P A ≡ P c ↔ between P A B ∧ P A ≡ P A)`

to turn `between P A B ∧ P A ≡ P A`

into `[ A / c ] (between P c B ∧ P A ≡ P c)`

.

Turning the substitution into ∃ and applying `LessEqualCutoff`

we are done.

### Biconditional[edit]

Here we combine the previous two results: `P is-outside A B → (P A ≤ P B ↔ between P A B)`

.

## Collinearity[edit]

In this section we prove a number of results involving collinearity.

### Outer transitivity[edit]

Here we prove `P ≠ Q ∧ collinear P Q A ∧ collinear P Q B → collinear P A B`

.^{[13]} We call it "outer" transitivity although unlike similar-looking results for betweenness, five segment, etc, this does not make it a different theorem than inner transitivity, just a different rearrangement (since the order of points in a collinearity predicate does not matter).

Actually, we first prove it in the slightly rearranged form `P ≠ Q ∧ collinear S P Q ∧ collinear X P Q → collinear X P S`

(in which `P`

and `Q`

are interchanged and the order of the points in the collinearity statements are changed). There is no deep reason for this rearrangement, but it will be slightly more convenient in the next section.

Expanding each `collinear`

in the antecedent by the definition, and then applying associativity, gives us nine cases. In each case we'll be able to prove `between X P S`

, `between P X S`

, `between P S X`

, or a disjunction between two of them. Each case will follow from either betweenness transitivity or betweenness connectivity.

We start with a lemma, and then proceed to the proof.

We prove `collinear X P S`

via its definition: `between X P S ∨ between P S X ∨ between S X P`

.

First we associate the two collinearity formulas together.

Now we apply distributivity multiple times to separate out the nine cases. Round one: splitting `collinear S P Q`

halfway.

Round two: splitting `collinear S P Q`

the rest of the way.

Round three: split `collinear X P Q`

halfway.

Round four: split `collinear X P Q`

the rest of the way.

Having split out the nine cases, we combine with `P ≠ Q`

and then distribute `P ≠ Q`

into each of the cases.

Round one.

Round two.

Round three.

Round four.

Sorry breaking out the cases took so long. Anyway, we are ready to tackle them one by one. The first is `between S P Q ∧ between X P Q`

(of course, all of them have `P ≠ Q`

tacked on the front, which we usually will not state explicitly). It follows from the following application of `BetweennessMiddleConnectivity`

: `Q ≠ P ∧ between Q P S ∧ between Q P X → between P S X ∨ between P X S`

To finish the first case we turn `between P S X ∨ between P X S`

into `collinear X P S`

.

The second case is `between S P Q ∧ between P Q X`

. This follows from `between S P Q ∧ between P Q X ∧ P ≠ Q → between S P X`

, which is an instance of `BetweennessOuterTransitivity`

.

Now we need `between S P X → collinear X P S`

.

The third case is `between S P Q ∧ between Q X P`

, which follows from `between S P Q ∧ between P X Q → between S P X`

, which is an instance of `BetweennessInnerTransitivity`

To finish this case we need `between S P X → collinear X P S`

.

We now start the second set of cases, those starting with `between P Q S`

. The fourth case is `between P Q S ∧ between X P Q`

, which follows from `between X P Q ∧ between P Q S ∧ P ≠ Q → between X P S`

, which is an instance of `BetweennessOuterTransitivity`

.

To finish this case we need `between X P S → collinear X P S`

.

The fifth case is `between P Q S ∧ between P Q X`

. This follows from `BetweennessOuterConnectivity`

, which in this case is `P ≠ Q ∧ between P Q S ∧ between P Q X → between P S X ∨ between P X S`

.

To finish this case we turn `between P S X ∨ between P X S`

into `collinear X P S`

.

The sixth case is `between P Q S ∧ between Q X P`

. It follows from `between P X Q ∧ between P Q S → between P X S`

, an instance of `BetweennessMiddleTransitivityFlipped`

To finish the case we turn `between P X S`

into `collinear X P S`

.

We are ready for the last trio of cases, those which start with `between Q S P`

. The seventh case is `between Q S P ∧ between X P Q`

. It follows from `between X P Q ∧ between P S Q → between X P S`

, which is an instance of `BetweennessInnerTransitivity`

.

To finish the case we turn `between X P S`

into `collinear X P S`

.

The eighth case is `between Q S P ∧ between P Q X`

. It follows by `between P S Q ∧ between P Q X → between P S X`

which is an instance of `BetweennessMiddleTransitivityFlipped`

.

To finish the case we need to turn `between P S X`

into `collinear X P S`

.

The ninth and final case is `between Q S P ∧ between Q X P`

. It follows from `between P S Q ∧ between P X Q → between P S X ∨ between P X S`

, which is an instance of `BetweennessInnerConnectivity`

.

To finish this case, we turn `between P S X ∨ between P X S`

into `collinear X P S`

.

To finish the proof, we simply combine the breaking down of the cases with the resolution of each case.

Now we return to `P ≠ Q ∧ collinear P Q A ∧ collinear P Q B → collinear P A B`

.

First we need `P ≠ Q`

Second we need `collinear A P Q`

.

Lastly we need `collinear B P Q`

.

Applying the previous rearrangement of transitivity gives us `collinear B P A`

, which we then rearrange to `collinear P A B`

.

### Being collinear to collinear points[edit]

Given three collinear distinct points, a fourth point being collinear to two of them is equivalent to being collinear to two others. More precisely, `P ≠ Q ∧ S ≠ P ∧ collinear S P Q → (collinear X P Q ↔ collinear X P S)`

.

The forward direction is `P ≠ Q ∧ S ≠ P ∧ collinear S P Q ∧ collinear X P Q → collinear X P S`

.^{[14]} It is almost identical to what we proved in the previous section (we just need to drop the `S ≠ P`

).

The reverse direction is `P ≠ Q ∧ S ≠ P ∧ collinear S P Q ∧ collinear X P S → collinear X P Q`

.^{[15]} This is essentially the same as the forward direction, as exchanging `S`

and `Q`

doesn't really change the statement. Narboux proves the reverse direction by copy-pasting the proof of the forward direction, interchanging `S`

and `Q`

, but our proof simply performs the right rearrangements to apply the forward direction.

We first need `P ≠ S`

.

Next is `Q ≠ P`

.

Next is `collinear Q P S`

.

Last is `collinear X P S`

.

Applying the forward theorem, with `S`

and `Q`

interchanged, finishes the job.

We combine the two previous results to get `P ≠ Q ∧ S ≠ P ∧ collinear S P Q → (collinear X P Q ↔ collinear X P S)`

### Inner transitivity[edit]

Here we prove `P ≠ Q ∧ collinear P Q A ∧ collinear P Q B → collinear Q A B`

.^{[16]} As we said before, the mathematical meaning of the theorem is not different from the "outer" collinearity transitivity; it is merely a rearrangement.

We will be applying collinearity outer transitivity. First we need `Q ≠ P`

.

Next is `collinear Q P A`

.

Last is `collinear Q P B`

.

## The intersection of two lines[edit]

If two distinct, non-degenerate lines intersect, they intersect in a single point. At least for this theorem, we consider a line `A B`

and line `C D`

to be distinct and non-degenerate if `¬ collinear A B C ∧ C ≠ D`

. The statement of the whole theorem is `¬ collinear A B C ∧ C ≠ D ∧ collinear A B P ∧ collinear A B Q ∧ collinear C D P ∧ collinear C D Q → P = Q`

.^{[17]}

The proof consists of multiple applications of collinearity transitivity, together with some cases and a proof by contradiction. It starts with `collinear C P Q`

(by collinearity transitivity).

`C ≠ D`

:

`collinear C D P`

:

`collinear C D Q`

:

Then note that `A ≠ B`

(as a consequence of `¬ collinear A B C`

), and collinearity transitivity gives us `collinear A P Q`

and `collinear B P Q`

.

We pick out `¬ collinear A B C`

, which we will need shortly.

The next step is to note `collinear A A C`

and apply a substitution to turn it into `A = B → collinear A B C`

.

Now we just transpose and combine with `¬ collinear A B C`

.

`A ≠ B`

:

`collinear A B P`

:

`collinear A B Q`

:

We now assume `P ≠ Q`

and will show `collinear A B C`

, which is a contradiction. The first thing we get from `P ≠ Q`

is `collinear A C Q`

(from `collinear A P Q`

and `collinear C P Q`

).

`P ≠ Q`

:

`collinear P Q A`

:

`collinear P Q C`

:

Transitivity produces `collinear Q A C`

, which we then rearrange to `collinear A C Q`

.

In a similar way we prove `collinear A B Q`

.

`P ≠ Q`

:

`collinear P Q A`

:

`collinear P Q B`

:

Transitivity produces `collinear Q A B`

, which we then rearrange to `collinear A B Q`

.

Now we consider two cases: `Q = A`

and `Q ≠ A`

.

For the `Q = A`

case, first apply collinearity transitivity to `collinear C P Q`

and `collinear B P Q`

to get `collinear C B Q`

, which turns into our desired contradiction `collinear A B C`

by substituting `A`

for `Q`

.

`P ≠ Q`

:

`collinear P Q B`

:

`collinear P Q C`

:

Applying transitivity yields `collinear Q B C`

, which we then turn into `collinear A B C`

via a subsitution.

The `Q ≠ A`

case lets us apply transitivity to `collinear A C Q`

and `collinear A B Q`

to get `collinear A B C`

, which is our desired contradiction.

`Q ≠ A`

:

`collinear Q A B`

:

`collinear Q A C`

:

Next we combine the cases.

Here we point out the contradiction.

Since assuming `P ≠ Q`

produced a contradiction, we can conclude that `P = Q`

.

## The existence of a point not on a given line[edit]

Given a line, there is a point which is not on that line. Formally, `A ≠ B → ∃ c ¬ collinear A B c`

.^{[18]}

The proof, not surprisingly, is based on `LowerDimension`

, which gives us three non-collinear points x, y, and z. If any one of them is not on the line (that is, `¬ collinear A B x`

or likewise for y or z), we are done. But if they are all collinear with `A`

and `B`

, we can conclude `collinear x y z`

by transitivity, which is a contradiction.

We start by restating `LowerDimension`

in terms of collinearity.

The next lemma says that if we have a point not collinear with `A`

and `B`

, we are done.

We're ready to start working on getting `collinear x y z`

by transitivity. There are two cases: `A = X`

and `A ≠ X`

. The `A = X`

case is the easier one: we first conclude `collinear A Y Z`

and then substitute `X`

for `A`

.

`A ≠ B`

:

`collinear A B Y`

:

`collinear A B Z`

:

Applying transitivity gives `collinear A Y Z`

,

and applying a substitution turns that into `collinear X Y Z`

.

The `A ≠ X`

case involves first proving `collinear A X Y`

and `collinear A X Z`

(each by transitivity), and applying transitivity again, to get `collinear X Y Z`

.

We start with `A ≠ X`

.

To prove `collinear A X Y`

, we first need `A ≠ B`

:

`collinear A B X`

:

`collinear A B Y`

:

That's all we need for `collinear A X Y`

Now we need `collinear A X Z`

, and the first antecedent is `A ≠ B`

.

`collinear A B X`

:

`collinear A B Z`

:

Applying transitivity we get `collinear A X Z`

We are now ready to apply transitivity to `A ≠ X`

, `collinear A X Y`

, and `collinear A X Z`

to get `collinear X Y Z`

.

We now combine the `A = X`

and `A ≠ X`

cases and rearrange a bit.

The next lemma gets rid of `collinear A B X`

(because the case `¬ collinear A B X`

is taken care of by `PointNotOnLineLemma`

).

First, the `collinear A B X`

case:

Second, the `¬ collinear A B X`

case:

Now we just need to combine the cases.

In a very similar manner we get rid of `collinear A B Y`

.

First, the `collinear A B Y`

case:

Second, the `¬ collinear A B Y`

case:

Now we just need to combine the cases.

At this point we are very close. The only thing remaining in the antecedent that we need to get rid of is `¬ collinear X Y Z`

. But `X`

, `Y`

, and `Z`

no longer appear anywhere else in the formula. So we can quantify at will, specifically to turn `¬ collinear X Y Z`

into `∃ x ∃ y ∃ z ¬ collinear x y z`

, which we can then detach as it is a theorem.

First we put the theorem on the proof stack.

Now we show we can move the quantifiers to the start: `A ≠ B ∧ ∃ x ∃ y ∃ z ¬ collinear x y z → ∃ x ∃ y ∃ z (A ≠ B ∧ ¬ collinear x y z)`

Now we can introduce the previous theorem and then add the quantifiers.

Detaching the theorem finishes the proof.

## Intersecting lines and congruences[edit]

Given two intersecting line segments, where the portions of each segment on the sides of the intersection are congruent, the segments drawn from the endpoints of one line segment to the endpoints of the other are congruent. That is, `between A B C ∧ between D B E ∧ A B ≡ D B ∧ B C ≡ B E → A E ≡ C D`

.^{[19]}

We consider `A = B`

and `A ≠ B`

cases. The `A = B`

case is easy: `A = B`

implies `D = B`

and substituting into `B C ≡ B E`

gives us `A E ≡ C D`

.

The `A ≠ B`

case follows from outer five segment, using baselines `A B C`

and `D B E`

and points `D`

and `A`

.

Starting on the `A = B`

case, the first step is proving `D = B`

.

To apply `CongruenceIdentityFromEquality`

, we first need `A = B`

.

Secondly, we need `A B ≡ D B`

.

That lets us conclude `D = B`

.

We'll need `B C ≡ B E`

a bit later, so we put it on the proof stack.

The next step is the substitution. The substitution will be `D = B ∧ A = B → (D C ≡ A E ↔ B C ≡ B E)`

, so we start with `D = B ∧ A = B`

.

Here is `D = B ∧ A = B → (D C ≡ A E ↔ B C ≡ B E)`

, as promised.

Pulling `B C ≡ B E`

off the proof stack and combining, we get `D C ≡ A E`

.

Now we just rearrange that congruence to `A E ≡ C D`

.

Now we are ready for the `A ≠ B`

case, in which we apply outer five segment using baselines `A B C`

and `D B E`

and points `D`

and `A`

.

First we need `A ≠ B`

.

We need two betweenness relationships, the first of which is `between A B C`

.

The other is `between D B E`

.

There are two congruences for the baseline, `A B ≡ D B`

,

and `B C ≡ B E`

.

The off-baseline congruences are `A D ≡ D A`

,

and `B D ≡ B A`

.

Applying five segment gives us `C D ≡ E A`

, which we then rearrange to `A E ≡ C D`

.

## Export[edit]

We now export to Interface:Out lines.

## References[edit]

- ↑ The formal proofs are at Formalization of Tarski's geometry in the Coq proof assistant and are described in Julien Narboux (2007), "Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156
- ↑ W. Schwabhäuser, W Szmielew, and A. Tarski (1983),
*Metamathematische Methoden in der Geometrie*, ISBN 0387129588 - ↑ Definition out in Narboux
- ↑ l6_2 in Narboux
- ↑ l6_3_1 in Narboux
- ↑ l6_3_2 in Narboux
- ↑ l6_4_1 in Narboux
- ↑ l6_4_2 in Narboux
- ↑ l6_11_existence in Narboux
- ↑ l6_11_unicity in Narboux
- ↑ l6_13_1 in Narboux
- ↑ l6_13_2 in Narboux
- ↑ col_transitivity_1 in Narboux
- ↑ l6_16_1 in Narboux
- ↑ l6_16_2 in Narboux
- ↑ col_transitivity_2 in Narboux
- ↑ l6_21 in Narboux
- ↑ l6_25 in Narboux
- ↑ Theorem t2_8 in Narboux

- Tarski, Alfred; Givant, Steven (1999), "Tarski's system of geometry", The Bulletin of Symbolic Logic 5 (2): 175–214, doi:10.2307/421089, MR1791303, ISSN 1079-8986