Metamath Proof Explorer

Theorem btwndiff

Description: There is always a c distinct from B such that B lies between A and c . Theorem 3.14 of Schwabhauser p. 32. (Contributed by Scott Fenton, 24-Sep-2013)

Ref Expression
Assertion btwndiff 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ B =/= c ) )

Proof

Step Hyp Ref Expression
1 axlowdim1 
 |-  ( N e. NN -> E. u e. ( EE ` N ) E. v e. ( EE ` N ) u =/= v )
2 1 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> E. u e. ( EE ` N ) E. v e. ( EE ` N ) u =/= v )
3 simp11 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> N e. NN )
4 simp12 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> A e. ( EE ` N ) )
5 simp13 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> B e. ( EE ` N ) )
6 simp2l 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> u e. ( EE ` N ) )
7 simp2r 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> v e. ( EE ` N ) )
8 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) ) -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ <. B , c >. Cgr <. u , v >. ) )
9 3 4 5 6 7 8 syl122anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ <. B , c >. Cgr <. u , v >. ) )
10 simpl11 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> N e. NN )
11 simpl13 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> B e. ( EE ` N ) )
12 simpr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> c e. ( EE ` N ) )
13 simpl2l 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> u e. ( EE ` N ) )
14 simpl2r 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> v e. ( EE ` N ) )
15 cgrdegen 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) ) -> ( <. B , c >. Cgr <. u , v >. -> ( B = c <-> u = v ) ) )
16 10 11 12 13 14 15 syl122anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> ( <. B , c >. Cgr <. u , v >. -> ( B = c <-> u = v ) ) )
17 biimp 
 |-  ( ( B = c <-> u = v ) -> ( B = c -> u = v ) )
18 17 necon3d 
 |-  ( ( B = c <-> u = v ) -> ( u =/= v -> B =/= c ) )
19 18 com12 
 |-  ( u =/= v -> ( ( B = c <-> u = v ) -> B =/= c ) )
20 19 3ad2ant3 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> ( ( B = c <-> u = v ) -> B =/= c ) )
21 20 adantr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> ( ( B = c <-> u = v ) -> B =/= c ) )
22 16 21 syld 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> ( <. B , c >. Cgr <. u , v >. -> B =/= c ) )
23 22 anim2d 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) /\ c e. ( EE ` N ) ) -> ( ( B Btwn <. A , c >. /\ <. B , c >. Cgr <. u , v >. ) -> ( B Btwn <. A , c >. /\ B =/= c ) ) )
24 23 reximdva 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> ( E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ <. B , c >. Cgr <. u , v >. ) -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ B =/= c ) ) )
25 9 24 mpd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) /\ u =/= v ) -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ B =/= c ) )
26 25 3exp 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( u e. ( EE ` N ) /\ v e. ( EE ` N ) ) -> ( u =/= v -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ B =/= c ) ) ) )
27 26 rexlimdvv 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( E. u e. ( EE ` N ) E. v e. ( EE ` N ) u =/= v -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ B =/= c ) ) )
28 2 27 mpd 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> E. c e. ( EE ` N ) ( B Btwn <. A , c >. /\ B =/= c ) )