Metamath Proof Explorer

Theorem xrlemin

Description: Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion xrlemin 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ if ( B <_ C , B , C ) <-> ( A <_ B /\ A <_ C ) ) )

Proof

Step Hyp Ref Expression
1 xrmin1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> if ( B <_ C , B , C ) <_ B )
2 1 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> if ( B <_ C , B , C ) <_ B )
3 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> A e. RR* )
4 ifcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> if ( B <_ C , B , C ) e. RR* )
5 4 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> if ( B <_ C , B , C ) e. RR* )
6 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> B e. RR* )
7 xrletr 
 |-  ( ( A e. RR* /\ if ( B <_ C , B , C ) e. RR* /\ B e. RR* ) -> ( ( A <_ if ( B <_ C , B , C ) /\ if ( B <_ C , B , C ) <_ B ) -> A <_ B ) )
8 3 5 6 7 syl3anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ if ( B <_ C , B , C ) /\ if ( B <_ C , B , C ) <_ B ) -> A <_ B ) )
9 2 8 mpan2d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ if ( B <_ C , B , C ) -> A <_ B ) )
10 xrmin2 
 |-  ( ( B e. RR* /\ C e. RR* ) -> if ( B <_ C , B , C ) <_ C )
11 10 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> if ( B <_ C , B , C ) <_ C )
12 xrletr 
 |-  ( ( A e. RR* /\ if ( B <_ C , B , C ) e. RR* /\ C e. RR* ) -> ( ( A <_ if ( B <_ C , B , C ) /\ if ( B <_ C , B , C ) <_ C ) -> A <_ C ) )
13 5 12 syld3an2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ if ( B <_ C , B , C ) /\ if ( B <_ C , B , C ) <_ C ) -> A <_ C ) )
14 11 13 mpan2d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ if ( B <_ C , B , C ) -> A <_ C ) )
15 9 14 jcad 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ if ( B <_ C , B , C ) -> ( A <_ B /\ A <_ C ) ) )
16 breq2 
 |-  ( B = if ( B <_ C , B , C ) -> ( A <_ B <-> A <_ if ( B <_ C , B , C ) ) )
17 breq2 
 |-  ( C = if ( B <_ C , B , C ) -> ( A <_ C <-> A <_ if ( B <_ C , B , C ) ) )
18 16 17 ifboth 
 |-  ( ( A <_ B /\ A <_ C ) -> A <_ if ( B <_ C , B , C ) )
19 15 18 impbid1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ if ( B <_ C , B , C ) <-> ( A <_ B /\ A <_ C ) ) )