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 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ → A ⋅ 𝑒 B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 elxrge0 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ * ∧ 0 ≤ A
2 elxrge0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ * ∧ 0 ≤ B
3 xmulcl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ⋅ 𝑒 B ∈ ℝ *
4 3 ad2ant2r ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B → A ⋅ 𝑒 B ∈ ℝ *
5 xmulge0 ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B → 0 ≤ A ⋅ 𝑒 B
6 elxrge0 ⊢ A ⋅ 𝑒 B ∈ 0 +∞ ↔ A ⋅ 𝑒 B ∈ ℝ * ∧ 0 ≤ A ⋅ 𝑒 B
7 4 5 6 sylanbrc ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B → A ⋅ 𝑒 B ∈ 0 +∞
8 1 2 7 syl2anb ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ → A ⋅ 𝑒 B ∈ 0 +∞