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 ) )