Metamath Proof Explorer

Theorem lineext

Description: Extend a line with a missing point. Theorem 4.14 of Schwabhauser p. 37. (Contributed by Scott Fenton, 6-Oct-2013)

Ref Expression
Assertion lineext ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Colinear B C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f

Proof

Step Hyp Ref Expression
1 brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
2 1 3adant3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
3 2 anbi1d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Colinear B C ∧ A B Cgr D E ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ∧ A B Cgr D E
4 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → N ∈ ℕ
5 simp3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N
6 simp3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
7 5 6 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N
8 simp21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
9 simp23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
10 8 9 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
11 4 7 10 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ E ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
12 11 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → N ∈ ℕ ∧ E ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
13 axsegcon ⊢ N ∈ ℕ ∧ E ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∃ f ∈ 𝔼 ⁡ N D Btwn E f ∧ D f Cgr A C
14 12 13 syl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N D Btwn E f ∧ D f Cgr A C
15 simprlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E ∧ D Btwn E f ∧ A C Cgr D f → A B Cgr D E
16 simprrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E ∧ D Btwn E f ∧ A C Cgr D f → A C Cgr D f
17 an4 ⊢ A Btwn B C ∧ A B Cgr D E ∧ D Btwn E f ∧ A C Cgr D f ↔ A Btwn B C ∧ D Btwn E f ∧ A B Cgr D E ∧ A C Cgr D f
18 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → N ∈ ℕ
19 simpl21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
20 simpl22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
21 simpl3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
22 simpl3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N
23 cgrcomlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A B Cgr D E ↔ B A Cgr E D
24 18 19 20 21 22 23 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A B Cgr D E ↔ B A Cgr E D
25 24 anbi1d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A B Cgr D E ∧ A C Cgr D f ↔ B A Cgr E D ∧ A C Cgr D f
26 25 anbi2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A Btwn B C ∧ D Btwn E f ∧ A B Cgr D E ∧ A C Cgr D f ↔ A Btwn B C ∧ D Btwn E f ∧ B A Cgr E D ∧ A C Cgr D f
27 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
28 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → f ∈ 𝔼 ⁡ N
29 cgrextend ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A Btwn B C ∧ D Btwn E f ∧ B A Cgr E D ∧ A C Cgr D f → B C Cgr E f
30 18 20 19 27 22 21 28 29 syl133anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A Btwn B C ∧ D Btwn E f ∧ B A Cgr E D ∧ A C Cgr D f → B C Cgr E f
31 26 30 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A Btwn B C ∧ D Btwn E f ∧ A B Cgr D E ∧ A C Cgr D f → B C Cgr E f
32 17 31 biimtrid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A Btwn B C ∧ A B Cgr D E ∧ D Btwn E f ∧ A C Cgr D f → B C Cgr E f
33 32 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E ∧ D Btwn E f ∧ A C Cgr D f → B C Cgr E f
34 15 16 33 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E ∧ D Btwn E f ∧ A C Cgr D f → A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
35 34 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → D Btwn E f ∧ A C Cgr D f → A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
36 cgrcom ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → D f Cgr A C ↔ A C Cgr D f
37 18 21 28 19 27 36 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → D f Cgr A C ↔ A C Cgr D f
38 37 anbi2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → D Btwn E f ∧ D f Cgr A C ↔ D Btwn E f ∧ A C Cgr D f
39 38 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → D Btwn E f ∧ D f Cgr A C ↔ D Btwn E f ∧ A C Cgr D f
40 simpl2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
41 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
42 18 40 21 22 28 41 syl113anc ⊢ 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
43 42 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → A B C Cgr3 D E f ↔ A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
44 35 39 43 3imtr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → D Btwn E f ∧ D f Cgr A C → A B C Cgr3 D E f
45 44 an32s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E ∧ f ∈ 𝔼 ⁡ N → D Btwn E f ∧ D f Cgr A C → A B C Cgr3 D E f
46 45 reximdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N D Btwn E f ∧ D f Cgr A C → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
47 14 46 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ A Btwn B C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
48 47 exp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Btwn B C → A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
49 3ancoma ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ↔ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
50 btwncom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
51 49 50 sylan2b ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
52 51 3adant3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
53 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N
54 simp22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
55 axsegcon ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∃ f ∈ 𝔼 ⁡ N E Btwn D f ∧ E f Cgr B C
56 4 53 54 9 55 syl112anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → ∃ f ∈ 𝔼 ⁡ N E Btwn D f ∧ E f Cgr B C
57 56 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N E Btwn D f ∧ E f Cgr B C
58 cgrextend ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ B C Cgr E f → A C Cgr D f
59 18 40 21 22 28 58 syl113anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ B C Cgr E f → A C Cgr D f
60 simpll ⊢ A B Cgr D E ∧ B C Cgr E f ∧ A C Cgr D f → A B Cgr D E
61 simpr ⊢ A B Cgr D E ∧ B C Cgr E f ∧ A C Cgr D f → A C Cgr D f
62 simplr ⊢ A B Cgr D E ∧ B C Cgr E f ∧ A C Cgr D f → B C Cgr E f
63 60 61 62 3jca ⊢ A B Cgr D E ∧ B C Cgr E f ∧ A C Cgr D f → A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
64 63 ex ⊢ A B Cgr D E ∧ B C Cgr E f → A C Cgr D f → A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
65 64 adantl ⊢ B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ B C Cgr E f → A C Cgr D f → A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
66 59 65 sylcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ B C Cgr E f → A B Cgr D E ∧ A C Cgr D f ∧ B C Cgr E f
67 an4 ⊢ B Btwn A C ∧ A B Cgr D E ∧ E Btwn D f ∧ E f Cgr B C ↔ B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ E f Cgr B C
68 cgrcom ⊢ N ∈ ℕ ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → E f Cgr B C ↔ B C Cgr E f
69 18 22 28 20 27 68 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → E f Cgr B C ↔ B C Cgr E f
70 69 anbi2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A B Cgr D E ∧ E f Cgr B C ↔ A B Cgr D E ∧ B C Cgr E f
71 70 anbi2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ E f Cgr B C ↔ B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ B C Cgr E f
72 67 71 bitrid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B Cgr D E ∧ E Btwn D f ∧ E f Cgr B C ↔ B Btwn A C ∧ E Btwn D f ∧ A B Cgr D E ∧ B C Cgr E f
73 66 72 42 3imtr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B Cgr D E ∧ E Btwn D f ∧ E f Cgr B C → A B C Cgr3 D E f
74 73 expdimp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B Cgr D E → E Btwn D f ∧ E f Cgr B C → A B C Cgr3 D E f
75 74 an32s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B Cgr D E ∧ f ∈ 𝔼 ⁡ N → E Btwn D f ∧ E f Cgr B C → A B C Cgr3 D E f
76 75 reximdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N E Btwn D f ∧ E f Cgr B C → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
77 57 76 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
78 77 exp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → B Btwn A C → A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
79 52 78 sylbird ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → B Btwn C A → A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
80 cgrxfr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → C Btwn A B ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N f Btwn D E ∧ A C B Cgr3 D f E
81 4 8 9 54 53 80 syl131anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → C Btwn A B ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N f Btwn D E ∧ A C B Cgr3 D f E
82 cgr3permute1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A B C Cgr3 D E f ↔ A C B Cgr3 D f E
83 18 40 21 22 28 82 syl113anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A B C Cgr3 D E f ↔ A C B Cgr3 D f E
84 83 biimprd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → A C B Cgr3 D f E → A B C Cgr3 D E f
85 84 adantld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ f ∈ 𝔼 ⁡ N → f Btwn D E ∧ A C B Cgr3 D f E → A B C Cgr3 D E f
86 85 reximdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → ∃ f ∈ 𝔼 ⁡ N f Btwn D E ∧ A C B Cgr3 D f E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
87 81 86 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → C Btwn A B ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
88 87 expd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → C Btwn A B → A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
89 48 79 88 3jaod ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B → A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
90 89 impd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f
91 3 90 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A Colinear B C ∧ A B Cgr D E → ∃ f ∈ 𝔼 ⁡ N A B C Cgr3 D E f