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

Proof

Step Hyp Ref Expression
1 brcolinear 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
2 1 3adant3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
3 2 anbi1d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> N e. NN )
5 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
6 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
7 5 6 jca 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( E e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
8 simp21 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
9 simp23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
10 8 9 jca 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
11 4 7 10 3jca 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( N e. NN /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) )
12 11 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( A Btwn <. B , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> ( N e. NN /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) )
13 axsegcon 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( D Btwn <. E , f >. /\ <. D , f >. Cgr <. A , C >. ) )
14 12 13 syl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( A Btwn <. B , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> E. f e. ( EE ` N ) ( D Btwn <. E , f >. /\ <. D , f >. Cgr <. A , C >. ) )
15 simprlr 
 |-  ( ( ( ( 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 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 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 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 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 ) ) -> N e. NN )
19 simpl21 
 |-  ( ( ( 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 e. ( EE ` N ) )
20 simpl22 
 |-  ( ( ( 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 ) ) -> B e. ( EE ` N ) )
21 simpl3l 
 |-  ( ( ( 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 ) ) -> D e. ( EE ` N ) )
22 simpl3r 
 |-  ( ( ( 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 ) ) -> E e. ( EE ` N ) )
23 cgrcomlr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> <. B , A >. Cgr <. E , D >. ) )
24 18 19 20 21 22 23 syl122anc 
 |-  ( ( ( 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 >. Cgr <. D , E >. <-> <. B , A >. Cgr <. E , D >. ) )
25 24 anbi1d 
 |-  ( ( ( 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 >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , f >. ) <-> ( <. B , A >. Cgr <. E , D >. /\ <. A , C >. Cgr <. D , f >. ) ) )
26 25 anbi2d 
 |-  ( ( ( 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 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 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 ) ) -> C e. ( EE ` N ) )
28 simpr 
 |-  ( ( ( 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 ) ) -> f e. ( EE ` N ) )
29 cgrextend 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) /\ f e. ( EE ` 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 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 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 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 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 syl5bi 
 |-  ( ( ( 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 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 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 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 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 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 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 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 e. NN /\ ( D e. ( EE ` N ) /\ f e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. D , f >. Cgr <. A , C >. <-> <. A , C >. Cgr <. D , f >. ) )
37 18 21 28 19 27 36 syl122anc 
 |-  ( ( ( 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 ) ) -> ( <. D , f >. Cgr <. A , C >. <-> <. A , C >. Cgr <. D , f >. ) )
38 37 anbi2d 
 |-  ( ( ( 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 ) ) -> ( ( D Btwn <. E , f >. /\ <. D , f >. Cgr <. A , C >. ) <-> ( D Btwn <. E , f >. /\ <. A , C >. Cgr <. D , f >. ) ) )
39 38 adantr 
 |-  ( ( ( ( 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 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 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 e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
41 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 >. ) ) )
42 18 40 21 22 28 41 syl113anc 
 |-  ( ( ( 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 >. ) ) )
43 42 adantr 
 |-  ( ( ( ( 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 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 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 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( A Btwn <. B , C >. /\ <. A , B >. Cgr <. D , E >. ) ) /\ f e. ( EE ` N ) ) -> ( ( D Btwn <. E , f >. /\ <. D , f >. Cgr <. A , C >. ) -> <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
46 45 reximdva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( A Btwn <. B , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> ( E. f e. ( EE ` N ) ( D Btwn <. E , f >. /\ <. D , f >. Cgr <. A , C >. ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
47 14 46 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( A Btwn <. B , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. )
48 47 exp32 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( A Btwn <. B , C >. -> ( <. A , B >. Cgr <. D , E >. -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) ) )
49 3ancoma 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) <-> ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
50 btwncom 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
51 49 50 sylan2b 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
52 51 3adant3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
53 simp3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) )
54 simp22 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
55 axsegcon 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( E Btwn <. D , f >. /\ <. E , f >. Cgr <. B , C >. ) )
56 4 53 54 9 55 syl112anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( E Btwn <. D , f >. /\ <. E , f >. Cgr <. B , C >. ) )
57 56 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> E. f e. ( EE ` N ) ( E Btwn <. D , f >. /\ <. E , f >. Cgr <. B , C >. ) )
58 cgrextend 
 |-  ( ( 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 ) ) ) -> ( ( ( 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 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 ) ) -> ( ( ( 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 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 ) ) -> ( ( ( 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. NN /\ ( E e. ( EE ` N ) /\ f e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. E , f >. Cgr <. B , C >. <-> <. B , C >. Cgr <. E , f >. ) )
69 18 22 28 20 27 68 syl122anc 
 |-  ( ( ( 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 ) ) -> ( <. E , f >. Cgr <. B , C >. <-> <. B , C >. Cgr <. E , f >. ) )
70 69 anbi2d 
 |-  ( ( ( 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 >. Cgr <. D , E >. /\ <. E , f >. Cgr <. B , C >. ) <-> ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , f >. ) ) )
71 70 anbi2d 
 |-  ( ( ( 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 ) ) -> ( ( ( 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 syl5bb 
 |-  ( ( ( 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 ) ) -> ( ( ( 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 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 ) ) -> ( ( ( 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 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 ) ) /\ ( 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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , B >. Cgr <. D , E >. ) ) /\ f e. ( EE ` N ) ) -> ( ( E Btwn <. D , f >. /\ <. E , f >. Cgr <. B , C >. ) -> <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
76 75 reximdva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> ( E. f e. ( EE ` N ) ( E Btwn <. D , f >. /\ <. E , f >. Cgr <. B , C >. ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
77 57 76 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , B >. Cgr <. D , E >. ) ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. )
78 77 exp32 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. -> ( <. A , B >. Cgr <. D , E >. -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) ) )
79 52 78 sylbird 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( B Btwn <. C , A >. -> ( <. A , B >. Cgr <. D , E >. -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) ) )
80 cgrxfr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , B >. Cgr <. D , E >. ) -> E. f e. ( EE ` N ) ( f Btwn <. D , E >. /\ <. A , <. C , B >. >. Cgr3 <. D , <. f , E >. >. ) ) )
81 4 8 9 54 53 80 syl131anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , B >. Cgr <. D , E >. ) -> E. f e. ( EE ` N ) ( f Btwn <. D , E >. /\ <. A , <. C , B >. >. Cgr3 <. D , <. f , E >. >. ) ) )
82 cgr3permute1 
 |-  ( ( 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 , <. C , B >. >. Cgr3 <. D , <. f , E >. >. ) )
83 18 40 21 22 28 82 syl113anc 
 |-  ( ( ( 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 , <. C , B >. >. Cgr3 <. D , <. f , E >. >. ) )
84 83 biimprd 
 |-  ( ( ( 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 , <. C , B >. >. Cgr3 <. D , <. f , E >. >. -> <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
85 84 adantld 
 |-  ( ( ( 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 ) ) -> ( ( f Btwn <. D , E >. /\ <. A , <. C , B >. >. Cgr3 <. D , <. f , E >. >. ) -> <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
86 85 reximdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( E. f e. ( EE ` N ) ( f Btwn <. D , E >. /\ <. A , <. C , B >. >. Cgr3 <. D , <. f , E >. >. ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
87 81 86 syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , B >. Cgr <. D , E >. ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
88 87 expd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> ( <. A , B >. Cgr <. D , E >. -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) ) )
89 48 79 88 3jaod 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) -> ( <. A , B >. Cgr <. D , E >. -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) ) )
90 89 impd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) /\ <. A , B >. Cgr <. D , E >. ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )
91 3 90 sylbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( A Colinear <. B , C >. /\ <. A , B >. Cgr <. D , E >. ) -> E. f e. ( EE ` N ) <. A , <. B , C >. >. Cgr3 <. D , <. E , f >. >. ) )