Metamath Proof Explorer

Theorem cgrxfr

Description: A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion cgrxfr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → N ∈ ℕ
2 simpl3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → F ∈ 𝔼 ⁡ N
3 simpl3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → D ∈ 𝔼 ⁡ N
4 btwndiff ⊢ N ∈ ℕ ∧ F ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ g ∈ 𝔼 ⁡ N D Btwn F g ∧ D ≠ g
5 1 2 3 4 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → ∃ g ∈ 𝔼 ⁡ N D Btwn F g ∧ D ≠ g
6 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N → N ∈ ℕ
7 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N → g ∈ 𝔼 ⁡ N
8 simpl3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
9 simpl21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
10 simpl22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
11 axsegcon ⊢ N ∈ ℕ ∧ g ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ e ∈ 𝔼 ⁡ N D Btwn g e ∧ D e Cgr A B
12 6 7 8 9 10 11 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N → ∃ e ∈ 𝔼 ⁡ N D Btwn g e ∧ D e Cgr A B
13 12 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g → ∃ e ∈ 𝔼 ⁡ N D Btwn g e ∧ D e Cgr A B
14 anass ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ↔ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N
15 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → N ∈ ℕ
16 simprl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → g ∈ 𝔼 ⁡ N
17 simprr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → e ∈ 𝔼 ⁡ N
18 simpl22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
19 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
20 axsegcon ⊢ N ∈ ℕ ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∃ f ∈ 𝔼 ⁡ N e Btwn g f ∧ e f Cgr B C
21 15 16 17 18 19 20 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → ∃ f ∈ 𝔼 ⁡ N e Btwn g f ∧ e f Cgr B C
22 21 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → ∃ f ∈ 𝔼 ⁡ N e Btwn g f ∧ e f Cgr B C
23 anass ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ↔ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N
24 df-3an ⊢ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ↔ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N
25 24 anbi2i ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ↔ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N
26 23 25 bitr4i ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ↔ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N
27 simplrr ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → D ≠ g
28 27 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D ≠ g
29 28 necomd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → g ≠ D
30 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → N ∈ ℕ
31 simpr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → g ∈ 𝔼 ⁡ N
32 simpl3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
33 simpr2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → e ∈ 𝔼 ⁡ N
34 simpr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → f ∈ 𝔼 ⁡ N
35 simprl ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → D Btwn g e
36 35 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D Btwn g e
37 simprrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → e Btwn g f
38 30 31 32 33 34 36 37 btwnexchand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D Btwn g f
39 simpl21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
40 simpl22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
41 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
42 30 31 32 33 34 36 37 btwnexch3and ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → e Btwn D f
43 simplll ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → B Btwn A C
44 43 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → B Btwn A C
45 simprr ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → D e Cgr A B
46 45 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D e Cgr A B
47 simprrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → e f Cgr B C
48 30 32 33 34 39 40 41 42 44 46 47 cgrextendand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D f Cgr A C
49 38 48 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D Btwn g f ∧ D f Cgr A C
50 simpl3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → F ∈ 𝔼 ⁡ N
51 simplrl ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → D Btwn F g
52 51 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D Btwn F g
53 30 32 50 31 52 btwncomand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D Btwn g F
54 simpllr ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → A C Cgr D F
55 54 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → A C Cgr D F
56 30 39 41 32 50 55 cgrcomand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D F Cgr A C
57 53 56 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → D Btwn g F ∧ D F Cgr A C
58 29 49 57 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → g ≠ D ∧ D Btwn g f ∧ D f Cgr A C ∧ D Btwn g F ∧ D F Cgr A C
59 58 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → g ≠ D ∧ D Btwn g f ∧ D f Cgr A C ∧ D Btwn g F ∧ D F Cgr A C
60 segconeq ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → g ≠ D ∧ D Btwn g f ∧ D f Cgr A C ∧ D Btwn g F ∧ D F Cgr A C → f = F
61 30 32 39 41 31 34 50 60 syl133anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → g ≠ D ∧ D Btwn g f ∧ D f Cgr A C ∧ D Btwn g F ∧ D F Cgr A C → f = F
62 59 61 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → f = F
63 62 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → f = F
64 opeq2 ⊢ f = F → g f = g F
65 64 breq2d ⊢ f = F → e Btwn g f ↔ e Btwn g F
66 opeq2 ⊢ f = F → e f = e F
67 66 breq1d ⊢ f = F → e f Cgr B C ↔ e F Cgr B C
68 65 67 anbi12d ⊢ f = F → e Btwn g f ∧ e f Cgr B C ↔ e Btwn g F ∧ e F Cgr B C
69 68 biimpa ⊢ f = F ∧ e Btwn g f ∧ e f Cgr B C → e Btwn g F ∧ e F Cgr B C
70 simpl ⊢ e Btwn g F ∧ e F Cgr B C → e Btwn g F
71 btwnexch3 ⊢ N ∈ ℕ ∧ g ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D Btwn g e ∧ e Btwn g F → e Btwn D F
72 30 31 32 33 50 71 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → D Btwn g e ∧ e Btwn g F → e Btwn D F
73 35 70 72 syl2ani ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → e Btwn D F
74 73 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → e Btwn D F
75 simplrr ⊢ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → D e Cgr A B
76 75 adantl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → D e Cgr A B
77 30 32 33 39 40 76 cgrcomand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → A B Cgr D e
78 54 ad2antrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → A C Cgr D F
79 simprrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → e F Cgr B C
80 30 33 50 40 41 79 cgrcomand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → B C Cgr e F
81 brcgr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D e F ↔ A B Cgr D e ∧ A C Cgr D F ∧ B C Cgr e F
82 30 39 40 41 32 33 50 81 syl133anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A B C Cgr3 D e F ↔ A B Cgr D e ∧ A C Cgr D F ∧ B C Cgr e F
83 82 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → A B C Cgr3 D e F ↔ A B Cgr D e ∧ A C Cgr D F ∧ B C Cgr e F
84 77 78 80 83 mpbir3and ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → A B C Cgr3 D e F
85 74 84 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g F ∧ e F Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
86 85 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → e Btwn g F ∧ e F Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
87 69 86 syl5 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → f = F ∧ e Btwn g f ∧ e f Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
88 87 expcomd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → e Btwn g f ∧ e f Cgr B C → f = F → e Btwn D F ∧ A B C Cgr3 D e F
89 88 impr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → f = F → e Btwn D F ∧ A B C Cgr3 D e F
90 63 89 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ e Btwn g f ∧ e f Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
91 90 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → e Btwn g f ∧ e f Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
92 26 91 sylanb ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → e Btwn g f ∧ e f Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
93 92 an32s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B ∧ f ∈ 𝔼 ⁡ N → e Btwn g f ∧ e f Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
94 93 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → ∃ f ∈ 𝔼 ⁡ N e Btwn g f ∧ e f Cgr B C → e Btwn D F ∧ A B C Cgr3 D e F
95 22 94 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ D Btwn g e ∧ D e Cgr A B → e Btwn D F ∧ A B C Cgr3 D e F
96 95 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g → D Btwn g e ∧ D e Cgr A B → e Btwn D F ∧ A B C Cgr3 D e F
97 14 96 sylanb ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g → D Btwn g e ∧ D e Cgr A B → e Btwn D F ∧ A B C Cgr3 D e F
98 97 an32s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g ∧ e ∈ 𝔼 ⁡ N → D Btwn g e ∧ D e Cgr A B → e Btwn D F ∧ A B C Cgr3 D e F
99 98 reximdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g → ∃ e ∈ 𝔼 ⁡ N D Btwn g e ∧ D e Cgr A B → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
100 13 99 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ D Btwn F g ∧ D ≠ g → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
101 100 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ g ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → D Btwn F g ∧ D ≠ g → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
102 101 an32s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F ∧ g ∈ 𝔼 ⁡ N → D Btwn F g ∧ D ≠ g → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
103 102 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → ∃ g ∈ 𝔼 ⁡ N D Btwn F g ∧ D ≠ g → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
104 5 103 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A C Cgr D F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
105 104 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F