Metamath Proof Explorer

Theorem btwnconn1lem8

Description: Lemma for btwnconn1 . Now, we introduce the last three points used in the construction: P , Q , and R will turn out to be equal further down, and will provide us with the key to the final statement. We begin by establishing congruence of R P and E d . (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem8 
|- ( ( ( ( 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 >. )

Proof

Step Hyp Ref Expression
1 simpr2l 
 |-  ( ( ( 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 Btwn <. d , R >. )
2 1 ad2antll 
 |-  ( ( ( ( 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 Btwn <. d , R >. )
3 simpr1r 
 |-  ( ( ( 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 >. )
4 3 ad2antll 
 |-  ( ( ( ( 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 >. )
5 simp11 
 |-  ( ( ( 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 )
6 simp2l1 
 |-  ( ( ( 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 ) )
7 simp31 
 |-  ( ( ( 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 ) )
8 simp2r1 
 |-  ( ( ( 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 ) )
9 cgrcomlr 
 |-  ( ( 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 >. ) )
10 5 6 7 6 8 9 syl122anc 
 |-  ( ( ( 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 >. ) )
11 cgrcom 
 |-  ( ( 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 >. ) )
12 5 7 6 8 6 11 syl122anc 
 |-  ( ( ( 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 >. ) )
13 10 12 bitrd 
 |-  ( ( ( 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 >. ) )
14 13 adantr 
 |-  ( ( ( ( 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 >. ) )
15 4 14 mpbid 
 |-  ( ( ( ( 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 >. )
16 simp33 
 |-  ( ( ( 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 ) )
17 simp2r3 
 |-  ( ( ( 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 ) )
18 simp2l3 
 |-  ( ( ( 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 ) )
19 simpr1l 
 |-  ( ( ( 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 Btwn <. c , P >. )
20 19 ad2antll 
 |-  ( ( ( ( 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 Btwn <. c , P >. )
21 5 6 18 7 20 btwncomand 
 |-  ( ( ( ( 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 Btwn <. P , c >. )
22 simprll 
 |-  ( ( ( ( ( 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 <. C , c >. )
23 22 adantl 
 |-  ( ( ( ( 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 <. C , c >. )
24 btwnintr 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ c e. ( EE ` N ) ) ) -> ( ( C Btwn <. P , c >. /\ E Btwn <. C , c >. ) -> C Btwn <. P , E >. ) )
25 5 7 6 17 18 24 syl122anc 
 |-  ( ( ( 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 Btwn <. P , c >. /\ E Btwn <. C , c >. ) -> C Btwn <. P , E >. ) )
26 25 adantr 
 |-  ( ( ( ( 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 Btwn <. P , c >. /\ E Btwn <. C , c >. ) -> C Btwn <. P , E >. ) )
27 21 23 26 mp2and 
 |-  ( ( ( ( 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 Btwn <. P , E >. )
28 simpr2r 
 |-  ( ( ( 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 >. )
29 28 ad2antll 
 |-  ( ( ( ( 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 >. )
30 5 8 6 16 7 6 17 2 27 15 29 cgrextendand 
 |-  ( ( ( ( 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 , R >. Cgr <. P , E >. )
31 brcgr3 
 |-  ( ( N e. NN /\ ( d e. ( EE ` N ) /\ C e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ C e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. <-> ( <. d , C >. Cgr <. P , C >. /\ <. d , R >. Cgr <. P , E >. /\ <. C , R >. Cgr <. C , E >. ) ) )
32 5 8 6 16 7 6 17 31 syl133anc 
 |-  ( ( ( 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 , <. C , R >. >. Cgr3 <. P , <. C , E >. >. <-> ( <. d , C >. Cgr <. P , C >. /\ <. d , R >. Cgr <. P , E >. /\ <. C , R >. Cgr <. C , E >. ) ) )
33 32 adantr 
 |-  ( ( ( ( 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 , R >. >. Cgr3 <. P , <. C , E >. >. <-> ( <. d , C >. Cgr <. P , C >. /\ <. d , R >. Cgr <. P , E >. /\ <. C , R >. Cgr <. C , E >. ) ) )
34 15 30 29 33 mpbir3and 
 |-  ( ( ( ( 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 , R >. >. Cgr3 <. P , <. C , E >. >. )
35 5 8 7 cgrrflx2d 
 |-  ( ( ( 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 , P >. Cgr <. P , d >. )
36 35 adantr 
 |-  ( ( ( ( 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 , P >. Cgr <. P , d >. )
37 36 4 jca 
 |-  ( ( ( ( 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 , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) )
38 2 34 37 3jca 
 |-  ( ( ( ( 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 Btwn <. d , R >. /\ <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. /\ ( <. d , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) ) )
39 simp1 
 |-  ( ( ( 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 /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
40 simp2l 
 |-  ( ( ( 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 ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) )
41 simp2r 
 |-  ( ( ( 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 ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) )
42 39 40 41 3jca 
 |-  ( ( ( 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 /\ 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 ) ) ) )
43 simpl 
 |-  ( ( ( ( ( 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 >. ) ) ) ) -> ( ( ( 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 >. ) ) ) )
44 simprl 
 |-  ( ( ( ( ( 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 <. C , c >. /\ E Btwn <. D , d >. ) )
45 43 44 jca 
 |-  ( ( ( ( ( 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 >. ) ) ) ) -> ( ( ( ( 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 >. ) ) )
46 btwnconn1lem7 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( ( ( 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 =/= d )
47 42 45 46 syl2an 
 |-  ( ( ( ( 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 =/= d )
48 47 necomd 
 |-  ( ( ( ( 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 )
49 brofs2 
 |-  ( ( ( N e. NN /\ d e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ E e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. <. d , C >. , <. R , P >. >. OuterFiveSeg <. <. P , C >. , <. E , d >. >. <-> ( C Btwn <. d , R >. /\ <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. /\ ( <. d , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) ) ) )
50 49 anbi1d 
 |-  ( ( ( N e. NN /\ d e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ E e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( <. <. d , C >. , <. R , P >. >. OuterFiveSeg <. <. P , C >. , <. E , d >. >. /\ d =/= C ) <-> ( ( C Btwn <. d , R >. /\ <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. /\ ( <. d , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) ) /\ d =/= C ) ) )
51 5segofs 
 |-  ( ( ( N e. NN /\ d e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ E e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( <. <. d , C >. , <. R , P >. >. OuterFiveSeg <. <. P , C >. , <. E , d >. >. /\ d =/= C ) -> <. R , P >. Cgr <. E , d >. ) )
52 50 51 sylbird 
 |-  ( ( ( N e. NN /\ d e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ E e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( ( C Btwn <. d , R >. /\ <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. /\ ( <. d , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) ) /\ d =/= C ) -> <. R , P >. Cgr <. E , d >. ) )
53 5 8 6 16 7 7 6 17 8 52 syl333anc 
 |-  ( ( ( 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 Btwn <. d , R >. /\ <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. /\ ( <. d , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) ) /\ d =/= C ) -> <. R , P >. Cgr <. E , d >. ) )
54 53 adantr 
 |-  ( ( ( ( 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 Btwn <. d , R >. /\ <. d , <. C , R >. >. Cgr3 <. P , <. C , E >. >. /\ ( <. d , P >. Cgr <. P , d >. /\ <. C , P >. Cgr <. C , d >. ) ) /\ d =/= C ) -> <. R , P >. Cgr <. E , d >. ) )
55 38 48 54 mp2and 
 |-  ( ( ( ( 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 >. )