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

Metamath Proof Explorer

Theorem remulg

Description: The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

Ref Expression
Assertion remulg ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ( .g ‘ ℝfld ) 𝐴 ) = ( 𝑁 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
2 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
3 renegcl ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
4 1re ⊢ 1 ∈ ℝ
5 1 2 3 4 cnsubglem ⊢ ℝ ∈ ( SubGrp ‘ ℂfld )
6 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
7 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
8 eqid ⊢ ( .g ‘ ℝfld ) = ( .g ‘ ℝfld )
9 6 7 8 subgmulg ⊢ ( ( ℝ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ( .g ‘ ℂfld ) 𝐴 ) = ( 𝑁 ( .g ‘ ℝfld ) 𝐴 ) )
10 5 9 mp3an1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ( .g ‘ ℂfld ) 𝐴 ) = ( 𝑁 ( .g ‘ ℝfld ) 𝐴 ) )
11 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
12 11 recnd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℂ )
13 cnfldmulg ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℂ ) → ( 𝑁 ( .g ‘ ℂfld ) 𝐴 ) = ( 𝑁 · 𝐴 ) )
14 12 13 syldan ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ( .g ‘ ℂfld ) 𝐴 ) = ( 𝑁 · 𝐴 ) )
15 10 14 eqtr3d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ( .g ‘ ℝfld ) 𝐴 ) = ( 𝑁 · 𝐴 ) )