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