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 ⊢ N ∈ ℤ ∧ A ∈ ℝ → N ⋅ ℝ fld A = N ⁢ A

Proof

Step Hyp Ref Expression
1 recn ⊢ x ∈ ℝ → x ∈ ℂ
2 readdcl ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + y ∈ ℝ
3 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 1 2 3 4 cnsubglem ⊢ ℝ ∈ SubGrp ⁡ ℂ fld
6 eqid ⊢ ⋅ ℂ fld = ⋅ ℂ fld
7 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
8 eqid ⊢ ⋅ ℝ fld = ⋅ ℝ fld
9 6 7 8 subgmulg ⊢ ℝ ∈ SubGrp ⁡ ℂ fld ∧ N ∈ ℤ ∧ A ∈ ℝ → N ⋅ ℂ fld A = N ⋅ ℝ fld A
10 5 9 mp3an1 ⊢ N ∈ ℤ ∧ A ∈ ℝ → N ⋅ ℂ fld A = N ⋅ ℝ fld A
11 simpr ⊢ N ∈ ℤ ∧ A ∈ ℝ → A ∈ ℝ
12 11 recnd ⊢ N ∈ ℤ ∧ A ∈ ℝ → A ∈ ℂ
13 cnfldmulg ⊢ N ∈ ℤ ∧ A ∈ ℂ → N ⋅ ℂ fld A = N ⁢ A
14 12 13 syldan ⊢ N ∈ ℤ ∧ A ∈ ℝ → N ⋅ ℂ fld A = N ⁢ A
15 10 14 eqtr3d ⊢ N ∈ ℤ ∧ A ∈ ℝ → N ⋅ ℝ fld A = N ⁢ A