Theorem remulg

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

	Ref	Expression
Assertion	remulg	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to N{\cdot }_{{ℝ}_{\mathrm{fld}}}A=NA$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢x\in ℝ\to x\in ℂ$$
2		readdcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+y\in ℝ$$
3		renegcl	$$⊢x\in ℝ\to -x\in ℝ$$
4		1re	$$⊢1\in ℝ$$
5	1 2 3 4	cnsubglem	$$⊢ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
6		eqid	$$⊢{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
7		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
8		eqid	$$⊢{\cdot }_{{ℝ}_{\mathrm{fld}}}={\cdot }_{{ℝ}_{\mathrm{fld}}}$$
9	6 7 8	subgmulg	$$⊢\left(ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge N\in \mathbb{Z}\wedge A\in ℝ\right)\to N{\cdot }_{{ℂ}_{\mathrm{fld}}}A=N{\cdot }_{{ℝ}_{\mathrm{fld}}}A$$
10	5 9	mp3an1	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to N{\cdot }_{{ℂ}_{\mathrm{fld}}}A=N{\cdot }_{{ℝ}_{\mathrm{fld}}}A$$
11		simpr	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to A\in ℝ$$
12	11	recnd	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to A\in ℂ$$
13		cnfldmulg	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℂ\right)\to N{\cdot }_{{ℂ}_{\mathrm{fld}}}A=NA$$
14	12 13	syldan	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to N{\cdot }_{{ℂ}_{\mathrm{fld}}}A=NA$$
15	10 14	eqtr3d	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to N{\cdot }_{{ℝ}_{\mathrm{fld}}}A=NA$$