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 ) |
| 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 ) |