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

Metamath Proof Explorer

Theorem xrsnsgrp

Description: The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020)

Ref Expression
Assertion xrsnsgrp ℝ*𝑠 ∉ Smgrp

Proof

Step Hyp Ref Expression
1 1xr ⊢ 1 ∈ ℝ*
2 mnfxr ⊢ -∞ ∈ ℝ*
3 pnfxr ⊢ +∞ ∈ ℝ*
4 1 2 3 3pm3.2i ⊢ ( 1 ∈ ℝ* ∧ -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* )
5 xaddcom ⊢ ( ( 1 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( 1 +𝑒 -∞ ) = ( -∞ +𝑒 1 ) )
6 1 2 5 mp2an ⊢ ( 1 +𝑒 -∞ ) = ( -∞ +𝑒 1 )
7 1re ⊢ 1 ∈ ℝ
8 renepnf ⊢ ( 1 ∈ ℝ → 1 ≠ +∞ )
9 7 8 ax-mp ⊢ 1 ≠ +∞
10 xaddmnf2 ⊢ ( ( 1 ∈ ℝ* ∧ 1 ≠ +∞ ) → ( -∞ +𝑒 1 ) = -∞ )
11 1 9 10 mp2an ⊢ ( -∞ +𝑒 1 ) = -∞
12 6 11 eqtri ⊢ ( 1 +𝑒 -∞ ) = -∞
13 12 oveq1i ⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) = ( -∞ +𝑒 +∞ )
14 mnfaddpnf ⊢ ( -∞ +𝑒 +∞ ) = 0
15 13 14 eqtri ⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) = 0
16 0ne1 ⊢ 0 ≠ 1
17 15 16 eqnetri ⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) ≠ 1
18 14 oveq2i ⊢ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) ) = ( 1 +𝑒 0 )
19 xaddrid ⊢ ( 1 ∈ ℝ* → ( 1 +𝑒 0 ) = 1 )
20 1 19 ax-mp ⊢ ( 1 +𝑒 0 ) = 1
21 18 20 eqtri ⊢ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) ) = 1
22 17 21 neeqtrri ⊢ ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) ≠ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) )
23 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
24 xrsadd ⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
25 23 24 isnsgrp ⊢ ( ( 1 ∈ ℝ* ∧ -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( ( 1 +𝑒 -∞ ) +𝑒 +∞ ) ≠ ( 1 +𝑒 ( -∞ +𝑒 +∞ ) ) → ℝ*𝑠 ∉ Smgrp ) )
26 4 22 25 mp2 ⊢ ℝ*𝑠 ∉ Smgrp