Theorem rpmsubg

Description: The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Hypothesis	cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
Assertion	rpmsubg	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
3		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
4		rpmulcl	$$⊢\left(x\in {ℝ}^{+}\wedge y\in {ℝ}^{+}\right)\to xy\in {ℝ}^{+}$$
5		1rp	$$⊢1\in {ℝ}^{+}$$
6		rpreccl	$$⊢x\in {ℝ}^{+}\to \frac{1}{x}\in {ℝ}^{+}$$
7	1 2 3 4 5 6	cnmsubglem	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left(M\right)$$