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 = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |
|
| Assertion | rpmsubg | |- RR+ e. ( SubGrp ` M ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnmgpabl.m | |- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |
|
| 2 | rpcn | |- ( x e. RR+ -> x e. CC ) |
|
| 3 | rpne0 | |- ( x e. RR+ -> x =/= 0 ) |
|
| 4 | rpmulcl | |- ( ( x e. RR+ /\ y e. RR+ ) -> ( x x. y ) e. RR+ ) |
|
| 5 | 1rp | |- 1 e. RR+ |
|
| 6 | rpreccl | |- ( x e. RR+ -> ( 1 / x ) e. RR+ ) |
|
| 7 | 1 2 3 4 5 6 | cnmsubglem | |- RR+ e. ( SubGrp ` M ) |