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
lt2.2 B
Assertion mulge0i 0 A 0 B 0 A B

Proof

Step Hyp Ref Expression
1 lt2.1 A
2 lt2.2 B
3 mulge0 A 0 A B 0 B 0 A B
4 3 an4s A B 0 A 0 B 0 A B
5 1 2 4 mpanl12 0 A 0 B 0 A B