Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrsmcmn Structured version   Unicode version

Theorem xrsmcmn 17814
 Description: The multiplicative group of the extended reals forms a commutative monoid (even though the additive group is not, see xrs1mnd 17826.) (Contributed by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
xrsmcmn mulGrp CMnd

Proof of Theorem xrsmcmn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2438 . . . . 5 mulGrp mulGrp
2 xrsbas 17807 . . . . 5
31, 2mgpbas 16585 . . . 4 mulGrp
43a1i 11 . . 3 mulGrp
5 xrsmul 17809 . . . . 5
61, 5mgpplusg 16583 . . . 4 mulGrp
76a1i 11 . . 3 mulGrp
8 xmulcl 11228 . . . . 5
983adant1 1006 . . . 4
10 xmulass 11242 . . . . 5
1110adantl 466 . . . 4
12 1re 9377 . . . . 5
13 rexr 9421 . . . . 5
1412, 13mp1i 12 . . . 4
15 xmulid2 11235 . . . . 5
1615adantl 466 . . . 4
17 xmulid1 11234 . . . . 5
1817adantl 466 . . . 4
194, 7, 9, 11, 14, 16, 18ismndd 15436 . . 3 mulGrp
20 xmulcom 11221 . . . 4