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	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
Assertion	rpmsubg	⊢ ℝ+ ∈ ( SubGrp ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
3		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
4		rpmulcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 · 𝑦 ) ∈ ℝ+ )
5		1rp	⊢ 1 ∈ ℝ+
6		rpreccl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
7	1 2 3 4 5 6	cnmsubglem	⊢ ℝ+ ∈ ( SubGrp ‘ 𝑀 )