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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> N e. NN )
2 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> F e. ( EE ` N ) )
3 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> D e. ( EE ` N ) )
4 btwndiff 
 |-  ( ( N e. NN /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> E. g e. ( EE ` N ) ( D Btwn <. F , g >. /\ D =/= g ) )
5 1 2 3 4 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> E. g e. ( EE ` N ) ( D Btwn <. F , g >. /\ D =/= g ) )
6 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) -> N e. NN )
7 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) -> g e. ( EE ` N ) )
8 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) -> D e. ( EE ` N ) )
9 simpl21 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) -> A e. ( EE ` N ) )
10 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) -> B e. ( EE ` N ) )
11 axsegcon 
 |-  ( ( N e. NN /\ ( g e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. e e. ( EE ` N ) ( D Btwn <. g , e >. /\ <. D , e >. Cgr <. A , B >. ) )
12 6 7 8 9 10 11 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) -> E. e e. ( EE ` N ) ( D Btwn <. g , e >. /\ <. D , e >. Cgr <. A , B >. ) )
13 12 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) /\ ( D Btwn <. F , g >. /\ D =/= g ) ) ) -> E. e e. ( EE ` N ) ( D Btwn <. g , e >. /\ <. D , e >. Cgr <. A , B >. ) )
14 anass 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ e e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) )
15 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> N e. NN )
16 simprl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> g e. ( EE ` N ) )
17 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> e e. ( EE ` N ) )
18 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
19 simpl23 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
20 axsegcon 
 |-  ( ( N e. NN /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( e Btwn <. g , f >. /\ <. e , f >. Cgr <. B , C >. ) )
21 15 16 17 18 19 20 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( e Btwn <. g , f >. /\ <. e , f >. Cgr <. B , C >. ) )
22 21 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` 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. f e. ( EE ` N ) ( e Btwn <. g , f >. /\ <. e , f >. Cgr <. B , C >. ) )
23 anass 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) /\ f e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ f e. ( EE ` N ) ) ) )
24 df-3an 
 |-  ( ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) <-> ( ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ f e. ( EE ` N ) ) )
25 24 anbi2i 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ f e. ( EE ` N ) ) ) )
26 23 25 bitr4i 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) /\ f e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> N e. NN )
31 simpr1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> g e. ( EE ` N ) )
32 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
33 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> e e. ( EE ` N ) )
34 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
40 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
41 simpl23 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
42 30 31 32 33 34 36 37 btwnexch3and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> F e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( D e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( g e. ( EE ` N ) /\ f e. ( EE ` N ) /\ F e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( g e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( D Btwn <. g , e >. /\ e Btwn <. g , F >. ) -> e Btwn <. D , F >. ) )
72 30 31 32 33 50 71 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( D Btwn <. g , e >. /\ e Btwn <. g , F >. ) -> e Btwn <. D , F >. ) )
73 35 70 72 syl2ani 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ e e. ( EE ` N ) /\ F e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) /\ f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` 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 e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` 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. f e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( g e. ( EE ` N ) /\ e e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ e e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) /\ ( D Btwn <. F , g >. /\ D =/= g ) ) ) /\ e e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) /\ ( D Btwn <. F , g >. /\ D =/= g ) ) ) -> ( E. e e. ( EE ` N ) ( D Btwn <. g , e >. /\ <. D , e >. Cgr <. A , B >. ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
100 13 99 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) /\ ( D Btwn <. F , g >. /\ D =/= g ) ) ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) )
101 100 expr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ g e. ( EE ` N ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> ( ( D Btwn <. F , g >. /\ D =/= g ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
102 101 an32s 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) /\ g e. ( EE ` N ) ) -> ( ( D Btwn <. F , g >. /\ D =/= g ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
103 102 rexlimdva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> ( E. g e. ( EE ` N ) ( D Btwn <. F , g >. /\ D =/= g ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
104 5 103 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) )
105 104 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )