Metamath Proof Explorer

Theorem btwnexch3

Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

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

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 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C 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 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
5 btwncom 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. A , D >. <-> C Btwn <. D , A >. ) )
6 1 2 3 4 5 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. A , D >. <-> C Btwn <. D , A >. ) )
7 simp2r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
8 btwncom 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
9 1 7 3 2 8 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
10 6 9 anbi12d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , D >. /\ B Btwn <. A , C >. ) <-> ( C Btwn <. D , A >. /\ B Btwn <. C , A >. ) ) )
11 axpasch 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( C Btwn <. D , A >. /\ B Btwn <. C , A >. ) -> E. x e. ( EE ` N ) ( x Btwn <. C , C >. /\ x Btwn <. B , D >. ) ) )
12 1 4 2 3 2 7 11 syl132anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. D , A >. /\ B Btwn <. C , A >. ) -> E. x e. ( EE ` N ) ( x Btwn <. C , C >. /\ x Btwn <. B , D >. ) ) )
13 10 12 sylbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , D >. /\ B Btwn <. A , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. C , C >. /\ x Btwn <. B , D >. ) ) )
14 13 ancomsd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> E. x e. ( EE ` N ) ( x Btwn <. C , C >. /\ x Btwn <. B , D >. ) ) )
15 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
16 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
17 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> C e. ( EE ` N ) )
18 axbtwnid 
 |-  ( ( N e. NN /\ x e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( x Btwn <. C , C >. -> x = C ) )
19 15 16 17 18 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. C , C >. -> x = C ) )
20 breq1 
 |-  ( x = C -> ( x Btwn <. B , D >. <-> C Btwn <. B , D >. ) )
21 20 biimpd 
 |-  ( x = C -> ( x Btwn <. B , D >. -> C Btwn <. B , D >. ) )
22 19 21 syl6 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. C , C >. -> ( x Btwn <. B , D >. -> C Btwn <. B , D >. ) ) )
23 22 impd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. C , C >. /\ x Btwn <. B , D >. ) -> C Btwn <. B , D >. ) )
24 23 rexlimdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( x Btwn <. C , C >. /\ x Btwn <. B , D >. ) -> C Btwn <. B , D >. ) )
25 14 24 syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> C Btwn <. B , D >. ) )