Theorem btwnsegle

Description: If B falls between A and C , then A B is no longer than A C . (Contributed by Scott Fenton, 16-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	btwnsegle	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		simplr2	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
2		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
3		simpl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
4		simpr1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simpr2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
6	3 4 5	cgrrflxd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
7	6	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
8		breq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
9		opeq2	⊢ ( 𝑥 = 𝐵 → ⟨ 𝐴 , 𝑥 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
10	9	breq2d	⊢ ( 𝑥 = 𝐵 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
11	8 10	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
12	11	rspcev	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) )
13	1 2 7 12	syl12anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) )
14		simpr3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
15		brsegle	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
16	3 4 5 4 14 15	syl122anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
17	16	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
18	13 17	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ )
19	18	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐴 , 𝐶 ⟩ ) )