Theorem renegscl

Description: The surreal reals are closed under negation. Part of theorem 13(ii) of Conway p. 24. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	renegscl	$$⊢A\in {ℝ}_s\to {+}_s\left(A\right)\in {ℝ}_s$$

Proof

Step	Hyp	Ref	Expression
1		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
2	1	adantr	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to {+}_s\left(A\right)\in \mathrm{No}$$
3		nnsno	$$⊢n\in {\mathbb{N}}_s\to n\in \mathrm{No}$$
4	3	adantl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to n\in \mathrm{No}$$
5	4	negscld	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(n\right)\in \mathrm{No}$$
6		simpl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A\in \mathrm{No}$$
7	5 6	sltnegd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(n\right){<}_{s}A\leftrightarrow {+}_s\left(A\right){<}_s{+}_s\left({+}_s\left(n\right)\right)\right)$$
8		negnegs	$$⊢n\in \mathrm{No}\to {+}_s\left({+}_s\left(n\right)\right)=n$$
9	4 8	syl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left({+}_s\left(n\right)\right)=n$$
10	9	breq2d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(A\right){<}_s{+}_s\left({+}_s\left(n\right)\right)\leftrightarrow {+}_s\left(A\right){<}_{s}n\right)$$
11	7 10	bitrd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(n\right){<}_{s}A\leftrightarrow {+}_s\left(A\right){<}_{s}n\right)$$
12	6 4	sltnegd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(A{<}_{s}n\leftrightarrow {+}_s\left(n\right){<}_s{+}_s\left(A\right)\right)$$
13	11 12	anbi12d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\leftrightarrow \left({+}_s\left(A\right){<}_{s}n\wedge {+}_s\left(n\right){<}_s{+}_s\left(A\right)\right)\right)$$
14	13	biancomd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\leftrightarrow \left({+}_s\left(n\right){<}_s{+}_s\left(A\right)\wedge {+}_s\left(A\right){<}_{s}n\right)\right)$$
15	14	rexbidva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{+}_s\left(A\right)\wedge {+}_s\left(A\right){<}_{s}n\right)\right)$$
16	15	biimpa	$$⊢\left(A\in \mathrm{No}\wedge \exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\right)\to \exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{+}_s\left(A\right)\wedge {+}_s\left(A\right){<}_{s}n\right)$$
17	16	adantrr	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to \exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{+}_s\left(A\right)\wedge {+}_s\left(A\right){<}_{s}n\right)$$
18		recut	$$⊢A\in \mathrm{No}\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
19	18	adantr	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
20		simprr	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
21	19 20	negsunif	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to {+}_s\left(A\right)={+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]{|}_s{+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]$$
22		negsfn	$$⊢{+}_{s}Fn\mathrm{No}$$
23		ssltss2	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
24	18 23	syl	$$⊢A\in \mathrm{No}\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
25		fvelimab	$$⊢\left({+}_{s}Fn\mathrm{No}\wedge \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}\right)\to \left(y\in {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]\leftrightarrow \exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\right)$$
26	22 24 25	sylancr	$$⊢A\in \mathrm{No}\to \left(y\in {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]\leftrightarrow \exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\right)$$
27		eqeq1	$$⊢x=z\to \left(x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
28	27	rexbidv	$$⊢x=z\to \left(\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
29	28	rexab	$$⊢\exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\leftrightarrow \exists z\left(\exists n\in {\mathbb{N}}_{s}z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
30		rexcom4	$$⊢\exists n\in {\mathbb{N}}_s\exists z\left(z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists z\exists n\in {\mathbb{N}}_s\left(z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
31		ovex	$$⊢A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{V}$$
32		fveqeq2	$$⊢z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left({+}_s\left(z\right)=y\leftrightarrow {+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\right)$$
33	31 32	ceqsexv	$$⊢\exists z\left(z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow {+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
34	33	rexbii	$$⊢\exists n\in {\mathbb{N}}_s\exists z\left(z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists n\in {\mathbb{N}}_s{+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
35		r19.41v	$$⊢\exists n\in {\mathbb{N}}_s\left(z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \left(\exists n\in {\mathbb{N}}_{s}z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
36	35	exbii	$$⊢\exists z\exists n\in {\mathbb{N}}_s\left(z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists z\left(\exists n\in {\mathbb{N}}_{s}z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
37	30 34 36	3bitr3ri	$$⊢\exists z\left(\exists n\in {\mathbb{N}}_{s}z=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists n\in {\mathbb{N}}_s{+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
38	29 37	bitri	$$⊢\exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\leftrightarrow \exists n\in {\mathbb{N}}_s{+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
39		1sno	$$⊢1_s\in \mathrm{No}$$
40	39	a1i	$$⊢n\in {\mathbb{N}}_s\to 1_s\in \mathrm{No}$$
41		nnne0s	$$⊢n\in {\mathbb{N}}_s\to n\ne 0_s$$
42	40 3 41	divscld	$$⊢n\in {\mathbb{N}}_s\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
43	42	adantl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
44		negsdi	$$⊢\left(A\in \mathrm{No}\wedge 1_s{/}_{\mathrm{su}}n\in \mathrm{No}\right)\to {+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
45	43 44	syldan	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
46	1	adantr	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A\right)\in \mathrm{No}$$
47	46 43	subsvald	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)={+}_s\left(A\right){+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
48	45 47	eqtr4d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
49	48	eqeq1d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\leftrightarrow {+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)=y\right)$$
50		eqcom	$$⊢{+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)=y\leftrightarrow y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
51	49 50	bitrdi	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\leftrightarrow y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
52	51	rexbidva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_s{+}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\leftrightarrow \exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
53	38 52	bitrid	$$⊢A\in \mathrm{No}\to \left(\exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\leftrightarrow \exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
54	26 53	bitrd	$$⊢A\in \mathrm{No}\to \left(y\in {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]\leftrightarrow \exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
55	54	eqabdv	$$⊢A\in \mathrm{No}\to {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
56		ssltss1	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
57	18 56	syl	$$⊢A\in \mathrm{No}\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
58		fvelimab	$$⊢\left({+}_{s}Fn\mathrm{No}\wedge \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}\right)\to \left(y\in {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]\leftrightarrow \exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\right)$$
59	22 57 58	sylancr	$$⊢A\in \mathrm{No}\to \left(y\in {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]\leftrightarrow \exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\right)$$
60		eqeq1	$$⊢x=z\to \left(x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
61	60	rexbidv	$$⊢x=z\to \left(\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
62	61	rexab	$$⊢\exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\leftrightarrow \exists z\left(\exists n\in {\mathbb{N}}_{s}z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
63		rexcom4	$$⊢\exists n\in {\mathbb{N}}_s\exists z\left(z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists z\exists n\in {\mathbb{N}}_s\left(z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
64		ovex	$$⊢A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{V}$$
65		fveqeq2	$$⊢z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left({+}_s\left(z\right)=y\leftrightarrow {+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\right)$$
66	64 65	ceqsexv	$$⊢\exists z\left(z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow {+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
67	66	rexbii	$$⊢\exists n\in {\mathbb{N}}_s\exists z\left(z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists n\in {\mathbb{N}}_s{+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
68		r19.41v	$$⊢\exists n\in {\mathbb{N}}_s\left(z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \left(\exists n\in {\mathbb{N}}_{s}z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
69	68	exbii	$$⊢\exists z\exists n\in {\mathbb{N}}_s\left(z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists z\left(\exists n\in {\mathbb{N}}_{s}z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)$$
70	63 67 69	3bitr3ri	$$⊢\exists z\left(\exists n\in {\mathbb{N}}_{s}z=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge {+}_s\left(z\right)=y\right)\leftrightarrow \exists n\in {\mathbb{N}}_s{+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
71	62 70	bitri	$$⊢\exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\leftrightarrow \exists n\in {\mathbb{N}}_s{+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y$$
72	6 43	subsvald	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)=A{+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
73	72	fveq2d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A{+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
74	43	negscld	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}$$
75		negsdi	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}\right)\to {+}_s\left(A{+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){+}_s{+}_s\left({+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
76	74 75	syldan	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A{+}_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){+}_s{+}_s\left({+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
77		negnegs	$$⊢1_s{/}_{\mathrm{su}}n\in \mathrm{No}\to {+}_s\left({+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=1_s{/}_{\mathrm{su}}n$$
78	43 77	syl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left({+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=1_s{/}_{\mathrm{su}}n$$
79	78	oveq2d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A\right){+}_s{+}_s\left({+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
80	73 76 79	3eqtrd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to {+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
81	80	eqeq1d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\leftrightarrow {+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)=y\right)$$
82		eqcom	$$⊢{+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)=y\leftrightarrow y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
83	81 82	bitrdi	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left({+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\leftrightarrow y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
84	83	rexbidva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_s{+}_s\left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)=y\leftrightarrow \exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
85	71 84	bitrid	$$⊢A\in \mathrm{No}\to \left(\exists z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{+}_s\left(z\right)=y\leftrightarrow \exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
86	59 85	bitrd	$$⊢A\in \mathrm{No}\to \left(y\in {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]\leftrightarrow \exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
87	86	eqabdv	$$⊢A\in \mathrm{No}\to {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
88	55 87	oveq12d	$$⊢A\in \mathrm{No}\to {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]{|}_s{+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
89	88	adantr	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to {+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]{|}_s{+}_s\left[\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right]=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
90	21 89	eqtrd	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to {+}_s\left(A\right)=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
91	2 17 90	jca32	$$⊢\left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)\to \left({+}_s\left(A\right)\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{+}_s\left(A\right)\wedge {+}_s\left(A\right){<}_{s}n\right)\wedge {+}_s\left(A\right)=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
92		elreno	$$⊢A\in {ℝ}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
93		elreno	$$⊢{+}_s\left(A\right)\in {ℝ}_s\leftrightarrow \left({+}_s\left(A\right)\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{+}_s\left(A\right)\wedge {+}_s\left(A\right){<}_{s}n\right)\wedge {+}_s\left(A\right)=\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y={+}_s\left(A\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
94	91 92 93	3imtr4i	$$⊢A\in {ℝ}_s\to {+}_s\left(A\right)\in {ℝ}_s$$