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→AASeg≤BC

Proof

Step Hyp Ref Expression
1 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N
2 btwntriv1 ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnBC
3 2 3adant3r1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnBC
4 cgrtriv ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→AACgrBB
5 4 3adant3r3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AACgrBB
6 breq1 ⊢y=B→yBtwnBC↔BBtwnBC
7 opeq2 ⊢y=B→By=BB
8 7 breq2d ⊢y=B→AACgrBy↔AACgrBB
9 6 8 anbi12d ⊢y=B→yBtwnBC∧AACgrBy↔BBtwnBC∧AACgrBB
10 9 rspcev ⊢B∈𝔼⁡N∧BBtwnBC∧AACgrBB→∃y∈𝔼⁡NyBtwnBC∧AACgrBy
11 1 3 5 10 syl12anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃y∈𝔼⁡NyBtwnBC∧AACgrBy
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→AASeg≤BC↔∃y∈𝔼⁡NyBtwnBC∧AACgrBy
16 12 13 13 1 14 15 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AASeg≤BC↔∃y∈𝔼⁡NyBtwnBC∧AACgrBy
17 11 16 mpbird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AASeg≤BC