Metamath Proof Explorer


Theorem mulge0i

Description: The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999)

Ref Expression
Hypotheses lt2.1
|- A e. RR
lt2.2
|- B e. RR
Assertion mulge0i
|- ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A x. B ) )

Proof

Step Hyp Ref Expression
1 lt2.1
 |-  A e. RR
2 lt2.2
 |-  B e. RR
3 mulge0
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
4 3 an4s
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
5 1 2 4 mpanl12
 |-  ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A x. B ) )