Theorem btwnconn1lem11 32204

Description: Lemma for btwnconn1 32208. Now, we establish that D and Q are equidistant from C. (Contributed by Scott Fenton, 8-Oct-2013.)

Assertion

Ref

Expression

btwnconn1lem11

|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. D , C >.Cgr <. Q , C >. )

Proof of Theorem btwnconn1lem11

Step	Hyp	Ref	Expression
1		btwnconn1lem8 32201	. . . . 5 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. R , P >.Cgr <. E , d >. )
2		btwnconn1lem9 32202	. . . . 5 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. R , Q >.Cgr <. E , D >. )
3		btwnconn1lem10 32203	. . . . 5 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. d , D >.Cgr <. P , Q >. )
4	1, 2, 3	3jca 1242	. . . 4 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) )
5	4	adantr 481	. . 3 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d = E ) -> ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) )
6		simpr3r 1123	. . . . . . 7 |- ( ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) -> <. R , Q >.Cgr <. R , P >. )
7	6	adantl 482	. . . . . 6 |- ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) -> <. R , Q >.Cgr <. R , P >. )
8		simpr2r 1121	. . . . . . 7 |- ( ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) -> <. C , R >.Cgr <. C , E >. )
9	8	adantl 482	. . . . . 6 |- ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) -> <. C , R >.Cgr <. C , E >. )
10	7, 9	jca 554	. . . . 5 |- ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) -> ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) )
11		opeq2 4403	. . . . . . . . . . . 12 |- ( d = E -> <. C , d >. = <. C , E >. )
12	11	breq2d 4665	. . . . . . . . . . 11 |- ( d = E -> ( <. C , R >.Cgr <. C , d >. <-> <. C , R >.Cgr <. C , E >. ) )
13	12	anbi2d 740	. . . . . . . . . 10 |- ( d = E -> ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) <-> ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) ) )
14		opeq1 4402	. . . . . . . . . . . 12 |- ( d = E -> <. d , d >. = <. E , d >. )
15	14	breq2d 4665	. . . . . . . . . . 11 |- ( d = E -> ( <. R , P >.Cgr <. d , d >. <-> <. R , P >.Cgr <. E , d >. ) )
16		opeq1 4402	. . . . . . . . . . . 12 |- ( d = E -> <. d , D >. = <. E , D >. )
17	16	breq2d 4665	. . . . . . . . . . 11 |- ( d = E -> ( <. R , Q >.Cgr <. d , D >. <-> <. R , Q >.Cgr <. E , D >. ) )
18	15, 17	3anbi12d 1400	. . . . . . . . . 10 |- ( d = E -> ( ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) <-> ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) )
19	13, 18	anbi12d 747	. . . . . . . . 9 |- ( d = E -> ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) <-> ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) ) )
20	19	biimpar 502	. . . . . . . 8 |- ( ( d = E /\ ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) ) -> ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) )
21		simpr1 1067	. . . . . . . . . 10 |- ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> <. R , P >.Cgr <. d , d >. )
22		simp11 1091	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> N e. NN )
23		simp33 1099	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> R e. ( EE ` N ) )
24		simp31 1097	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
25		simp2r1 1163	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> d e. ( EE ` N ) )
26		axcgrid 25796	. . . . . . . . . . 11 |- ( ( N e. NN /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. R , P >.Cgr <. d , d >. -> R = P ) )
27	22, 23, 24, 25, 26	syl13anc 1328	. . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. R , P >.Cgr <. d , d >. -> R = P ) )
28	21, 27	syl5 34	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> R = P ) )
29		opeq1 4402	. . . . . . . . . . . . . . 15 |- ( R = P -> <. R , Q >. = <. P , Q >. )
30		opeq1 4402	. . . . . . . . . . . . . . 15 |- ( R = P -> <. R , P >. = <. P , P >. )
31	29, 30	breq12d 4666	. . . . . . . . . . . . . 14 |- ( R = P -> ( <. R , Q >.Cgr <. R , P >. <-> <. P , Q >.Cgr <. P , P >. ) )
32		opeq2 4403	. . . . . . . . . . . . . . 15 |- ( R = P -> <. C , R >. = <. C , P >. )
33	32	breq1d 4663	. . . . . . . . . . . . . 14 |- ( R = P -> ( <. C , R >.Cgr <. C , d >. <-> <. C , P >.Cgr <. C , d >. ) )
34	31, 33	anbi12d 747	. . . . . . . . . . . . 13 |- ( R = P -> ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) <-> ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) ) )
35	30	breq1d 4663	. . . . . . . . . . . . . 14 |- ( R = P -> ( <. R , P >.Cgr <. d , d >. <-> <. P , P >.Cgr <. d , d >. ) )
36	29	breq1d 4663	. . . . . . . . . . . . . 14 |- ( R = P -> ( <. R , Q >.Cgr <. d , D >. <-> <. P , Q >.Cgr <. d , D >. ) )
37	35, 36	3anbi12d 1400	. . . . . . . . . . . . 13 |- ( R = P -> ( ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) <-> ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) )
38	34, 37	anbi12d 747	. . . . . . . . . . . 12 |- ( R = P -> ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) <-> ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) ) )
39	38	biimpac 503	. . . . . . . . . . 11 |- ( ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) /\ R = P ) -> ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) )
40		simpll 790	. . . . . . . . . . . . 13 |- ( ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> <. P , Q >.Cgr <. P , P >. )
41		simp32 1098	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> Q e. ( EE ` N ) )
42		axcgrid 25796	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( <. P , Q >.Cgr <. P , P >. -> P = Q ) )
43	22, 24, 41, 24, 42	syl13anc 1328	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. P , Q >.Cgr <. P , P >. -> P = Q ) )
44	40, 43	syl5 34	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> P = Q ) )
45		simprlr 803	. . . . . . . . . . . . . . . 16 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> <. C , P >.Cgr <. C , d >. )
46		simpr3 1069	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) -> <. d , D >.Cgr <. P , P >. )
47		simp2l2 1161	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
48		axcgrid 25796	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. NN /\ ( d e. ( EE ` N ) /\ D e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( <. d , D >.Cgr <. P , P >. -> d = D ) )
49	22, 25, 47, 24, 48	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. d , D >.Cgr <. P , P >. -> d = D ) )
50	46, 49	syl5 34	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) -> d = D ) )
51	50	imp 445	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> d = D )
52	51	opeq2d 4409	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> <. C , d >. = <. C , D >. )
53	52	breq2d 4665	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> ( <. C , P >.Cgr <. C , d >. <-> <. C , P >.Cgr <. C , D >. ) )
54		simp2l1 1160	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
55		cgrcomlr 32105	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , P >.Cgr <. C , D >. <-> <. P , C >.Cgr <. D , C >. ) )
56	22, 54, 24, 54, 47, 55	syl122anc 1335	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. C , P >.Cgr <. C , D >. <-> <. P , C >.Cgr <. D , C >. ) )
57		cgrcom 32097	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. P , C >.Cgr <. D , C >. <-> <. D , C >.Cgr <. P , C >. ) )
58	22, 24, 54, 47, 54, 57	syl122anc 1335	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. P , C >.Cgr <. D , C >. <-> <. D , C >.Cgr <. P , C >. ) )
59	56, 58	bitrd 268	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. C , P >.Cgr <. C , D >. <-> <. D , C >.Cgr <. P , C >. ) )
60	59	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> ( <. C , P >.Cgr <. C , D >. <-> <. D , C >.Cgr <. P , C >. ) )
61	53, 60	bitrd 268	. . . . . . . . . . . . . . . 16 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> ( <. C , P >.Cgr <. C , d >. <-> <. D , C >.Cgr <. P , C >. ) )
62	45, 61	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) ) -> <. D , C >.Cgr <. P , C >. )
63	62	ex 450	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) -> <. D , C >.Cgr <. P , C >. ) )
64		opeq2 4403	. . . . . . . . . . . . . . . . . 18 |- ( P = Q -> <. P , P >. = <. P , Q >. )
65	64	breq1d 4663	. . . . . . . . . . . . . . . . 17 |- ( P = Q -> ( <. P , P >.Cgr <. P , P >. <-> <. P , Q >.Cgr <. P , P >. ) )
66	65	anbi1d 741	. . . . . . . . . . . . . . . 16 |- ( P = Q -> ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) <-> ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) ) )
67	64	breq1d 4663	. . . . . . . . . . . . . . . . 17 |- ( P = Q -> ( <. P , P >.Cgr <. d , D >. <-> <. P , Q >.Cgr <. d , D >. ) )
68	64	breq2d 4665	. . . . . . . . . . . . . . . . 17 |- ( P = Q -> ( <. d , D >.Cgr <. P , P >. <-> <. d , D >.Cgr <. P , Q >. ) )
69	67, 68	3anbi23d 1402	. . . . . . . . . . . . . . . 16 |- ( P = Q -> ( ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) <-> ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) )
70	66, 69	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( P = Q -> ( ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) <-> ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) ) )
71		opeq1 4402	. . . . . . . . . . . . . . . 16 |- ( P = Q -> <. P , C >. = <. Q , C >. )
72	71	breq2d 4665	. . . . . . . . . . . . . . 15 |- ( P = Q -> ( <. D , C >.Cgr <. P , C >. <-> <. D , C >.Cgr <. Q , C >. ) )
73	70, 72	imbi12d 334	. . . . . . . . . . . . . 14 |- ( P = Q -> ( ( ( ( <. P , P >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , P >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , P >. ) ) -> <. D , C >.Cgr <. P , C >. ) <-> ( ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> <. D , C >.Cgr <. Q , C >. ) ) )
74	63, 73	syl5ibcom 235	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( P = Q -> ( ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> <. D , C >.Cgr <. Q , C >. ) ) )
75	74	com23 86	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> ( P = Q -> <. D , C >.Cgr <. Q , C >. ) ) )
76	44, 75	mpdd 43	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. P , Q >.Cgr <. P , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( <. P , P >.Cgr <. d , d >. /\ <. P , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> <. D , C >.Cgr <. Q , C >. ) )
77	39, 76	syl5 34	. . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) /\ R = P ) -> <. D , C >.Cgr <. Q , C >. ) )
78	77	expd 452	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> ( R = P -> <. D , C >.Cgr <. Q , C >. ) ) )
79	28, 78	mpdd 43	. . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , d >. ) /\ ( <. R , P >.Cgr <. d , d >. /\ <. R , Q >.Cgr <. d , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) -> <. D , C >.Cgr <. Q , C >. ) )
80	20, 79	syl5 34	. . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( d = E /\ ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) ) ) -> <. D , C >.Cgr <. Q , C >. ) )
81	80	exp4d 637	. . . . . 6 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( d = E -> ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) -> ( ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) -> <. D , C >.Cgr <. Q , C >. ) ) ) )
82	81	com23 86	. . . . 5 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( <. R , Q >.Cgr <. R , P >. /\ <. C , R >.Cgr <. C , E >. ) -> ( d = E -> ( ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) -> <. D , C >.Cgr <. Q , C >. ) ) ) )
83	10, 82	syl5 34	. . . 4 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) -> ( d = E -> ( ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) -> <. D , C >.Cgr <. Q , C >. ) ) ) )
84	83	imp31 448	. . 3 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d = E ) -> ( ( <. R , P >.Cgr <. E , d >. /\ <. R , Q >.Cgr <. E , D >. /\ <. d , D >.Cgr <. P , Q >. ) -> <. D , C >.Cgr <. Q , C >. ) )
85	5, 84	mpd 15	. 2 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d = E ) -> <. D , C >.Cgr <. Q , C >. )
86		simp2r3 1165	. . . . . 6 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
87		simprlr 803	. . . . . . 7 |- ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) -> E Btwn <. D , d >. )
88	87	adantl 482	. . . . . 6 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> E Btwn <. D , d >. )
89	22, 86, 47, 25, 88	btwncomand 32122	. . . . 5 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> E Btwn <. d , D >. )
90		cgrcomlr 32105	. . . . . . . . . 10 |- ( ( N e. NN /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. R , P >.Cgr <. E , d >. <-> <. P , R >.Cgr <. d , E >. ) )
91	22, 23, 24, 86, 25, 90	syl122anc 1335	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. R , P >.Cgr <. E , d >. <-> <. P , R >.Cgr <. d , E >. ) )
92		cgrcom 32097	. . . . . . . . . 10 |- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. P , R >.Cgr <. d , E >. <-> <. d , E >.Cgr <. P , R >. ) )
93	22, 24, 23, 25, 86, 92	syl122anc 1335	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. P , R >.Cgr <. d , E >. <-> <. d , E >.Cgr <. P , R >. ) )
94	91, 93	bitrd 268	. . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. R , P >.Cgr <. E , d >. <-> <. d , E >.Cgr <. P , R >. ) )
95	94	adantr 481	. . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( <. R , P >.Cgr <. E , d >. <-> <. d , E >.Cgr <. P , R >. ) )
96	1, 95	mpbid 222	. . . . . 6 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. d , E >.Cgr <. P , R >. )
97	22, 23, 41, 86, 47, 2	cgrcomand 32098	. . . . . 6 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. E , D >.Cgr <. R , Q >. )
98		brcgr3 32153	. . . . . . . 8 |- ( ( N e. NN /\ ( d e. ( EE ` N ) /\ E e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ R e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. <-> ( <. d , E >.Cgr <. P , R >. /\ <. d , D >.Cgr <. P , Q >. /\ <. E , D >.Cgr <. R , Q >. ) ) )
99	22, 25, 86, 47, 24, 23, 41, 98	syl133anc 1349	. . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. <-> ( <. d , E >.Cgr <. P , R >. /\ <. d , D >.Cgr <. P , Q >. /\ <. E , D >.Cgr <. R , Q >. ) ) )
100	99	adantr 481	. . . . . 6 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. <-> ( <. d , E >.Cgr <. P , R >. /\ <. d , D >.Cgr <. P , Q >. /\ <. E , D >.Cgr <. R , Q >. ) ) )
101	96, 3, 97, 100	mpbir3and 1245	. . . . 5 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. )
102		simpr1r 1119	. . . . . . . 8 |- ( ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) -> <. C , P >.Cgr <. C , d >. )
103	102	ad2antll 765	. . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. C , P >.Cgr <. C , d >. )
104		cgrcomlr 32105	. . . . . . . . . 10 |- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. C , P >.Cgr <. C , d >. <-> <. P , C >.Cgr <. d , C >. ) )
105	22, 54, 24, 54, 25, 104	syl122anc 1335	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. C , P >.Cgr <. C , d >. <-> <. P , C >.Cgr <. d , C >. ) )
106		cgrcom 32097	. . . . . . . . . 10 |- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. P , C >.Cgr <. d , C >. <-> <. d , C >.Cgr <. P , C >. ) )
107	22, 24, 54, 25, 54, 106	syl122anc 1335	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. P , C >.Cgr <. d , C >. <-> <. d , C >.Cgr <. P , C >. ) )
108	105, 107	bitrd 268	. . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. C , P >.Cgr <. C , d >. <-> <. d , C >.Cgr <. P , C >. ) )
109	108	adantr 481	. . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( <. C , P >.Cgr <. C , d >. <-> <. d , C >.Cgr <. P , C >. ) )
110	103, 109	mpbid 222	. . . . . 6 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. d , C >.Cgr <. P , C >. )
111	8	ad2antll 765	. . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. C , R >.Cgr <. C , E >. )
112		cgrcomlr 32105	. . . . . . . . . 10 |- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. C , R >.Cgr <. C , E >. <-> <. R , C >.Cgr <. E , C >. ) )
113	22, 54, 23, 54, 86, 112	syl122anc 1335	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. C , R >.Cgr <. C , E >. <-> <. R , C >.Cgr <. E , C >. ) )
114		cgrcom 32097	. . . . . . . . . 10 |- ( ( N e. NN /\ ( R e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. R , C >.Cgr <. E , C >. <-> <. E , C >.Cgr <. R , C >. ) )
115	22, 23, 54, 86, 54, 114	syl122anc 1335	. . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. R , C >.Cgr <. E , C >. <-> <. E , C >.Cgr <. R , C >. ) )
116	113, 115	bitrd 268	. . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( <. C , R >.Cgr <. C , E >. <-> <. E , C >.Cgr <. R , C >. ) )
117	116	adantr 481	. . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( <. C , R >.Cgr <. C , E >. <-> <. E , C >.Cgr <. R , C >. ) )
118	111, 117	mpbid 222	. . . . . 6 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. E , C >.Cgr <. R , C >. )
119	110, 118	jca 554	. . . . 5 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) )
120	89, 101, 119	3jca 1242	. . . 4 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) )
121	120	adantr 481	. . 3 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d =/= E ) -> ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) )
122		simpr 477	. . 3 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d =/= E ) -> d =/= E )
123		brofs2 32184	. . . . . . 7 |- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. <. d , E >. , <. D , C >. >. OuterFiveSeg <. <. P , R >. , <. Q , C >. >. <-> ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) ) )
124	123	anbi1d 741	. . . . . 6 |- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( <. <. d , E >. , <. D , C >. >. OuterFiveSeg <. <. P , R >. , <. Q , C >. >. /\ d =/= E ) <-> ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) /\ d =/= E ) ) )
125		5segofs 32113	. . . . . 6 |- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( <. <. d , E >. , <. D , C >. >. OuterFiveSeg <. <. P , R >. , <. Q , C >. >. /\ d =/= E ) -> <. D , C >.Cgr <. Q , C >. ) )
126	124, 125	sylbird 250	. . . . 5 |- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) /\ d =/= E ) -> <. D , C >.Cgr <. Q , C >. ) )
127	22, 25, 86, 47, 54, 24, 23, 41, 54, 126	syl333anc 1358	. . . 4 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) /\ d =/= E ) -> <. D , C >.Cgr <. Q , C >. ) )
128	127	ad2antrr 762	. . 3 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d =/= E ) -> ( ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >.Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >.Cgr <. P , C >. /\ <. E , C >.Cgr <. R , C >. ) ) /\ d =/= E ) -> <. D , C >.Cgr <. Q , C >. ) )
129	121, 122, 128	mp2and 715	. 2 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) /\ d =/= E ) -> <. D , C >.Cgr <. Q , C >. )
130	85, 129	pm2.61dane 2881	1 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >.Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >.Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >.Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >.Cgr <. D , B >. ) ) ) /\ ( ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) /\ ( ( C Btwn <. c , P >. /\ <. C , P >.Cgr <. C , d >. ) /\ ( C Btwn <. d , R >. /\ <. C , R >.Cgr <. C , E >. ) /\ ( R Btwn <. P , Q >. /\ <. R , Q >.Cgr <. R , P >. ) ) ) ) ) -> <. D , C >.Cgr <. Q , C >. )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   <.cop 4183   class class class wbr 4653   ` cfv 5888   NNcn 11020   EEcee 25768   Btwn cbtwn 25769  Cgrccgr 25770   OuterFiveSeg cofs 32089  Cgr3ccgr3 32143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-ee 25771  df-btwn 25772  df-cgr 25773  df-ofs 32090  df-ifs 32147  df-cgr3 32148

This theorem is referenced by:  btwnconn1lem12  32205