Theorem elreno2

Description: Alternate characterization of the surreal reals. Theorem 4.4(b) of Gonshor p. 39. (Contributed by Scott Fenton, 29-Jan-2026)

	Ref	Expression
Assertion	elreno2	Could not format assertion : No typesetting found for |- ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )

Proof

Step	Hyp	Ref	Expression
1		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\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
2		recut	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
3	2	adantr	$$⊢\left(A\in \mathrm{No}\wedge A=\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
4		simpr	$$⊢\left(A\in \mathrm{No}\wedge A=\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\to A=\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
5	3 4	cofcutr1d	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) with typecode |-
6		eqeq1	$$⊢w=y\to \left(w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
7	6	rexbidv	$$⊢w=y\to \left(\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
8	7	rexab	Could not format ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) : No typesetting found for |- ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) with typecode |-
9		rexcom4	Could not format ( E. n e. NN_s E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. y E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) : No typesetting found for |- ( E. n e. NN_s E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. y E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) with typecode |-
10		ovex	$$⊢A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{V}$$
11		breq2	Could not format ( y = ( A -s ( 1s /su n ) ) -> ( xO <_s y <-> xO <_s ( A -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( y = ( A -s ( 1s /su n ) ) -> ( xO <_s y <-> xO <_s ( A -s ( 1s /su n ) ) ) ) with typecode |-
12	10 11	ceqsexv	Could not format ( E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> xO <_s ( A -s ( 1s /su n ) ) ) : No typesetting found for |- ( E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> xO <_s ( A -s ( 1s /su n ) ) ) with typecode |-
13	12	rexbii	Could not format ( E. n e. NN_s E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) : No typesetting found for |- ( E. n e. NN_s E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) with typecode |-
14		r19.41v	Could not format ( E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) : No typesetting found for |- ( E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) with typecode |-
15	14	exbii	Could not format ( E. y E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) : No typesetting found for |- ( E. y E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) ) with typecode |-
16	9 13 15	3bitr3ri	Could not format ( E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) : No typesetting found for |- ( E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) with typecode |-
17	8 16	bitri	Could not format ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) : No typesetting found for |- ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) with typecode |-
18		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
19	18	sseli	Could not format ( xO e. ( _Left ` A ) -> xO e. No ) : No typesetting found for |- ( xO e. ( _Left ` A ) -> xO e. No ) with typecode |-
20	19	adantl	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO e. No ) with typecode |-
21	20	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> xO e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> xO e. No ) with typecode |-
22		simpll	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> A e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> A e. No ) with typecode |-
23		1sno	$$⊢1_s\in \mathrm{No}$$
24	23	a1i	$$⊢n\in {\mathbb{N}}_s\to 1_s\in \mathrm{No}$$
25		nnsno	$$⊢n\in {\mathbb{N}}_s\to n\in \mathrm{No}$$
26		nnne0s	$$⊢n\in {\mathbb{N}}_s\to n\ne 0_s$$
27	24 25 26	divscld	$$⊢n\in {\mathbb{N}}_s\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
28	27	adantl	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No ) with typecode |-
29	22 28	subscld	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No ) with typecode |-
30	21 29 28	sleadd1d	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO <_s ( A -s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO <_s ( A -s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) ) ) with typecode |-
31		npcans	$$⊢\left(A\in \mathrm{No}\wedge 1_s{/}_{\mathrm{su}}n\in \mathrm{No}\right)\to \left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right){+}_s\left(1_s{/}_{\mathrm{su}}n\right)=A$$
32	22 28 31	syl2anc	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) = A ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) = A ) with typecode |-
33	32	breq2d	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( xO +s ( 1s /su n ) ) <_s ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( xO +s ( 1s /su n ) ) <_s ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
34	30 33	bitrd	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO <_s ( A -s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO <_s ( A -s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
35	34	rexbidva	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
36	35	adantlr	Could not format ( ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
37	17 36	bitrid	Could not format ( ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) /\ xO e. ( _Left ` A ) ) -> ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) /\ xO e. ( _Left ` A ) ) -> ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
38	37	ralbidva	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
39	5 38	mpbid	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) with typecode |-
40	3 4	cofcutr2d	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) with typecode |-
41		eqeq1	$$⊢w=y\to \left(w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
42	41	rexbidv	$$⊢w=y\to \left(\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
43	42	rexab	Could not format ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) : No typesetting found for |- ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) with typecode |-
44		rexcom4	Could not format ( E. n e. NN_s E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. y E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) : No typesetting found for |- ( E. n e. NN_s E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. y E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) with typecode |-
45		ovex	$$⊢A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{V}$$
46		breq1	Could not format ( y = ( A +s ( 1s /su n ) ) -> ( y <_s xO <-> ( A +s ( 1s /su n ) ) <_s xO ) ) : No typesetting found for |- ( y = ( A +s ( 1s /su n ) ) -> ( y <_s xO <-> ( A +s ( 1s /su n ) ) <_s xO ) ) with typecode |-
47	45 46	ceqsexv	Could not format ( E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( A +s ( 1s /su n ) ) <_s xO ) : No typesetting found for |- ( E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( A +s ( 1s /su n ) ) <_s xO ) with typecode |-
48	47	rexbii	Could not format ( E. n e. NN_s E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) : No typesetting found for |- ( E. n e. NN_s E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) with typecode |-
49		r19.41v	Could not format ( E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) : No typesetting found for |- ( E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) with typecode |-
50	49	exbii	Could not format ( E. y E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) : No typesetting found for |- ( E. y E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) ) with typecode |-
51	44 48 50	3bitr3ri	Could not format ( E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) : No typesetting found for |- ( E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) with typecode |-
52	43 51	bitri	Could not format ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) : No typesetting found for |- ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) with typecode |-
53		simpll	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> A e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> A e. No ) with typecode |-
54		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
55	54	sseli	Could not format ( xO e. ( _Right ` A ) -> xO e. No ) : No typesetting found for |- ( xO e. ( _Right ` A ) -> xO e. No ) with typecode |-
56	55	adantl	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> xO e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> xO e. No ) with typecode |-
57	56	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> xO e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> xO e. No ) with typecode |-
58	27	adantl	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No ) with typecode |-
59	57 58	subscld	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( xO -s ( 1s /su n ) ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( xO -s ( 1s /su n ) ) e. No ) with typecode |-
60	53 59 58	sleadd1d	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( A <_s ( xO -s ( 1s /su n ) ) <-> ( A +s ( 1s /su n ) ) <_s ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( A <_s ( xO -s ( 1s /su n ) ) <-> ( A +s ( 1s /su n ) ) <_s ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) ) ) with typecode |-
61		npcans	Could not format ( ( xO e. No /\ ( 1s /su n ) e. No ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO ) : No typesetting found for |- ( ( xO e. No /\ ( 1s /su n ) e. No ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO ) with typecode |-
62	57 58 61	syl2anc	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO ) with typecode |-
63	62	breq2d	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) <_s ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) <-> ( A +s ( 1s /su n ) ) <_s xO ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) <_s ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) <-> ( A +s ( 1s /su n ) ) <_s xO ) ) with typecode |-
64	60 63	bitr2d	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) <_s xO <-> A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) <_s xO <-> A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
65	64	rexbidva	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
66	52 65	bitrid	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
67	66	ralbidva	Could not format ( A e. No -> ( A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( A e. No -> ( A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
68	67	adantr	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
69	40 68	mpbid	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) with typecode |-
70	39 69	jca	Could not format ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
71		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
72	71	adantr	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
73		lltropt	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
74	73	a1i	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( _Left ` A ) < ( _Left ` A ) <
75	35	biimpar	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) ) with typecode |-
76	75 17	sylibr	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) with typecode |-
77	76	ex	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A -> E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A -> E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) ) with typecode |-
78	77	ralimdva	Could not format ( A e. No -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) ) : No typesetting found for |- ( A e. No -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) ) with typecode |-
79	78	imp	Could not format ( ( A e. No /\ A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) : No typesetting found for |- ( ( A e. No /\ A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) with typecode |-
80	79	adantrr	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) : No typesetting found for |- ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) with typecode |-
81	65	biimpar	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO ) with typecode |-
82	81 52	sylibr	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) with typecode |-
83	82	ex	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) -> E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) -> E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) ) with typecode |-
84	83	ralimdva	Could not format ( A e. No -> ( A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) ) : No typesetting found for |- ( A e. No -> ( A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) ) with typecode |-
85	84	imp	Could not format ( ( A e. No /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) : No typesetting found for |- ( ( A e. No /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) with typecode |-
86	85	adantrl	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) : No typesetting found for |- ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) with typecode |-
87		nnsex	$$⊢{\mathbb{N}}_s\in \mathrm{V}$$
88	87	abrexex	$$⊢\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
89	88	a1i	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
90		snexg	$$⊢A\in \mathrm{No}\to \left\{A\right\}\in \mathrm{V}$$
91		simpl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A\in \mathrm{No}$$
92	27	adantl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
93	91 92	subscld	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}$$
94		eleq1	$$⊢w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(w\in \mathrm{No}\leftrightarrow A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}\right)$$
95	93 94	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\to w\in \mathrm{No}\right)$$
96	95	rexlimdva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\to w\in \mathrm{No}\right)$$
97	96	abssdv	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
98		snssi	$$⊢A\in \mathrm{No}\to \left\{A\right\}\subseteq \mathrm{No}$$
99		biid	$$⊢A\in \mathrm{No}\leftrightarrow A\in \mathrm{No}$$
100		vex	$$⊢y\in \mathrm{V}$$
101	100 7	elab	$$⊢y\in \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\leftrightarrow \exists n\in {\mathbb{N}}_{s}y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
102		velsn	$$⊢z\in \left\{A\right\}\leftrightarrow z=A$$
103		id	$$⊢n\in {\mathbb{N}}_s\to n\in {\mathbb{N}}_s$$
104	103	nnsrecgt0d	$$⊢n\in {\mathbb{N}}_s\to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
105	104	adantl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
106	92 91	sltsubposd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right){<}_{s}A\right)$$
107	105 106	mpbid	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right){<}_{s}A$$
108		breq12	$$⊢\left(y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge z=A\right)\to \left(y{<}_{s}z\leftrightarrow \left(A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right){<}_{s}A\right)$$
109	107 108	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(\left(y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge z=A\right)\to y{<}_{s}z\right)$$
110	109	expd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(z=A\to y{<}_{s}z\right)\right)$$
111	110	rexlimdva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_{s}y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(z=A\to y{<}_{s}z\right)\right)$$
112	111	3imp	$$⊢\left(A\in \mathrm{No}\wedge \exists n\in {\mathbb{N}}_{s}y=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge z=A\right)\to y{<}_{s}z$$
113	99 101 102 112	syl3anb	$$⊢\left(A\in \mathrm{No}\wedge y\in \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\wedge z\in \left\{A\right\}\right)\to y{<}_{s}z$$
114	89 90 97 98 113	ssltd	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{A\right\}$$
115	71	sneqd	$$⊢A\in \mathrm{No}\to \left\{L\left(A\right){|}_{s}R\left(A\right)\right\}=\left\{A\right\}$$
116	114 115	breqtrrd	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{L\left(A\right){|}_{s}R\left(A\right)\right\}$$
117	116	adantr	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } < { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
118	72	sneqd	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } = { A } ) : No typesetting found for |- ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } = { A } ) with typecode |-
119	87	abrexex	$$⊢\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
120	119	a1i	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
121	91 92	addscld	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}$$
122		eleq1	$$⊢w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(w\in \mathrm{No}\leftrightarrow A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}\right)$$
123	121 122	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to w\in \mathrm{No}\right)$$
124	123	rexlimdva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to w\in \mathrm{No}\right)$$
125	124	abssdv	$$⊢A\in \mathrm{No}\to \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
126	100 42	elab	$$⊢y\in \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\leftrightarrow \exists n\in {\mathbb{N}}_{s}y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
127	92 91	sltaddpos1d	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow A{<}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)\right)$$
128	105 127	mpbid	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A{<}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
129		breq12	$$⊢\left(z=A\wedge y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)\to \left(z{<}_{s}y\leftrightarrow A{<}_s\left(A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)\right)$$
130	128 129	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(\left(z=A\wedge y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)\to z{<}_{s}y\right)$$
131	130	expcomd	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to \left(y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(z=A\to z{<}_{s}y\right)\right)$$
132	131	rexlimdva	$$⊢A\in \mathrm{No}\to \left(\exists n\in {\mathbb{N}}_{s}y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(z=A\to z{<}_{s}y\right)\right)$$
133	132	com23	$$⊢A\in \mathrm{No}\to \left(z=A\to \left(\exists n\in {\mathbb{N}}_{s}y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to z{<}_{s}y\right)\right)$$
134	133	3imp	$$⊢\left(A\in \mathrm{No}\wedge z=A\wedge \exists n\in {\mathbb{N}}_{s}y=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)\to z{<}_{s}y$$
135	99 102 126 134	syl3anb	$$⊢\left(A\in \mathrm{No}\wedge z\in \left\{A\right\}\wedge y\in \left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\to z{<}_{s}y$$
136	90 120 98 125 135	ssltd	$$⊢A\in \mathrm{No}\to \left\{A\right\}{\ll }_s\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
137	136	adantr	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { A } < { A } <
138	118 137	eqbrtrd	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } < { ( ( _Left ` A ) |s ( _Right ` A ) ) } <
139	74 80 86 117 138	cofcut1d	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) : No typesetting found for |- ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) with typecode |-
140	72 139	eqtr3d	Could not format ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) : No typesetting found for |- ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) with typecode |-
141	70 140	impbida	Could not format ( A e. No -> ( A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) ) : No typesetting found for |- ( A e. No -> ( A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) ) with typecode |-
142		ralunb	Could not format ( A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) /\ A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) ) : No typesetting found for |- ( A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) /\ A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) ) with typecode |-
143		simpl	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> A e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> A e. No ) with typecode |-
144	143 20	subscld	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( A -s xO ) e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( A -s xO ) e. No ) with typecode |-
145		0sno	$$⊢0_s\in \mathrm{No}$$
146	145	a1i	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s e. No ) with typecode |-
147		leftlt	Could not format ( xO e. ( _Left ` A ) -> xO xO
148	147	adantl	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO xO
149	20 143	posdifsd	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO 0s ( xO 0s
150	148 149	mpbid	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s 0s
151	146 144 150	sltled	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s <_s ( A -s xO ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s <_s ( A -s xO ) ) with typecode |-
152		abssid	Could not format ( ( ( A -s xO ) e. No /\ 0s <_s ( A -s xO ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) ) : No typesetting found for |- ( ( ( A -s xO ) e. No /\ 0s <_s ( A -s xO ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) ) with typecode |-
153	144 151 152	syl2anc	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) ) with typecode |-
154	153	breq2d	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) ) with typecode |-
155	154	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) ) with typecode |-
156	144	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s xO ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s xO ) e. No ) with typecode |-
157	28 156 21	sleadd2d	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( A -s xO ) <-> ( xO +s ( 1s /su n ) ) <_s ( xO +s ( A -s xO ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( A -s xO ) <-> ( xO +s ( 1s /su n ) ) <_s ( xO +s ( A -s xO ) ) ) ) with typecode |-
158		pncan3s	Could not format ( ( xO e. No /\ A e. No ) -> ( xO +s ( A -s xO ) ) = A ) : No typesetting found for |- ( ( xO e. No /\ A e. No ) -> ( xO +s ( A -s xO ) ) = A ) with typecode |-
159	20 143 158	syl2anc	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO +s ( A -s xO ) ) = A ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO +s ( A -s xO ) ) = A ) with typecode |-
160	159	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO +s ( A -s xO ) ) = A ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO +s ( A -s xO ) ) = A ) with typecode |-
161	160	breq2d	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( xO +s ( 1s /su n ) ) <_s ( xO +s ( A -s xO ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( xO +s ( 1s /su n ) ) <_s ( xO +s ( A -s xO ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
162	155 157 161	3bitrd	Could not format ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
163	162	rexbidva	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
164	163	ralbidva	Could not format ( A e. No -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) : No typesetting found for |- ( A e. No -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) ) with typecode |-
165		absssub	Could not format ( ( A e. No /\ xO e. No ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) ) : No typesetting found for |- ( ( A e. No /\ xO e. No ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) ) with typecode |-
166	55 165	sylan2	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) ) with typecode |-
167	166	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) ) with typecode |-
168		simpl	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A e. No ) with typecode |-
169	56 168	subscld	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( xO -s A ) e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( xO -s A ) e. No ) with typecode |-
170	145	a1i	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s e. No ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s e. No ) with typecode |-
171		rightgt	Could not format ( xO e. ( _Right ` A ) -> A A
172	171	adantl	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A A
173	168 56	posdifsd	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( A 0s ( A 0s
174	172 173	mpbid	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s 0s
175	170 169 174	sltled	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s <_s ( xO -s A ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s <_s ( xO -s A ) ) with typecode |-
176		abssid	Could not format ( ( ( xO -s A ) e. No /\ 0s <_s ( xO -s A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) ) : No typesetting found for |- ( ( ( xO -s A ) e. No /\ 0s <_s ( xO -s A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) ) with typecode |-
177	169 175 176	syl2anc	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) ) with typecode |-
178	177	adantr	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) ) with typecode |-
179	167 178	eqtrd	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( xO -s A ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( xO -s A ) ) with typecode |-
180	179	breq2d	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( xO -s A ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( xO -s A ) ) ) with typecode |-
181	58 57 53	slesubd	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( xO -s A ) <-> A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( xO -s A ) <-> A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
182	180 181	bitrd	Could not format ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
183	182	rexbidva	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
184	183	ralbidva	Could not format ( A e. No -> ( A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) : No typesetting found for |- ( A e. No -> ( A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) with typecode |-
185	164 184	anbi12d	Could not format ( A e. No -> ( ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) /\ A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) ) : No typesetting found for |- ( A e. No -> ( ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) /\ A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) ) with typecode |-
186	142 185	bitrid	Could not format ( A e. No -> ( A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) ) : No typesetting found for |- ( A e. No -> ( A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) ) with typecode |-
187	141 186	bitr4d	Could not format ( A e. No -> ( A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) <-> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) ) : No typesetting found for |- ( A e. No -> ( A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) <-> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) ) with typecode |-
188	187	anbi2d	Could not format ( A e. No -> ( ( E. n e. NN_s ( ( -us ` n ) ( E. n e. NN_s ( ( -us ` n ) ( ( E. n e. NN_s ( ( -us ` n ) ( E. n e. NN_s ( ( -us ` n )
189	188	pm5.32i	Could not format ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n ) ( A e. No /\ ( E. n e. NN_s ( ( -us ` n ) ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
190	1 189	bitri	Could not format ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n ) ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )