This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ℝ^*_𝑠 ∈ ( 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 )