Metamath Proof Explorer


Theorem ge0xmulcl

Description: The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ge0xmulcl A0+∞B0+∞A𝑒B0+∞

Proof

Step Hyp Ref Expression
1 elxrge0 A0+∞A*0A
2 elxrge0 B0+∞B*0B
3 xmulcl A*B*A𝑒B*
4 3 ad2ant2r A*0AB*0BA𝑒B*
5 xmulge0 A*0AB*0B0A𝑒B
6 elxrge0 A𝑒B0+∞A𝑒B*0A𝑒B
7 4 5 6 sylanbrc A*0AB*0BA𝑒B0+∞
8 1 2 7 syl2anb A0+∞B0+∞A𝑒B0+∞