Metamath Proof Explorer

Theorem xrsmgmdifsgrp

Description: The "additive group" of the extended reals is a magma but not a semigroup, and therefore also not a monoid nor a group, in contrast to the "multiplicative group", see xrsmcmn . (Contributed by AV, 30-Jan-2020)

Ref Expression
Assertion xrsmgmdifsgrp 
|- RR*s e. ( Mgm \ Smgrp )

Proof

Step Hyp Ref Expression
1 xrsmgm 
 |-  RR*s e. Mgm
2 xrsnsgrp 
 |-  RR*s e/ Smgrp
3 2 neli 
 |-  -. RR*s e. Smgrp
4 eldif 
 |-  ( RR*s e. ( Mgm \ Smgrp ) <-> ( RR*s e. Mgm /\ -. RR*s e. Smgrp ) )
5 1 3 4 mpbir2an 
 |-  RR*s e. ( Mgm \ Smgrp )