Metamath Proof Explorer

Theorem btwnconn3

Description: Inner connectivity law for betweenness. Theorem 5.3 of Schwabhauser p. 41. (Contributed by Scott Fenton, 9-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
2 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
3 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
4 btwndiff 
 |-  ( ( N e. NN /\ D e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> E. p e. ( EE ` N ) ( A Btwn <. D , p >. /\ A =/= p ) )
5 1 2 3 4 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. p e. ( EE ` N ) ( A Btwn <. D , p >. /\ A =/= p ) )
6 simprlr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> A =/= p )
7 6 necomd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> p =/= A )
8 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> N e. NN )
9 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> A e. ( EE ` N ) )
10 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> B e. ( EE ` N ) )
11 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> p e. ( EE ` N ) )
12 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> D e. ( EE ` N ) )
13 simprrl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> B Btwn <. A , D >. )
14 8 10 9 12 13 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> B Btwn <. D , A >. )
15 simprll 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> A Btwn <. D , p >. )
16 8 12 10 9 11 14 15 btwnexch3and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> A Btwn <. B , p >. )
17 8 9 10 11 16 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> A Btwn <. p , B >. )
18 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> C e. ( EE ` N ) )
19 simprrr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> C Btwn <. A , D >. )
20 8 18 9 12 19 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> C Btwn <. D , A >. )
21 8 12 18 9 11 20 15 btwnexch3and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> A Btwn <. C , p >. )
22 8 9 18 11 21 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> A Btwn <. p , C >. )
23 7 17 22 3jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) /\ ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) ) -> ( p =/= A /\ A Btwn <. p , B >. /\ A Btwn <. p , C >. ) )
24 23 ex 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> ( ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) -> ( p =/= A /\ A Btwn <. p , B >. /\ A Btwn <. p , C >. ) ) )
25 btwnconn2 
 |-  ( ( N e. NN /\ ( p e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( p =/= A /\ A Btwn <. p , B >. /\ A Btwn <. p , C >. ) -> ( B Btwn <. A , C >. \/ C Btwn <. A , B >. ) ) )
26 8 11 9 10 18 25 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> ( ( p =/= A /\ A Btwn <. p , B >. /\ A Btwn <. p , C >. ) -> ( B Btwn <. A , C >. \/ C Btwn <. A , B >. ) ) )
27 24 26 syld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> ( ( ( A Btwn <. D , p >. /\ A =/= p ) /\ ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) ) -> ( B Btwn <. A , C >. \/ C Btwn <. A , B >. ) ) )
28 27 expd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ p e. ( EE ` N ) ) -> ( ( A Btwn <. D , p >. /\ A =/= p ) -> ( ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) -> ( B Btwn <. A , C >. \/ C Btwn <. A , B >. ) ) ) )
29 28 rexlimdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. p e. ( EE ` N ) ( A Btwn <. D , p >. /\ A =/= p ) -> ( ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) -> ( B Btwn <. A , C >. \/ C Btwn <. A , B >. ) ) ) )
30 5 29 mpd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , D >. /\ C Btwn <. A , D >. ) -> ( B Btwn <. A , C >. \/ C Btwn <. A , B >. ) ) )