Main derivation
S01 · definition
Before
\text{three points }A,B,C\text{ of the model}After
\triangle ABC=[A,B]\cup[B,C]\cup[C,A]\ \text{when}\ A,B,C\ \text{are distinct and noncollinear}Conditions: none
Rule: mko_triangle_def · Uses: G1, G2, mko_model_dependence
Leaf basis: mko_triangle_def + mko_model_dependence
The MKO's definition has two hypotheses: the three points are distinct, and they are not collinear; under both, the union of the three segments is the nondegenerate triangle ABC. The precise meaning of lines, segments and collinearity depends on the chosen model, so the coordinate model of ℝ² (G1, G2) is fixed first. The rest of the work checks the two hypotheses one at a time and then writes out the union.
S02 · implies
Before
A=(0,0),\ B=(4,0),\ C=(1,3)
After
A\neq B,\ B\neq C,\ C\neq A
Conditions: none
Rule: cartesian_product_def · Uses: G3, cartesian_product_def
Leaf basis: cartesian_product_def + numeric_evaluation
Ordered pairs are equal only if both coordinates agree. The first coordinates of A and B are 0≠4, of B and C are 4≠1, and of C and A are 1≠0, so the three points are pairwise distinct. This is the MKO's first hypothesis, and it also supplies A≠B, which G1 needs for L(A,B) to be defined.
S03 · equivalent
Before
L(A,B)=\{A+t(B-A)\mid t\in\mathbb{R}\}After
L(A,B)=\{(4t,\,0)\mid t\in\mathbb{R}\}Conditions: A\neq B
Rule: coord_ops · Uses: G1, G3, S02
Leaf basis: coord_ops + mul_zero + add_zero
Compute coordinatewise: B−A=(4−0, 0−0)=(4,0), so A+t(B−A)=(0+4t, 0+0·t)=(4t,0). For every t the two expressions are the same point, so the two sets are equal. The condition A≠B was checked in S02.
S04 · equivalent
Before
C\in L(A,B)
After
\exists t\in\mathbb{R}:\ 1=4t\ \land\ 3=0Conditions: none
Rule: image_preimage_def · Uses: S03, G3
Leaf basis: image_preimage_def + cartesian_product_def
L(A,B) is the image of t↦(4t,0), so C∈L(A,B) means exactly that some real t gives (1,3)=(4t,0); equality of ordered pairs splits this into the coordinate equations 1=4t and 3=0, both with the same t.
S05 · implies
Before
\exists t\in\mathbb{R}:\ 1=4t\ \land\ 3=0After
C\notin L(A,B)
Conditions: none
Rule: contradiction · Uses: S04
Leaf basis: contradiction + quantifier_negation + numeric_evaluation
The second equation 3=0 does not involve t and fails for every t, so the conjunction fails for every t and no such t exists; by the equivalence S04, C∉L(A,B). Note that the first equation alone has the solution t=1/4, so looking at the first coordinate alone would mislead.
S06 · equivalent
Before
A,B,C\ \text{collinear}After
\exists P,Q,\ P\neq Q:\ A,B,C\in L(P,Q)
Conditions: none
Rule: collinear_def · Uses: G1, G2
Leaf basis: collinear_def + line_def + def_unfold
By G2, the three points are collinear when one line contains all three; by G1, the lines of the model are exactly the sets L(P,Q) for distinct P, Q. Together the two definitions give the right-hand side. The next step temporarily assumes the points are collinear and sees what follows.
S07 · implies
Before
A,B,C\in L(P,Q),\ P\neq Q,\ A\neq B
After
L(P,Q)=L(A,B),\ C\in L(A,B)
Conditions: P\neq Q; A\neq B
Rule: L_line_unique · Uses: S02, S06, L_line_unique
Leaf basis: L_line_unique + exists_elim + eq_replace
Assume A, B, C are collinear; by S06 take P≠Q with A, B, C∈L(P,Q) (∃-elimination; P and Q are fresh names). A and B are two points of L(P,Q) and A≠B (S02), so Lemma L_line_unique (X=A, Y=B) gives L(P,Q)=L(A,B). Then C∈L(P,Q) gives C∈L(A,B). The lemma is proved in S07.1 to S07.3.
S08 · implies
Before
C\in L(A,B)\ \text{(under the assumption)},\ C\notin L(A,B)After
A,B,C\ \text{noncollinear}Conditions: none
Rule: contradiction · Uses: S05, S07
Leaf basis: contradiction + imp_intro
The collinearity assumption leads to C∈L(A,B) (S07), but S05 proved C∉L(A,B): a contradiction. By proof by contradiction the assumption fails: no line contains A, B and C, that is, the three points are noncollinear. This is the MKO's second hypothesis.
S09 · theorem_application
Before
A,B,C\ \text{distinct and noncollinear}After
\triangle ABC=[A,B]\cup[B,C]\cup[C,A]\ \text{nondegenerate}Conditions: A\neq B,\ B\neq C,\ C\neq A; A,B,C\ \text{noncollinear}
Rule: mko_triangle_def · Uses: S02, S08, mko_triangle_def
Leaf basis: mko_triangle_def + and_intro_elim
Both hypotheses hold (S02, S08), so by the MKO the union of the three segments determines the nondegenerate triangle ABC. Its vertices are the three points A, B, C; its sides are the three segments [A,B], [B,C], [C,A]. The side opposite a vertex is the side that does not have it as an endpoint: BC is opposite A, CA is opposite B, and AB is opposite C.
S10 · equivalent
Before
[A,B],\ [B,C],\ [C,A]
After
\{(4t,0)\},\ \{(4-3t,\,3t)\},\ \{(1-t,\,3-3t)\}\quad(0\le t\le 1)Conditions: none
Rule: segment_def · Uses: S09, G1, G3
Leaf basis: segment_def + coord_ops + numeric_evaluation
By the segment definition and coordinatewise operations: B−A=(4,0), so [A,B]={(4t,0)}; C−B=(1−4, 3−0)=(−3,3), so [B,C]={(4−3t, 3t)}; A−C=(0−1, 0−3)=(−1,−3), so [C,A]={(1−t, 3−3t)}; all with 0≤t≤1.
S11 · equivalent
Before
\triangle ACB=[A,C]\cup[C,B]\cup[B,A]
After
[C,A]\cup[B,C]\cup[A,B]=\triangle ABC
Conditions: none
Rule: L_seg_reverse · Uses: S09, L_seg_reverse
Leaf basis: L_seg_reverse + set_operations_def + set_extensionality
Changing the order of the vertices only changes the name: by Lemma L_seg_reverse, [A,C]=[C,A], [C,B]=[B,C] and [B,A]=[A,B]; a union does not depend on order, so ACB and ABC are the same set. The lemma is proved in S11.1 and S11.2.
S12 · implies
Before
A=(4-3t,\,3t),\ 0\le t\le 1
After
A\notin[B,C]
Conditions: none
Rule: contradiction · Uses: S10, G3
Leaf basis: contradiction + cartesian_product_def + numeric_evaluation
If A∈[B,C], some t gives (0,0)=(4−3t, 3t). The second coordinate 0=3t gives t=0, and then the first coordinate is 4−3·0=4≠0, a contradiction. So the vertex A is not on its opposite side BC. The general reason: [B,C]⊆L(B,C), and A∈L(B,C) would make the three points collinear, contradicting S08.
S13 · equivalent
Before
G\in\triangle ABC
After
G\in[A,B]\ \lor\ G\in[B,C]\ \lor\ G\in[C,A]
Conditions: none
Rule: set_operations_def · Uses: S09, G3
Leaf basis: set_operations_def + def_unfold
G=((0+4+1)/3, (0+0+3)/3)=(5/3,1) is the average of the three vertices. By the MKO, triangle ABC is the union of its three sides, so G is on the triangle exactly when it is on at least one side. The three sub-steps check each side.
S14 · implies
Before
G\notin[A,B],\ G\notin[B,C],\ G\notin[C,A]
After
G\notin\triangle ABC
Conditions: none
Rule: de_morgan_logic · Uses: S13, S13.1, S13.2, S13.3
Leaf basis: de_morgan_logic + set_operations_def
All three disjuncts fail, so by De Morgan's law the disjunction is false, and by the equivalence S13, G∉△ABC. In a sketch G lies in the region the triangle encloses, but the triangle in the MKO is the union of the three sides and contains no interior point. By contrast M=(2,0)=(4·(1/2),0) is on [A,B], so M∈△ABC.
S15 · implies
Before
A=(0,0),\ D=(2,1),\ E=(6,3)
After
A,D,E\in L(A,D)
Conditions: A\neq D
Rule: collinear_def · Uses: G1, G2, G3
Leaf basis: collinear_def + exists_intro + coord_ops + numeric_evaluation
A≠D (first coordinates 0≠2), so L(A,D) is defined, and D−A=(2,1). t=0 gives A, t=1 gives D, and t=3 gives A+3(D−A)=(6,3)=E. All three points lie on the one line L(A,D), so by G2 they are collinear. They are also pairwise distinct (the first coordinate 6 of E differs from 0 and from 2).
S16 · implies
Before
\text{S09, S10, S14, S15}After
\triangle ABC\ \text{nondegenerate};\ A,D,E\ \text{give no nondegenerate triangle}Conditions: none
Rule: mko_triangle_def · Uses: S09, S10, S12, S14, S15
Leaf basis: mko_triangle_def + and_intro_elim
A, B, C are distinct and noncollinear and determine the nondegenerate triangle ABC, with sides as in S10 and opposite sides as in S09, and G is not on the triangle. A, D, E are distinct but collinear, violating the MKO's second hypothesis, so they do not determine a nondegenerate triangle in this entry's sense.
Substeps and lemmas
S07.1 · implies
Before
X,Y\in L(P,Q),\ X\neq Y,\ D=Q-P
After
X=P+sD,\ Y=P+uD,\ s\neq u
Conditions: none
Rule: exists_elim · Uses: G1
Leaf basis: exists_elim + contrapositive + eq_replace
X∈L(P,Q) gives some real s with X=P+sD, and Y∈L(P,Q) gives some real u with Y=P+uD (∃-elimination; s and u are fresh names). If s=u, then X=P+sD=P+uD=Y, contradicting X≠Y; so s≠u.
S07.2 · equivalent
Before
X+t(Y-X)
After
P+\bigl(s+t(u-s)\bigr)D
Conditions: none
Rule: distributive · Uses: S07.1
Leaf basis: distributive + add_assoc + add_comm + mul_comm + coord_ops
First Y−X=(P+uD)−(P+sD)=(u−s)D; then X+t(Y−X)=P+sD+t(u−s)D=P+(s+t(u−s))D. In each coordinate only associativity, commutativity and distributivity are used, so it holds for every real t (N14 checks it as a polynomial identity).
S07.3 · implies
Before
L(X,Y)=\{P+(s+t(u-s))D\mid t\in\mathbb{R}\}After
L(X,Y)=\{P+rD\mid r\in\mathbb{R}\}=L(P,Q)Conditions: u-s\neq 0
Rule: set_extensionality · Uses: S07.1, S07.2
Leaf basis: set_extensionality + subset_def + mul_inverse_nonzero + exists_intro
⊆: each s+t(u−s) is a real number r, so every point of L(X,Y) is in L(P,Q). ⊇: given a real r, take t=(r−s)/(u−s), which is defined because u−s≠0, and then s+t(u−s)=r, so P+rD∈L(X,Y). The two inclusions give equality of the sets. S07.1 to S07.3 together prove Lemma L_line_unique.
S11.1 · equivalent
Before
P+t(Q-P)
After
Q+(1-t)(P-Q)
Conditions: none
Rule: distributive · Uses: G1
Leaf basis: distributive + add_inverse + add_comm + add_assoc + coord_ops
Expand the right side: Q+(1−t)(P−Q)=Q+P−Q−tP+tQ=P+t(Q−P). In each coordinate this is a polynomial identity of reals, valid for every t, P and Q (N15).
S11.2 · implies
Before
0\le t\le 1
After
[P,Q]=[Q,P]
Conditions: none
Rule: set_extensionality · Uses: S11.1
Leaf basis: order_basics + set_extensionality + subset_def
0≤t≤1 ⇔ 0≤1−t≤1 (multiplying by −1 reverses the inequalities, then add 1). So as t runs over [0,1], 1−t also runs over exactly [0,1]; with S11.1, every point of [P,Q] is a point of [Q,P] and conversely. S11.1 and S11.2 together prove Lemma L_seg_reverse.
S13.1 · implies
Before
(5/3,\,1)=(4t,\,0)
After
G\notin[A,B]
Conditions: none
Rule: contradiction · Uses: S10
Leaf basis: cartesian_product_def + contradiction
Every point of [A,B] has second coordinate 0, while G has second coordinate 1, and 1≠0, so G∉[A,B].
S13.2 · implies
Before
(5/3,\,1)=(4-3t,\,3t)
After
G\notin[B,C]
Conditions: none
Rule: contradiction · Uses: S10
Leaf basis: eq_congruence + mul_inverse_nonzero + contradiction + numeric_evaluation
The second coordinate gives 1=3t ⇔ t=1/3 (3≠0); in the first coordinate this gives 4−3·(1/3)=3, and 3≠5/3, so no t satisfies both, and G∉[B,C].
S13.3 · implies
Before
(5/3,\,1)=(1-t,\,3-3t)
After
G\notin[C,A]
Conditions: none
Rule: contradiction · Uses: S10
Leaf basis: eq_congruence + mul_inverse_nonzero + contradiction + numeric_evaluation
The second coordinate gives 1=3−3t ⇔ t=(3−1)/3=2/3; in the first coordinate this gives 1−2/3=1/3, and 1/3≠5/3, so G∉[C,A].