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

Metamath Proof Explorer

Theorem mulge0

Description: The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion mulge0 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 e. RR )
2 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
3 1 2 leloed 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
4 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
5 1 4 leloed 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
6 3 5 anbi12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ 0 <_ B ) <-> ( ( 0 < A \/ 0 = A ) /\ ( 0 < B \/ 0 = B ) ) ) )
7 0red 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 e. RR )
8 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> A e. RR )
9 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> B e. RR )
10 8 9 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> ( A x. B ) e. RR )
11 mulgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )
12 11 an4s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A x. B ) )
13 7 10 12 ltled 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 <_ ( A x. B ) )
14 13 ex 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 <_ ( A x. B ) ) )
15 0re 
 |-  0 e. RR
16 leid 
 |-  ( 0 e. RR -> 0 <_ 0 )
17 15 16 ax-mp 
 |-  0 <_ 0
18 4 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
19 18 mul02d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 x. B ) = 0 )
20 17 19 breqtrrid 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 <_ ( 0 x. B ) )
21 oveq1 
 |-  ( 0 = A -> ( 0 x. B ) = ( A x. B ) )
22 21 breq2d 
 |-  ( 0 = A -> ( 0 <_ ( 0 x. B ) <-> 0 <_ ( A x. B ) ) )
23 20 22 syl5ibcom 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 = A -> 0 <_ ( A x. B ) ) )
24 23 adantrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 = A /\ 0 < B ) -> 0 <_ ( A x. B ) ) )
25 2 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
26 25 mul01d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. 0 ) = 0 )
27 17 26 breqtrrid 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 <_ ( A x. 0 ) )
28 oveq2 
 |-  ( 0 = B -> ( A x. 0 ) = ( A x. B ) )
29 28 breq2d 
 |-  ( 0 = B -> ( 0 <_ ( A x. 0 ) <-> 0 <_ ( A x. B ) ) )
30 27 29 syl5ibcom 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 = B -> 0 <_ ( A x. B ) ) )
31 30 adantld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 = B ) -> 0 <_ ( A x. B ) ) )
32 30 adantld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 = A /\ 0 = B ) -> 0 <_ ( A x. B ) ) )
33 14 24 31 32 ccased 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( 0 < A \/ 0 = A ) /\ ( 0 < B \/ 0 = B ) ) -> 0 <_ ( A x. B ) ) )
34 6 33 sylbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A x. B ) ) )
35 34 imp 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
36 35 an4s 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )