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

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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
3 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
4 2 3 sseqtri ⊢ ( 0 [,] +∞ ) ⊆ ( Base ‘ ℝ*𝑠 )
5 eqid ⊢ ( .g ‘ ℝ*𝑠 ) = ( .g ‘ ℝ*𝑠 )
6 eqid ⊢ ( invg ‘ ℝ*𝑠 ) = ( invg ‘ ℝ*𝑠 )
7 xrs0 ⊢ 0 = ( 0g ‘ ℝ*𝑠 )
8 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
9 7 8 eqtr3i ⊢ ( 0g ‘ ℝ*𝑠 ) = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
10 1 4 5 6 9 ressmulgnn0 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) )
11 nn0z ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
12 eliccxr ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 𝐵 ∈ ℝ* )
13 xrsmulgzz ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )
14 11 12 13 syl2an ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ℝ*𝑠 ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )
15 10 14 eqtrd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ( .g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) 𝐵 ) = ( 𝐴 ·e 𝐵 ) )