Theorem xrsnsgrp

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

	Ref	Expression
Assertion	xrsnsgrp	|- RR*s e/ Smgrp

Proof

Step	Hyp	Ref	Expression
1		1xr	|- 1 e. RR*
2		mnfxr	|- -oo e. RR*
3		pnfxr	|- +oo e. RR*
4	1 2 3	3pm3.2i	|- ( 1 e. RR* /\ -oo e. RR* /\ +oo e. RR* )
5		xaddcom	|- ( ( 1 e. RR* /\ -oo e. RR* ) -> ( 1 +e -oo ) = ( -oo +e 1 ) )
6	1 2 5	mp2an	|- ( 1 +e -oo ) = ( -oo +e 1 )
7		1re	|- 1 e. RR
8		renepnf	|- ( 1 e. RR -> 1 =/= +oo )
9	7 8	ax-mp	|- 1 =/= +oo
10		xaddmnf2	|- ( ( 1 e. RR* /\ 1 =/= +oo ) -> ( -oo +e 1 ) = -oo )
11	1 9 10	mp2an	|- ( -oo +e 1 ) = -oo
12	6 11	eqtri	|- ( 1 +e -oo ) = -oo
13	12	oveq1i	|- ( ( 1 +e -oo ) +e +oo ) = ( -oo +e +oo )
14		mnfaddpnf	|- ( -oo +e +oo ) = 0
15	13 14	eqtri	|- ( ( 1 +e -oo ) +e +oo ) = 0
16		0ne1	|- 0 =/= 1
17	15 16	eqnetri	|- ( ( 1 +e -oo ) +e +oo ) =/= 1
18	14	oveq2i	|- ( 1 +e ( -oo +e +oo ) ) = ( 1 +e 0 )
19		xaddid1	|- ( 1 e. RR* -> ( 1 +e 0 ) = 1 )
20	1 19	ax-mp	|- ( 1 +e 0 ) = 1
21	18 20	eqtri	|- ( 1 +e ( -oo +e +oo ) ) = 1
22	17 21	neeqtrri	|- ( ( 1 +e -oo ) +e +oo ) =/= ( 1 +e ( -oo +e +oo ) )
23		xrsbas	|- RR* = ( Base ` RR*s )
24		xrsadd	|- +e = ( +g ` RR*s )
25	23 24	isnsgrp	|- ( ( 1 e. RR* /\ -oo e. RR* /\ +oo e. RR* ) -> ( ( ( 1 +e -oo ) +e +oo ) =/= ( 1 +e ( -oo +e +oo ) ) -> RR*s e/ Smgrp ) )
26	4 22 25	mp2	|- RR*s e/ Smgrp