Metamath Proof Explorer

Theorem segcon2

Description: Generalization of axsegcon . This time, we generate an endpoint for a segment on the ray Q A congruent to B C and starting at Q , as opposed to axsegcon , where the segment starts at A (Contributed by Scott Fenton, 14-Oct-2013) Remove unneeded inequality. (Revised by Scott Fenton, 15-Oct-2013)

Ref Expression
Assertion segcon2 
|- ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( A = Q -> ( A Btwn <. Q , x >. <-> Q Btwn <. Q , x >. ) )
2 1 orbi1d 
 |-  ( A = Q -> ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) <-> ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) ) )
3 2 anbi1d 
 |-  ( A = Q -> ( ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) <-> ( ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
4 3 rexbidv 
 |-  ( A = Q -> ( E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) <-> E. x e. ( EE ` N ) ( ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
5 simp1 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
6 simp2 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
7 6 ancomd 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A e. ( EE ` N ) /\ Q e. ( EE ` N ) ) )
8 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ Q e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> E. a e. ( EE ` N ) ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) )
9 5 7 7 8 syl3anc 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. a e. ( EE ` N ) ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) )
10 9 adantr 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A =/= Q ) -> E. a e. ( EE ` N ) ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) )
11 simpl1 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) -> N e. NN )
12 simpr 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) -> a e. ( EE ` N ) )
13 simpl2l 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) -> Q e. ( EE ` N ) )
14 simpl3 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) -> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
15 axsegcon 
 |-  ( ( N e. NN /\ ( a e. ( EE ` N ) /\ Q e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) )
16 11 12 13 14 15 syl121anc 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) -> E. x e. ( EE ` N ) ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) )
17 16 adantr 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) -> E. x e. ( EE ` N ) ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) )
18 anass 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) )
19 df-3an 
 |-  ( ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) <-> ( ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) /\ Q Btwn <. a , x >. ) )
20 simpr1 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> A =/= Q )
21 simpr2r 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> <. Q , a >. Cgr <. A , Q >. )
22 simpl1 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> N e. NN )
23 simpl2l 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> Q e. ( EE ` N ) )
24 simprl 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> a e. ( EE ` N ) )
25 simpl2r 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
26 cgrdegen 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ a e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( <. Q , a >. Cgr <. A , Q >. -> ( Q = a <-> A = Q ) ) )
27 22 23 24 25 23 26 syl122anc 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( <. Q , a >. Cgr <. A , Q >. -> ( Q = a <-> A = Q ) ) )
28 27 adantr 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> ( <. Q , a >. Cgr <. A , Q >. -> ( Q = a <-> A = Q ) ) )
29 21 28 mpd 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> ( Q = a <-> A = Q ) )
30 29 necon3bid 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> ( Q =/= a <-> A =/= Q ) )
31 20 30 mpbird 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> Q =/= a )
32 31 necomd 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> a =/= Q )
33 simpr2l 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> Q Btwn <. A , a >. )
34 22 23 25 24 33 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> Q Btwn <. a , A >. )
35 simpr3 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> Q Btwn <. a , x >. )
36 simprr 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> x e. ( EE ` N ) )
37 btwnconn2 
 |-  ( ( N e. NN /\ ( a e. ( EE ` N ) /\ Q e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( ( a =/= Q /\ Q Btwn <. a , A >. /\ Q Btwn <. a , x >. ) -> ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) ) )
38 22 24 23 25 36 37 syl122anc 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( ( a =/= Q /\ Q Btwn <. a , A >. /\ Q Btwn <. a , x >. ) -> ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) ) )
39 38 adantr 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> ( ( a =/= Q /\ Q Btwn <. a , A >. /\ Q Btwn <. a , x >. ) -> ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) ) )
40 32 34 35 39 mp3and 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) /\ Q Btwn <. a , x >. ) ) -> ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) )
41 19 40 sylan2br 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) /\ Q Btwn <. a , x >. ) ) -> ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) )
42 41 expr 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) -> ( Q Btwn <. a , x >. -> ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) ) )
43 42 anim1d 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( a e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) -> ( ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) -> ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
44 18 43 sylanb 
 |-  ( ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) -> ( ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) -> ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
45 44 an32s 
 |-  ( ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) /\ x e. ( EE ` N ) ) -> ( ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) -> ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
46 45 reximdva 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) -> ( E. x e. ( EE ` N ) ( Q Btwn <. a , x >. /\ <. Q , x >. Cgr <. B , C >. ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
47 17 46 mpd 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ ( A =/= Q /\ ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) ) ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )
48 47 expr 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ a e. ( EE ` N ) ) /\ A =/= Q ) -> ( ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
49 48 an32s 
 |-  ( ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A =/= Q ) /\ a e. ( EE ` N ) ) -> ( ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
50 49 rexlimdva 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A =/= Q ) -> ( E. a e. ( EE ` N ) ( Q Btwn <. A , a >. /\ <. Q , a >. Cgr <. A , Q >. ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) ) )
51 10 50 mpd 
 |-  ( ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A =/= Q ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )
52 simp2l 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> Q e. ( EE ` N ) )
53 simp3 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
54 axsegcon 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ Q e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( Q Btwn <. Q , x >. /\ <. Q , x >. Cgr <. B , C >. ) )
55 5 52 52 53 54 syl121anc 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( Q Btwn <. Q , x >. /\ <. Q , x >. Cgr <. B , C >. ) )
56 orc 
 |-  ( Q Btwn <. Q , x >. -> ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) )
57 56 anim1i 
 |-  ( ( Q Btwn <. Q , x >. /\ <. Q , x >. Cgr <. B , C >. ) -> ( ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )
58 57 reximi 
 |-  ( E. x e. ( EE ` N ) ( Q Btwn <. Q , x >. /\ <. Q , x >. Cgr <. B , C >. ) -> E. x e. ( EE ` N ) ( ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )
59 55 58 syl 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( ( Q Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )
60 4 51 59 pm2.61ne 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( ( A Btwn <. Q , x >. \/ x Btwn <. Q , A >. ) /\ <. Q , x >. Cgr <. B , C >. ) )