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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) )

Proof

Step	Hyp	Ref	Expression
1		axlowdim1	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) 𝑢 ≠ 𝑣 )
2	1	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) 𝑢 ≠ 𝑣 )
3		simp11	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → 𝑁 ∈ ℕ )
4		simp12	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simp13	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
6		simp2l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) )
7		simp2r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) )
8		axsegcon	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ ) )
9	3 4 5 6 7 8	syl122anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ ) )
10		simpl11	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
11		simpl13	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
12		simpr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
13		simpl2l	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) )
14		simpl2r	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) )
15		cgrdegen	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) ) )
16	10 11 12 13 14 15	syl122anc	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) ) )
17		biimp	⊢ ( ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) → ( 𝐵 = 𝑐 → 𝑢 = 𝑣 ) )
18	17	necon3d	⊢ ( ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) → ( 𝑢 ≠ 𝑣 → 𝐵 ≠ 𝑐 ) )
19	18	com12	⊢ ( 𝑢 ≠ 𝑣 → ( ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) → 𝐵 ≠ 𝑐 ) )
20	19	3ad2ant3	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) → 𝐵 ≠ 𝑐 ) )
21	20	adantr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 = 𝑐 ↔ 𝑢 = 𝑣 ) → 𝐵 ≠ 𝑐 ) )
22	16 21	syld	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ → 𝐵 ≠ 𝑐 ) )
23	22	anim2d	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) ) )
24	23	reximdva	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑢 , 𝑣 ⟩ ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) ) )
25	9 24	mpd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑢 ≠ 𝑣 ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) )
26	25	3exp	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑢 ≠ 𝑣 → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) ) ) )
27	26	rexlimdvv	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) 𝑢 ≠ 𝑣 → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) ) )
28	2 27	mpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝐵 ≠ 𝑐 ) )