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→BBtwnAC∧ACCgrDF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF

Proof

Step Hyp Ref Expression
1 simpl1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF→N∈ℕ
2 simpl3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF→F∈𝔼⁡N
3 simpl3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF→D∈𝔼⁡N
4 btwndiff ⊢N∈ℕ∧F∈𝔼⁡N∧D∈𝔼⁡N→∃g∈𝔼⁡NDBtwnFg∧D≠g
5 1 2 3 4 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF→∃g∈𝔼⁡NDBtwnFg∧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∈𝔼⁡NDBtwnge∧DeCgrAB
12 6 7 8 9 10 11 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N→∃e∈𝔼⁡NDBtwnge∧DeCgrAB
13 12 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g→∃e∈𝔼⁡NDBtwnge∧DeCgrAB
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∈𝔼⁡NeBtwngf∧efCgrBC
21 15 16 17 18 19 20 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N→∃f∈𝔼⁡NeBtwngf∧efCgrBC
22 21 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→∃f∈𝔼⁡NeBtwngf∧efCgrBC
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 ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→D≠g
28 27 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→D≠g
29 28 necomd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→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 ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→DBtwnge
36 35 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DBtwnge
37 simprrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→eBtwngf
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∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DBtwngf
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∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→eBtwnDf
43 simplll ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→BBtwnAC
44 43 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→BBtwnAC
45 simprr ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→DeCgrAB
46 45 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DeCgrAB
47 simprrr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→efCgrBC
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∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DfCgrAC
49 38 48 jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DBtwngf∧DfCgrAC
50 simpl3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N→F∈𝔼⁡N
51 simplrl ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→DBtwnFg
52 51 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DBtwnFg
53 30 32 50 31 52 btwncomand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DBtwngF
54 simpllr ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→ACCgrDF
55 54 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→ACCgrDF
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∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DFCgrAC
57 53 56 jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→DBtwngF∧DFCgrAC
58 29 49 57 3jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→g≠D∧DBtwngf∧DfCgrAC∧DBtwngF∧DFCgrAC
59 58 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→g≠D∧DBtwngf∧DfCgrAC∧DBtwngF∧DFCgrAC
60 segconeq ⊢N∈ℕ∧D∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧g∈𝔼⁡N∧f∈𝔼⁡N∧F∈𝔼⁡N→g≠D∧DBtwngf∧DfCgrAC∧DBtwngF∧DFCgrAC→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∧DBtwngf∧DfCgrAC∧DBtwngF∧DFCgrAC→f=F
62 59 61 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→f=F
63 62 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→f=F
64 opeq2 ⊢f=F→gf=gF
65 64 breq2d ⊢f=F→eBtwngf↔eBtwngF
66 opeq2 ⊢f=F→ef=eF
67 66 breq1d ⊢f=F→efCgrBC↔eFCgrBC
68 65 67 anbi12d ⊢f=F→eBtwngf∧efCgrBC↔eBtwngF∧eFCgrBC
69 68 biimpa ⊢f=F∧eBtwngf∧efCgrBC→eBtwngF∧eFCgrBC
70 simpl ⊢eBtwngF∧eFCgrBC→eBtwngF
71 btwnexch3 ⊢N∈ℕ∧g∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N→DBtwnge∧eBtwngF→eBtwnDF
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→DBtwnge∧eBtwngF→eBtwnDF
73 35 70 72 syl2ani ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N→BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→eBtwnDF
74 73 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→eBtwnDF
75 simplrr ⊢BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→DeCgrAB
76 75 adantl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→DeCgrAB
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∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→ABCgrDe
78 54 ad2antrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→ACCgrDF
79 simprrr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→eFCgrBC
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∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→BCCgreF
81 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DeF↔ABCgrDe∧ACCgrDF∧BCCgreF
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→ABCCgr3DeF↔ABCgrDe∧ACCgrDF∧BCCgreF
83 82 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→ABCCgr3DeF↔ABCgrDe∧ACCgrDF∧BCCgreF
84 77 78 80 83 mpbir3and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→ABCCgr3DeF
85 74 84 jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngF∧eFCgrBC→eBtwnDF∧ABCCgr3DeF
86 85 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→eBtwngF∧eFCgrBC→eBtwnDF∧ABCCgr3DeF
87 69 86 syl5 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→f=F∧eBtwngf∧efCgrBC→eBtwnDF∧ABCCgr3DeF
88 87 expcomd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→eBtwngf∧efCgrBC→f=F→eBtwnDF∧ABCCgr3DeF
89 88 impr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→f=F→eBtwnDF∧ABCCgr3DeF
90 63 89 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧eBtwngf∧efCgrBC→eBtwnDF∧ABCCgr3DeF
91 90 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→eBtwngf∧efCgrBC→eBtwnDF∧ABCCgr3DeF
92 26 91 sylanb ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧f∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→eBtwngf∧efCgrBC→eBtwnDF∧ABCCgr3DeF
93 92 an32s ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB∧f∈𝔼⁡N→eBtwngf∧efCgrBC→eBtwnDF∧ABCCgr3DeF
94 93 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→∃f∈𝔼⁡NeBtwngf∧efCgrBC→eBtwnDF∧ABCCgr3DeF
95 22 94 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧DBtwnge∧DeCgrAB→eBtwnDF∧ABCCgr3DeF
96 95 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g→DBtwnge∧DeCgrAB→eBtwnDF∧ABCCgr3DeF
97 14 96 sylanb ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g→DBtwnge∧DeCgrAB→eBtwnDF∧ABCCgr3DeF
98 97 an32s ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g∧e∈𝔼⁡N→DBtwnge∧DeCgrAB→eBtwnDF∧ABCCgr3DeF
99 98 reximdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g→∃e∈𝔼⁡NDBtwnge∧DeCgrAB→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
100 13 99 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧DBtwnFg∧D≠g→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
101 100 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧g∈𝔼⁡N∧BBtwnAC∧ACCgrDF→DBtwnFg∧D≠g→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
102 101 an32s ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF∧g∈𝔼⁡N→DBtwnFg∧D≠g→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
103 102 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF→∃g∈𝔼⁡NDBtwnFg∧D≠g→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
104 5 103 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ACCgrDF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
105 104 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ACCgrDF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF