Metamath Proof Explorer

Theorem xrmaxlt

Description: Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrmaxlt 
|- ( ( 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 xrlelttr 
 |-  ( ( 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 xrlelttr 
 |-  ( ( 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 ) ) )