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