Metamath Proof Explorer

Theorem xrge0mulgnn0

Description: The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017)

Ref Expression
Assertion xrge0mulgnn0 ⊢ A ∈ ℕ 0 ∧ B ∈ 0 +∞ → A ⋅ ℝ 𝑠 * ↾ 𝑠 0 +∞ B = A ⋅ 𝑒 B

Proof

Step Hyp Ref Expression
1 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
2 iccssxr ⊢ 0 +∞ ⊆ ℝ *
3 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
4 2 3 sseqtri ⊢ 0 +∞ ⊆ Base ℝ 𝑠 *
5 eqid ⊢ ⋅ ℝ 𝑠 * = ⋅ ℝ 𝑠 *
6 eqid ⊢ inv g ⁡ ℝ 𝑠 * = inv g ⁡ ℝ 𝑠 *
7 xrs0 ⊢ 0 = 0 ℝ 𝑠 *
8 xrge00 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
9 7 8 eqtr3i ⊢ 0 ℝ 𝑠 * = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
10 1 4 5 6 9 ressmulgnn0 ⊢ A ∈ ℕ 0 ∧ B ∈ 0 +∞ → A ⋅ ℝ 𝑠 * ↾ 𝑠 0 +∞ B = A ⋅ ℝ 𝑠 * B
11 nn0z ⊢ A ∈ ℕ 0 → A ∈ ℤ
12 eliccxr ⊢ B ∈ 0 +∞ → B ∈ ℝ *
13 xrsmulgzz ⊢ A ∈ ℤ ∧ B ∈ ℝ * → A ⋅ ℝ 𝑠 * B = A ⋅ 𝑒 B
14 11 12 13 syl2an ⊢ A ∈ ℕ 0 ∧ B ∈ 0 +∞ → A ⋅ ℝ 𝑠 * B = A ⋅ 𝑒 B
15 10 14 eqtrd ⊢ A ∈ ℕ 0 ∧ B ∈ 0 +∞ → A ⋅ ℝ 𝑠 * ↾ 𝑠 0 +∞ B = A ⋅ 𝑒 B