Metamath Proof Explorer

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 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A A Seg ≤ B C

Proof

Step Hyp Ref Expression
1 simpr2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
2 btwntriv1 ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn B C
3 2 3adant3r1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn B C
4 cgrtriv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A A Cgr B B
5 4 3adant3r3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A A Cgr B B
6 breq1 ⊢ y = B → y Btwn B C ↔ B Btwn B C
7 opeq2 ⊢ y = B → B y = B B
8 7 breq2d ⊢ y = B → A A Cgr B y ↔ A A Cgr B B
9 6 8 anbi12d ⊢ y = B → y Btwn B C ∧ A A Cgr B y ↔ B Btwn B C ∧ A A Cgr B B
10 9 rspcev ⊢ B ∈ 𝔼 ⁡ N ∧ B Btwn B C ∧ A A Cgr B B → ∃ y ∈ 𝔼 ⁡ N y Btwn B C ∧ A A Cgr B y
11 1 3 5 10 syl12anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∃ y ∈ 𝔼 ⁡ N y Btwn B C ∧ A A Cgr B y
12 simpl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → N ∈ ℕ
13 simpr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
14 simpr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
15 brsegle ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A A Seg ≤ B C ↔ ∃ y ∈ 𝔼 ⁡ N y Btwn B C ∧ A A Cgr B y
16 12 13 13 1 14 15 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A A Seg ≤ B C ↔ ∃ y ∈ 𝔼 ⁡ N y Btwn B C ∧ A A Cgr B y
17 11 16 mpbird ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A A Seg ≤ B C