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