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→AColinearBC∧ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf

Proof

Step Hyp Ref Expression
1 brcolinear ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔ABtwnBC∨BBtwnCA∨CBtwnAB
2 1 3adant3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→AColinearBC↔ABtwnBC∨BBtwnCA∨CBtwnAB
3 2 anbi1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→AColinearBC∧ABCgrDE↔ABtwnBC∨BBtwnCA∨CBtwnAB∧ABCgrDE
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∧ABtwnBC∧ABCgrDE→N∈ℕ∧E∈𝔼⁡N∧D∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N
13 axsegcon ⊢N∈ℕ∧E∈𝔼⁡N∧D∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→∃f∈𝔼⁡NDBtwnEf∧DfCgrAC
14 12 13 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧ABtwnBC∧ABCgrDE→∃f∈𝔼⁡NDBtwnEf∧DfCgrAC
15 simprlr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE∧DBtwnEf∧ACCgrDf→ABCgrDE
16 simprrr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE∧DBtwnEf∧ACCgrDf→ACCgrDf
17 an4 ⊢ABtwnBC∧ABCgrDE∧DBtwnEf∧ACCgrDf↔ABtwnBC∧DBtwnEf∧ABCgrDE∧ACCgrDf
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→ABCgrDE↔BACgrED
24 18 19 20 21 22 23 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABCgrDE↔BACgrED
25 24 anbi1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABCgrDE∧ACCgrDf↔BACgrED∧ACCgrDf
26 25 anbi2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABtwnBC∧DBtwnEf∧ABCgrDE∧ACCgrDf↔ABtwnBC∧DBtwnEf∧BACgrED∧ACCgrDf
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→ABtwnBC∧DBtwnEf∧BACgrED∧ACCgrDf→BCCgrEf
30 18 20 19 27 22 21 28 29 syl133anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABtwnBC∧DBtwnEf∧BACgrED∧ACCgrDf→BCCgrEf
31 26 30 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABtwnBC∧DBtwnEf∧ABCgrDE∧ACCgrDf→BCCgrEf
32 17 31 biimtrid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABtwnBC∧ABCgrDE∧DBtwnEf∧ACCgrDf→BCCgrEf
33 32 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE∧DBtwnEf∧ACCgrDf→BCCgrEf
34 15 16 33 3jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE∧DBtwnEf∧ACCgrDf→ABCgrDE∧ACCgrDf∧BCCgrEf
35 34 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE→DBtwnEf∧ACCgrDf→ABCgrDE∧ACCgrDf∧BCCgrEf
36 cgrcom ⊢N∈ℕ∧D∈𝔼⁡N∧f∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→DfCgrAC↔ACCgrDf
37 18 21 28 19 27 36 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→DfCgrAC↔ACCgrDf
38 37 anbi2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→DBtwnEf∧DfCgrAC↔DBtwnEf∧ACCgrDf
39 38 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE→DBtwnEf∧DfCgrAC↔DBtwnEf∧ACCgrDf
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→ABCCgr3DEf↔ABCgrDE∧ACCgrDf∧BCCgrEf
42 18 40 21 22 28 41 syl113anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABCCgr3DEf↔ABCgrDE∧ACCgrDf∧BCCgrEf
43 42 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE→ABCCgr3DEf↔ABCgrDE∧ACCgrDf∧BCCgrEf
44 35 39 43 3imtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧ABtwnBC∧ABCgrDE→DBtwnEf∧DfCgrAC→ABCCgr3DEf
45 44 an32s ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧ABtwnBC∧ABCgrDE∧f∈𝔼⁡N→DBtwnEf∧DfCgrAC→ABCCgr3DEf
46 45 reximdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧ABtwnBC∧ABCgrDE→∃f∈𝔼⁡NDBtwnEf∧DfCgrAC→∃f∈𝔼⁡NABCCgr3DEf
47 14 46 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧ABtwnBC∧ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
48 47 exp32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABtwnBC→ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
49 3ancoma ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N
50 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC↔BBtwnCA
51 49 50 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC↔BBtwnCA
52 51 3adant3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→BBtwnAC↔BBtwnCA
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∈𝔼⁡NEBtwnDf∧EfCgrBC
56 4 53 54 9 55 syl112anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→∃f∈𝔼⁡NEBtwnDf∧EfCgrBC
57 56 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧BBtwnAC∧ABCgrDE→∃f∈𝔼⁡NEBtwnDf∧EfCgrBC
58 cgrextend ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧EBtwnDf∧ABCgrDE∧BCCgrEf→ACCgrDf
59 18 40 21 22 28 58 syl113anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧EBtwnDf∧ABCgrDE∧BCCgrEf→ACCgrDf
60 simpll ⊢ABCgrDE∧BCCgrEf∧ACCgrDf→ABCgrDE
61 simpr ⊢ABCgrDE∧BCCgrEf∧ACCgrDf→ACCgrDf
62 simplr ⊢ABCgrDE∧BCCgrEf∧ACCgrDf→BCCgrEf
63 60 61 62 3jca ⊢ABCgrDE∧BCCgrEf∧ACCgrDf→ABCgrDE∧ACCgrDf∧BCCgrEf
64 63 ex ⊢ABCgrDE∧BCCgrEf→ACCgrDf→ABCgrDE∧ACCgrDf∧BCCgrEf
65 64 adantl ⊢BBtwnAC∧EBtwnDf∧ABCgrDE∧BCCgrEf→ACCgrDf→ABCgrDE∧ACCgrDf∧BCCgrEf
66 59 65 sylcom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧EBtwnDf∧ABCgrDE∧BCCgrEf→ABCgrDE∧ACCgrDf∧BCCgrEf
67 an4 ⊢BBtwnAC∧ABCgrDE∧EBtwnDf∧EfCgrBC↔BBtwnAC∧EBtwnDf∧ABCgrDE∧EfCgrBC
68 cgrcom ⊢N∈ℕ∧E∈𝔼⁡N∧f∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→EfCgrBC↔BCCgrEf
69 18 22 28 20 27 68 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→EfCgrBC↔BCCgrEf
70 69 anbi2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABCgrDE∧EfCgrBC↔ABCgrDE∧BCCgrEf
71 70 anbi2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧EBtwnDf∧ABCgrDE∧EfCgrBC↔BBtwnAC∧EBtwnDf∧ABCgrDE∧BCCgrEf
72 67 71 bitrid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧ABCgrDE∧EBtwnDf∧EfCgrBC↔BBtwnAC∧EBtwnDf∧ABCgrDE∧BCCgrEf
73 66 72 42 3imtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧ABCgrDE∧EBtwnDf∧EfCgrBC→ABCCgr3DEf
74 73 expdimp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ABCgrDE→EBtwnDf∧EfCgrBC→ABCCgr3DEf
75 74 an32s ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧BBtwnAC∧ABCgrDE∧f∈𝔼⁡N→EBtwnDf∧EfCgrBC→ABCCgr3DEf
76 75 reximdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧BBtwnAC∧ABCgrDE→∃f∈𝔼⁡NEBtwnDf∧EfCgrBC→∃f∈𝔼⁡NABCCgr3DEf
77 57 76 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧BBtwnAC∧ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
78 77 exp32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→BBtwnAC→ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
79 52 78 sylbird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→BBtwnCA→ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
80 cgrxfr ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→CBtwnAB∧ABCgrDE→∃f∈𝔼⁡NfBtwnDE∧ACBCgr3DfE
81 4 8 9 54 53 80 syl131anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→CBtwnAB∧ABCgrDE→∃f∈𝔼⁡NfBtwnDE∧ACBCgr3DfE
82 cgr3permute1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABCCgr3DEf↔ACBCgr3DfE
83 18 40 21 22 28 82 syl113anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ABCCgr3DEf↔ACBCgr3DfE
84 83 biimprd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→ACBCgr3DfE→ABCCgr3DEf
85 84 adantld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧f∈𝔼⁡N→fBtwnDE∧ACBCgr3DfE→ABCCgr3DEf
86 85 reximdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→∃f∈𝔼⁡NfBtwnDE∧ACBCgr3DfE→∃f∈𝔼⁡NABCCgr3DEf
87 81 86 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→CBtwnAB∧ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
88 87 expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→CBtwnAB→ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
89 48 79 88 3jaod ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABtwnBC∨BBtwnCA∨CBtwnAB→ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
90 89 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABtwnBC∨BBtwnCA∨CBtwnAB∧ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf
91 3 90 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→AColinearBC∧ABCgrDE→∃f∈𝔼⁡NABCCgr3DEf