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 * B * C * A < if B C B C A < B A < C

Proof

Step Hyp Ref Expression
1 xrmin1 B * C * if B C B C B
2 1 3adant1 A * B * C * if B C B C B
3 simp1 A * B * C * A *
4 ifcl B * C * if B C B C *
5 4 3adant1 A * B * C * if B C B C *
6 simp2 A * B * C * B *
7 xrltletr A * if B C B C * B * A < if B C B C if B C B C B A < B
8 3 5 6 7 syl3anc A * B * C * A < if B C B C if B C B C B A < B
9 2 8 mpan2d A * B * C * A < if B C B C A < B
10 xrmin2 B * C * if B C B C C
11 10 3adant1 A * B * C * if B C B C C
12 xrltletr A * if B C B C * C * A < if B C B C if B C B C C A < C
13 5 12 syld3an2 A * B * C * A < if B C B C if B C B C C A < C
14 11 13 mpan2d A * B * C * A < if B C B C A < C
15 9 14 jcad A * B * C * 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 * B * C * A < if B C B C A < B A < C