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∈𝔼⁡NBBtwnAc∧B≠c

Proof

Step Hyp Ref Expression
1 axlowdim1 ⊢N∈ℕ→∃u∈𝔼⁡N∃v∈𝔼⁡Nu≠v
2 1 3ad2ant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃u∈𝔼⁡N∃v∈𝔼⁡Nu≠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∈𝔼⁡NBBtwnAc∧BcCgruv
9 3 4 5 6 7 8 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧u∈𝔼⁡N∧v∈𝔼⁡N∧u≠v→∃c∈𝔼⁡NBBtwnAc∧BcCgruv
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→BcCgruv→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→BcCgruv→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→BcCgruv→B≠c
23 22 anim2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧u∈𝔼⁡N∧v∈𝔼⁡N∧u≠v∧c∈𝔼⁡N→BBtwnAc∧BcCgruv→BBtwnAc∧B≠c
24 23 reximdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧u∈𝔼⁡N∧v∈𝔼⁡N∧u≠v→∃c∈𝔼⁡NBBtwnAc∧BcCgruv→∃c∈𝔼⁡NBBtwnAc∧B≠c
25 9 24 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧u∈𝔼⁡N∧v∈𝔼⁡N∧u≠v→∃c∈𝔼⁡NBBtwnAc∧B≠c
26 25 3exp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→u∈𝔼⁡N∧v∈𝔼⁡N→u≠v→∃c∈𝔼⁡NBBtwnAc∧B≠c
27 26 rexlimdvv ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃u∈𝔼⁡N∃v∈𝔼⁡Nu≠v→∃c∈𝔼⁡NBBtwnAc∧B≠c
28 2 27 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃c∈𝔼⁡NBBtwnAc∧B≠c