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 A 𝔼 N B 𝔼 N c 𝔼 N B Btwn A c B c

Proof

Step Hyp Ref Expression
1 axlowdim1 N u 𝔼 N v 𝔼 N u v
2 1 3ad2ant1 N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v
3 simp11 N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v N
4 simp12 N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v A 𝔼 N
5 simp13 N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v B 𝔼 N
6 simp2l N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v u 𝔼 N
7 simp2r N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v v 𝔼 N
8 axsegcon N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N c 𝔼 N B Btwn A c B c Cgr u v
9 3 4 5 6 7 8 syl122anc N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B Btwn A c B c Cgr u v
10 simpl11 N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N N
11 simpl13 N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B 𝔼 N
12 simpr N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N c 𝔼 N
13 simpl2l N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N u 𝔼 N
14 simpl2r N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N v 𝔼 N
15 cgrdegen N B 𝔼 N c 𝔼 N u 𝔼 N v 𝔼 N B c Cgr u v B = c u = v
16 10 11 12 13 14 15 syl122anc N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 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 A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v B = c u = v B c
21 20 adantr N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B = c u = v B c
22 16 21 syld N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B c Cgr u v B c
23 22 anim2d N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B Btwn A c B c Cgr u v B Btwn A c B c
24 23 reximdva N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B Btwn A c B c Cgr u v c 𝔼 N B Btwn A c B c
25 9 24 mpd N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B Btwn A c B c
26 25 3exp N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B Btwn A c B c
27 26 rexlimdvv N A 𝔼 N B 𝔼 N u 𝔼 N v 𝔼 N u v c 𝔼 N B Btwn A c B c
28 2 27 mpd N A 𝔼 N B 𝔼 N c 𝔼 N B Btwn A c B c