Theorem xrsnsgrp

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

	Ref	Expression
Assertion	xrsnsgrp	$$⊢{ℝ}_{𝑠}^{*}\notin \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		1xr	$$⊢1\in {ℝ}^{*}$$
2		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
3		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
4	1 2 3	3pm3.2i	$$⊢\left(1\in {ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)$$
5		xaddcom	$$⊢\left(1\in {ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\right)\to 1{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }{+}_{𝑒}1$$
6	1 2 5	mp2an	$$⊢1{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }{+}_{𝑒}1$$
7		1re	$$⊢1\in ℝ$$
8		renepnf	$$⊢1\in ℝ\to 1\ne \mathrm{+\infty }$$
9	7 8	ax-mp	$$⊢1\ne \mathrm{+\infty }$$
10		xaddmnf2	$$⊢\left(1\in {ℝ}^{*}\wedge 1\ne \mathrm{+\infty }\right)\to \mathrm{-\infty }{+}_{𝑒}1=\mathrm{-\infty }$$
11	1 9 10	mp2an	$$⊢\mathrm{-\infty }{+}_{𝑒}1=\mathrm{-\infty }$$
12	6 11	eqtri	$$⊢1{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }$$
13	12	oveq1i	$$⊢\left(1{+}_{𝑒}\mathrm{-\infty }\right){+}_{𝑒}\mathrm{+\infty }=\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }$$
14		mnfaddpnf	$$⊢\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }=0$$
15	13 14	eqtri	$$⊢\left(1{+}_{𝑒}\mathrm{-\infty }\right){+}_{𝑒}\mathrm{+\infty }=0$$
16		0ne1	$$⊢0\ne 1$$
17	15 16	eqnetri	$$⊢\left(1{+}_{𝑒}\mathrm{-\infty }\right){+}_{𝑒}\mathrm{+\infty }\ne 1$$
18	14	oveq2i	$$⊢1{+}_{𝑒}\left(\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }\right)=1{+}_{𝑒}0$$
19		xaddrid	$$⊢1\in {ℝ}^{*}\to 1{+}_{𝑒}0=1$$
20	1 19	ax-mp	$$⊢1{+}_{𝑒}0=1$$
21	18 20	eqtri	$$⊢1{+}_{𝑒}\left(\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }\right)=1$$
22	17 21	neeqtrri	$$⊢\left(1{+}_{𝑒}\mathrm{-\infty }\right){+}_{𝑒}\mathrm{+\infty }\ne 1{+}_{𝑒}\left(\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }\right)$$
23		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
24		xrsadd	$$⊢{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
25	23 24	isnsgrp	$$⊢\left(1\in {ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(\left(1{+}_{𝑒}\mathrm{-\infty }\right){+}_{𝑒}\mathrm{+\infty }\ne 1{+}_{𝑒}\left(\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }\right)\to {ℝ}_{𝑠}^{*}\notin \mathrm{Smgrp}\right)$$
26	4 22 25	mp2	$$⊢{ℝ}_{𝑠}^{*}\notin \mathrm{Smgrp}$$