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	⊢ ℝ*𝑠 ∈ ( Mgm ∖ Smgrp )

Proof

Step	Hyp	Ref	Expression
1		xrsmgm	⊢ ℝ*𝑠 ∈ Mgm
2		xrsnsgrp	⊢ ℝ*𝑠 ∉ Smgrp
3	2	neli	⊢ ¬ ℝ*𝑠 ∈ Smgrp
4		eldif	⊢ ( ℝ*𝑠 ∈ ( Mgm ∖ Smgrp ) ↔ ( ℝ*𝑠 ∈ Mgm ∧ ¬ ℝ*𝑠 ∈ Smgrp ) )
5	1 3 4	mpbir2an	⊢ ℝ*𝑠 ∈ ( Mgm ∖ Smgrp )