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 ) 𝐴 ) = ( 𝑁 · 𝐴 ) )