Metamath Proof Explorer

Theorem segconeq

Description: Two points that satisfy the conclusion of axsegcon are identical. Uniqueness portion of Theorem 2.12 of Schwabhauser p. 29. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion segconeq 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> X = Y ) )

Proof

Step Hyp Ref Expression
1 simpr2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> A Btwn <. Q , X >. )
2 1 1 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( A Btwn <. Q , X >. /\ A Btwn <. Q , X >. ) )
3 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> N e. NN )
4 simpl31 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> Q e. ( EE ` N ) )
5 simpl21 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> A e. ( EE ` N ) )
6 3 4 5 cgrrflxd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. Q , A >. Cgr <. Q , A >. )
7 simpl32 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> X e. ( EE ` N ) )
8 3 5 7 cgrrflxd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. A , X >. Cgr <. A , X >. )
9 6 8 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( <. Q , A >. Cgr <. Q , A >. /\ <. A , X >. Cgr <. A , X >. ) )
10 simpl33 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> Y e. ( EE ` N ) )
11 4 5 10 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) /\ Y e. ( EE ` N ) ) )
12 4 5 7 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) /\ X e. ( EE ` N ) ) )
13 3 11 12 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) /\ Y e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) /\ X e. ( EE ` N ) ) ) )
14 simpr3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> A Btwn <. Q , Y >. )
15 14 1 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( A Btwn <. Q , Y >. /\ A Btwn <. Q , X >. ) )
16 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> B e. ( EE ` N ) )
17 simpl23 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> C e. ( EE ` N ) )
18 simpr3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. A , Y >. Cgr <. B , C >. )
19 cgrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ Y e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , Y >. Cgr <. B , C >. <-> <. B , C >. Cgr <. A , Y >. ) )
20 3 5 10 16 17 19 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( <. A , Y >. Cgr <. B , C >. <-> <. B , C >. Cgr <. A , Y >. ) )
21 18 20 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. B , C >. Cgr <. A , Y >. )
22 simpr2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. A , X >. Cgr <. B , C >. )
23 cgrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ X e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , X >. Cgr <. B , C >. <-> <. B , C >. Cgr <. A , X >. ) )
24 3 5 7 16 17 23 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( <. A , X >. Cgr <. B , C >. <-> <. B , C >. Cgr <. A , X >. ) )
25 22 24 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. B , C >. Cgr <. A , X >. )
26 3 16 17 5 10 5 7 21 25 cgrtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. A , Y >. Cgr <. A , X >. )
27 15 6 26 jca32 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( ( A Btwn <. Q , Y >. /\ A Btwn <. Q , X >. ) /\ ( <. Q , A >. Cgr <. Q , A >. /\ <. A , Y >. Cgr <. A , X >. ) ) )
28 cgrextend 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) /\ Y e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ A e. ( EE ` N ) /\ X e. ( EE ` N ) ) ) -> ( ( ( A Btwn <. Q , Y >. /\ A Btwn <. Q , X >. ) /\ ( <. Q , A >. Cgr <. Q , A >. /\ <. A , Y >. Cgr <. A , X >. ) ) -> <. Q , Y >. Cgr <. Q , X >. ) )
29 13 27 28 sylc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> <. Q , Y >. Cgr <. Q , X >. )
30 29 26 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( <. Q , Y >. Cgr <. Q , X >. /\ <. A , Y >. Cgr <. A , X >. ) )
31 2 9 30 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) /\ ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) ) -> ( ( A Btwn <. Q , X >. /\ A Btwn <. Q , X >. ) /\ ( <. Q , A >. Cgr <. Q , A >. /\ <. A , X >. Cgr <. A , X >. ) /\ ( <. Q , Y >. Cgr <. Q , X >. /\ <. A , Y >. Cgr <. A , X >. ) ) )
32 31 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> ( ( A Btwn <. Q , X >. /\ A Btwn <. Q , X >. ) /\ ( <. Q , A >. Cgr <. Q , A >. /\ <. A , X >. Cgr <. A , X >. ) /\ ( <. Q , Y >. Cgr <. Q , X >. /\ <. A , Y >. Cgr <. A , X >. ) ) ) )
33 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> N e. NN )
34 simp31 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> Q e. ( EE ` N ) )
35 simp21 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
36 simp32 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> X e. ( EE ` N ) )
37 simp33 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> Y e. ( EE ` N ) )
38 brofs 
 |-  ( ( ( N e. NN /\ Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( X e. ( EE ` N ) /\ Y e. ( EE ` N ) /\ Q e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ X e. ( EE ` N ) /\ X e. ( EE ` N ) ) ) -> ( <. <. Q , A >. , <. X , Y >. >. OuterFiveSeg <. <. Q , A >. , <. X , X >. >. <-> ( ( A Btwn <. Q , X >. /\ A Btwn <. Q , X >. ) /\ ( <. Q , A >. Cgr <. Q , A >. /\ <. A , X >. Cgr <. A , X >. ) /\ ( <. Q , Y >. Cgr <. Q , X >. /\ <. A , Y >. Cgr <. A , X >. ) ) ) )
39 33 34 35 36 37 34 35 36 36 38 syl333anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( <. <. Q , A >. , <. X , Y >. >. OuterFiveSeg <. <. Q , A >. , <. X , X >. >. <-> ( ( A Btwn <. Q , X >. /\ A Btwn <. Q , X >. ) /\ ( <. Q , A >. Cgr <. Q , A >. /\ <. A , X >. Cgr <. A , X >. ) /\ ( <. Q , Y >. Cgr <. Q , X >. /\ <. A , Y >. Cgr <. A , X >. ) ) ) )
40 32 39 sylibrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> <. <. Q , A >. , <. X , Y >. >. OuterFiveSeg <. <. Q , A >. , <. X , X >. >. ) )
41 simp1 
 |-  ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> Q =/= A )
42 41 a1i 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> Q =/= A ) )
43 40 42 jcad 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> ( <. <. Q , A >. , <. X , Y >. >. OuterFiveSeg <. <. Q , A >. , <. X , X >. >. /\ Q =/= A ) ) )
44 5segofs 
 |-  ( ( ( N e. NN /\ Q e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( X e. ( EE ` N ) /\ Y e. ( EE ` N ) /\ Q e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ X e. ( EE ` N ) /\ X e. ( EE ` N ) ) ) -> ( ( <. <. Q , A >. , <. X , Y >. >. OuterFiveSeg <. <. Q , A >. , <. X , X >. >. /\ Q =/= A ) -> <. X , Y >. Cgr <. X , X >. ) )
45 33 34 35 36 37 34 35 36 36 44 syl333anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( <. <. Q , A >. , <. X , Y >. >. OuterFiveSeg <. <. Q , A >. , <. X , X >. >. /\ Q =/= A ) -> <. X , Y >. Cgr <. X , X >. ) )
46 axcgrid 
 |-  ( ( N e. NN /\ ( X e. ( EE ` N ) /\ Y e. ( EE ` N ) /\ X e. ( EE ` N ) ) ) -> ( <. X , Y >. Cgr <. X , X >. -> X = Y ) )
47 33 36 37 36 46 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( <. X , Y >. Cgr <. X , X >. -> X = Y ) )
48 43 45 47 3syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( Q e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> ( ( Q =/= A /\ ( A Btwn <. Q , X >. /\ <. A , X >. Cgr <. B , C >. ) /\ ( A Btwn <. Q , Y >. /\ <. A , Y >. Cgr <. B , C >. ) ) -> X = Y ) )