Metamath Proof Explorer

Theorem trisegint

Description: A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of Schwabhauser p. 33. (Contributed by Scott Fenton, 24-Sep-2013)

Ref Expression
Assertion trisegint 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) -> E. q e. ( EE ` N ) ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> N e. NN )
2 simpl23 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> C e. ( EE ` N ) )
3 simpl21 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> A e. ( EE ` N ) )
4 simpl31 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> D e. ( EE ` N ) )
5 2 3 4 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
6 simpl32 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> E e. ( EE ` N ) )
7 simpl33 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> P e. ( EE ` N ) )
8 6 7 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> ( E e. ( EE ` N ) /\ P e. ( EE ` N ) ) )
9 1 5 8 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) )
10 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> E Btwn <. D , C >. )
11 btwncom 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( E Btwn <. D , C >. <-> E Btwn <. C , D >. ) )
12 1 6 4 2 11 syl13anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> ( E Btwn <. D , C >. <-> E Btwn <. C , D >. ) )
13 10 12 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> E Btwn <. C , D >. )
14 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> P Btwn <. A , D >. )
15 13 14 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> ( E Btwn <. C , D >. /\ P Btwn <. A , D >. ) )
16 axpasch 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( E Btwn <. C , D >. /\ P Btwn <. A , D >. ) -> E. r e. ( EE ` N ) ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) )
17 9 15 16 sylc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> E. r e. ( EE ` N ) ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) )
18 simp1l1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> N e. NN )
19 6 3ad2ant1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> E e. ( EE ` N ) )
20 2 3ad2ant1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> C e. ( EE ` N ) )
21 3 3ad2ant1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> A e. ( EE ` N ) )
22 19 20 21 3jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> ( E e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
23 simp2 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> r e. ( EE ` N ) )
24 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> B e. ( EE ` N ) )
25 24 3ad2ant1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> B e. ( EE ` N ) )
26 23 25 jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> ( r e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
27 18 22 26 3jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> ( N e. NN /\ ( E e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( r e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) )
28 simp3l 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> r Btwn <. E , A >. )
29 simp1r1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> B Btwn <. A , C >. )
30 btwncom 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
31 18 25 21 20 30 syl13anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
32 29 31 mpbid 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> B Btwn <. C , A >. )
33 28 32 jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> ( r Btwn <. E , A >. /\ B Btwn <. C , A >. ) )
34 axpasch 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( r e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( r Btwn <. E , A >. /\ B Btwn <. C , A >. ) -> E. q e. ( EE ` N ) ( q Btwn <. r , C >. /\ q Btwn <. B , E >. ) ) )
35 27 33 34 sylc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> E. q e. ( EE ` N ) ( q Btwn <. r , C >. /\ q Btwn <. B , E >. ) )
36 simpll1 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) )
37 36 1 syl 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> N e. NN )
38 36 7 syl 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> P e. ( EE ` N ) )
39 simpll2 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> r e. ( EE ` N ) )
40 38 39 jca 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> ( P e. ( EE ` N ) /\ r e. ( EE ` N ) ) )
41 simplr 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> q e. ( EE ` N ) )
42 36 2 syl 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> C e. ( EE ` N ) )
43 41 42 jca 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> ( q e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
44 37 40 43 3jca 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> ( N e. NN /\ ( P e. ( EE ` N ) /\ r e. ( EE ` N ) ) /\ ( q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) )
45 simpl3r 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) -> r Btwn <. P , C >. )
46 45 anim1i 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> ( r Btwn <. P , C >. /\ q Btwn <. r , C >. ) )
47 btwnexch2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ r e. ( EE ` N ) ) /\ ( q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( r Btwn <. P , C >. /\ q Btwn <. r , C >. ) -> q Btwn <. P , C >. ) )
48 44 46 47 sylc 
 |-  ( ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) /\ q Btwn <. r , C >. ) -> q Btwn <. P , C >. )
49 48 ex 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) -> ( q Btwn <. r , C >. -> q Btwn <. P , C >. ) )
50 49 anim1d 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) /\ q e. ( EE ` N ) ) -> ( ( q Btwn <. r , C >. /\ q Btwn <. B , E >. ) -> ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) ) )
51 50 reximdva 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> ( E. q e. ( EE ` N ) ( q Btwn <. r , C >. /\ q Btwn <. B , E >. ) -> E. q e. ( EE ` N ) ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) ) )
52 35 51 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) /\ r e. ( EE ` N ) /\ ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) ) -> E. q e. ( EE ` N ) ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) )
53 52 rexlimdv3a 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> ( E. r e. ( EE ` N ) ( r Btwn <. E , A >. /\ r Btwn <. P , C >. ) -> E. q e. ( EE ` N ) ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) ) )
54 17 53 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) ) -> E. q e. ( EE ` N ) ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) )
55 54 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ E Btwn <. D , C >. /\ P Btwn <. A , D >. ) -> E. q e. ( EE ` N ) ( q Btwn <. P , C >. /\ q Btwn <. B , E >. ) ) )