Metamath Proof Explorer

Theorem xrmaxle

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

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

Proof

Step Hyp Ref Expression
1 xrmax1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> A <_ if ( A <_ B , B , A ) )
2 1 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> A <_ if ( A <_ B , B , A ) )
3 ifcl 
 |-  ( ( B e. RR* /\ A e. RR* ) -> if ( A <_ B , B , A ) e. RR* )
4 3 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> if ( A <_ B , B , A ) e. RR* )
5 4 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> if ( A <_ B , B , A ) e. RR* )
6 xrletr 
 |-  ( ( A e. RR* /\ if ( A <_ B , B , A ) e. RR* /\ C e. RR* ) -> ( ( A <_ if ( A <_ B , B , A ) /\ if ( A <_ B , B , A ) <_ C ) -> A <_ C ) )
7 5 6 syld3an2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ if ( A <_ B , B , A ) /\ if ( A <_ B , B , A ) <_ C ) -> A <_ C ) )
8 2 7 mpand 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( if ( A <_ B , B , A ) <_ C -> A <_ C ) )
9 xrmax2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> B <_ if ( A <_ B , B , A ) )
10 9 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> B <_ if ( A <_ B , B , A ) )
11 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> B e. RR* )
12 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> C e. RR* )
13 xrletr 
 |-  ( ( B e. RR* /\ if ( A <_ B , B , A ) e. RR* /\ C e. RR* ) -> ( ( B <_ if ( A <_ B , B , A ) /\ if ( A <_ B , B , A ) <_ C ) -> B <_ C ) )
14 11 5 12 13 syl3anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( B <_ if ( A <_ B , B , A ) /\ if ( A <_ B , B , A ) <_ C ) -> B <_ C ) )
15 10 14 mpand 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( if ( A <_ B , B , A ) <_ C -> B <_ C ) )
16 8 15 jcad 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( if ( A <_ B , B , A ) <_ C -> ( A <_ C /\ B <_ C ) ) )
17 breq1 
 |-  ( B = if ( A <_ B , B , A ) -> ( B <_ C <-> if ( A <_ B , B , A ) <_ C ) )
18 breq1 
 |-  ( A = if ( A <_ B , B , A ) -> ( A <_ C <-> if ( A <_ B , B , A ) <_ C ) )
19 17 18 ifboth 
 |-  ( ( B <_ C /\ A <_ C ) -> if ( A <_ B , B , A ) <_ C )
20 19 ancoms 
 |-  ( ( A <_ C /\ B <_ C ) -> if ( A <_ B , B , A ) <_ C )
21 16 20 impbid1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( if ( A <_ B , B , A ) <_ C <-> ( A <_ C /\ B <_ C ) ) )