Theorem seglemin

Description: Any segment is at least as long as a degenerate segment. Theorem 5.11 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

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

Proof

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