Theorem xrsnsgrp

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

	Ref	Expression
Assertion	xrsnsgrp	Could not format assertion : No typesetting found for |- RR*s e/ Smgrp with typecode |-

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		xaddid1	$$⊢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	Could not format ( ( 1 e. RR* /\ -oo e. RR* /\ +oo e. RR* ) -> ( ( ( 1 +e -oo ) +e +oo ) =/= ( 1 +e ( -oo +e +oo ) ) -> RR*s e/ Smgrp ) ) : No typesetting found for |- ( ( 1 e. RR* /\ -oo e. RR* /\ +oo e. RR* ) -> ( ( ( 1 +e -oo ) +e +oo ) =/= ( 1 +e ( -oo +e +oo ) ) -> RR*s e/ Smgrp ) ) with typecode |-
26	4 22 25	mp2	Could not format RR*s e/ Smgrp : No typesetting found for |- RR*s e/ Smgrp with typecode |-