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

Metamath Proof Explorer

Theorem mulge0i

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

Step	Hyp	Ref	Expression
1		lt2.1	$⊢ A \in ℝ$
2		lt2.2	$⊢ B \in ℝ$
3		mulge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to 0 \leq A B$
4	3	an4s	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 0 \leq B)) \to 0 \leq A B$
5	1 2 4	mpanl12	$⊢ (0 \leq A \land 0 \leq B) \to 0 \leq A B$