This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrltmin

Description: Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrltmin 
|- ( ( 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 xrltletr 
 |-  ( ( 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 xrltletr 
 |-  ( ( 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 ) ) )