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 e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , A >. Seg<_ <. B , C >. )

Proof

Step Hyp Ref Expression
1 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
2 btwntriv1 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> B Btwn <. B , C >. )
3 2 3adant3r1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B Btwn <. B , C >. )
4 cgrtriv 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , A >. Cgr <. B , B >. )
5 4 3adant3r3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` 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 e. ( EE ` N ) /\ ( B Btwn <. B , C >. /\ <. A , A >. Cgr <. B , B >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. B , C >. /\ <. A , A >. Cgr <. B , y >. ) )
11 1 3 5 10 syl12anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. y e. ( EE ` N ) ( y Btwn <. B , C >. /\ <. A , A >. Cgr <. B , y >. ) )
12 simpl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
13 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
14 simpr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
15 brsegle 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , A >. Seg<_ <. B , C >. <-> E. y e. ( EE ` N ) ( y Btwn <. B , C >. /\ <. A , A >. Cgr <. B , y >. ) ) )
16 12 13 13 1 14 15 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , A >. Seg<_ <. B , C >. <-> E. y e. ( EE ` N ) ( y Btwn <. B , C >. /\ <. A , A >. Cgr <. B , y >. ) ) )
17 11 16 mpbird 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , A >. Seg<_ <. B , C >. )