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	Could not format assertion : No typesetting found for |- RR*s e. ( Mgm \ Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		xrsmgm	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Mgm}$$
2		xrsnsgrp	Could not format RR*s e/ Smgrp : No typesetting found for |- RR*s e/ Smgrp with typecode |-
3	2	neli	Could not format -. RR*s e. Smgrp : No typesetting found for |- -. RR*s e. Smgrp with typecode |-
4		eldif	Could not format ( RR*s e. ( Mgm \ Smgrp ) <-> ( RR*s e. Mgm /\ -. RR*s e. Smgrp ) ) : No typesetting found for |- ( RR*s e. ( Mgm \ Smgrp ) <-> ( RR*s e. Mgm /\ -. RR*s e. Smgrp ) ) with typecode |-
5	1 3 4	mpbir2an	Could not format RR*s e. ( Mgm \ Smgrp ) : No typesetting found for |- RR*s e. ( Mgm \ Smgrp ) with typecode |-