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		leftno	Could not format ( xO e. ( _Left ` A ) -> xO e. No ) : No typesetting found for |- ( xO e. ( _Left ` A ) -> xO e. No ) with typecode |-
19	18	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 |-
20	19	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 |-
21		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 |-
22		1no	$$⊢1_s\in \mathrm{No}$$
23	22	a1i	$$⊢n\in {\mathbb{N}}_s\to 1_s\in \mathrm{No}$$
24		nnno	$$⊢n\in {\mathbb{N}}_s\to n\in \mathrm{No}$$
25		nnne0s	$$⊢n\in {\mathbb{N}}_s\to n\ne 0_s$$
26	23 24 25	divscld	$$⊢n\in {\mathbb{N}}_s\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
27	26	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 |-
28	21 27	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 |-
29	20 28 27	leadds1d	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 |-
30		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$$
31	21 27 30	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 |-
32	31	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 |-
33	29 32	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 |-
34	33	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 |-
35	34	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 |-
36	17 35	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 |-
37	36	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 |-
38	5 37	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 |-
39	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 |-
40		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)$$
41	40	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)$$
42	41	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 |-
43		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 |-
44		ovex	$$⊢A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{V}$$
45		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 |-
46	44 45	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 |-
47	46	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 |-
48		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 |-
49	48	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 |-
50	43 47 49	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 |-
51	42 50	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 |-
52		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 |-
53		rightno	Could not format ( xO e. ( _Right ` A ) -> xO e. No ) : No typesetting found for |- ( xO e. ( _Right ` A ) -> xO e. No ) with typecode |-
54	53	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 |-
55	54	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 |-
56	26	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 |-
57	55 56	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 |-
58	52 57 56	leadds1d	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 |-
59		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 |-
60	55 56 59	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 |-
61	60	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 |-
62	58 61	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 |-
63	62	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 |-
64	51 63	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 |-
65	64	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 |-
66	65	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 |-
67	39 66	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 |-
68	38 67	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 |-
69		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
70	69	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 |-
71		lltr	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
72	71	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 ) <
73	34	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 |-
74	73 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 |-
75	74	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 |-
76	75	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 |-
77	76	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 |-
78	77	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 |-
79	63	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 |-
80	79 51	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 |-
81	80	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 |-
82	81	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 |-
83	82	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 |-
84	83	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 |-
85		nnsex	$$⊢{\mathbb{N}}_s\in \mathrm{V}$$
86	85	abrexex	$$⊢\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
87	86	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}$$
88		snexg	$$⊢A\in \mathrm{No}\to \left\{A\right\}\in \mathrm{V}$$
89		simpl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to A\in \mathrm{No}$$
90	26	adantl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
91	89 90	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}$$
92		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)$$
93	91 92	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)$$
94	93	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)$$
95	94	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}$$
96		snssi	$$⊢A\in \mathrm{No}\to \left\{A\right\}\subseteq \mathrm{No}$$
97		biid	$$⊢A\in \mathrm{No}\leftrightarrow A\in \mathrm{No}$$
98		vex	$$⊢y\in \mathrm{V}$$
99	98 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)$$
100		velsn	$$⊢z\in \left\{A\right\}\leftrightarrow z=A$$
101		id	$$⊢n\in {\mathbb{N}}_s\to n\in {\mathbb{N}}_s$$
102	101	nnsrecgt0d	$$⊢n\in {\mathbb{N}}_s\to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
103	102	adantl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_s\right)\to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
104	90 89	ltsubsposd	$$⊢\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)$$
105	103 104	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$$
106		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)$$
107	105 106	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)$$
108	107	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)$$
109	108	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)$$
110	109	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$$
111	97 99 100 110	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$$
112	87 88 95 96 111	sltsd	$$⊢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\}$$
113	69	sneqd	$$⊢A\in \mathrm{No}\to \left\{L\left(A\right){|}_{s}R\left(A\right)\right\}=\left\{A\right\}$$
114	112 113	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\}$$
115	114	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 ) ) } <
116	70	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 |-
117	85	abrexex	$$⊢\left\{w|\exists n\in {\mathbb{N}}_{s}w=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
118	117	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}$$
119	89 90	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}$$
120		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)$$
121	119 120	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)$$
122	121	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)$$
123	122	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}$$
124	98 41	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)$$
125	90 89	ltaddspos1d	$$⊢\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)$$
126	103 125	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)$$
127		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)$$
128	126 127	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)$$
129	128	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)$$
130	129	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)$$
131	130	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)$$
132	131	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$$
133	97 100 124 132	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$$
134	88 118 96 123 133	sltsd	$$⊢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\}$$
135	134	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 } <
136	116 135	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 ) ) } <
137	72 78 84 115 136	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 |-
138	70 137	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 |-
139	68 138	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 |-
140		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 |-
141		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 |-
142	141 19	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 |-
143		0no	$$⊢0_s\in \mathrm{No}$$
144	143	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 |-
145		leftlt	Could not format ( xO e. ( _Left ` A ) -> xO xO
146	145	adantl	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO xO
147	19 141	posdifsd	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO 0s ( xO 0s
148	146 147	mpbid	Could not format ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s 0s
149	144 142 148	ltlesd	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 |-
150		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 |-
151	142 149 150	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 |-
152	151	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 |-
153	152	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 |-
154	142	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 |-
155	27 154 20	leadds2d	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 |-
156		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 |-
157	19 141 156	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 |-
158	157	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 |-
159	158	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 |-
160	153 155 159	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 |-
161	160	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 |-
162	161	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 |-
163		abssubs	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 |-
164	53 163	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 |-
165	164	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 |-
166		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 |-
167	54 166	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 |-
168	143	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 |-
169		rightgt	Could not format ( xO e. ( _Right ` A ) -> A A
170	169	adantl	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A A
171	166 54	posdifsd	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( A 0s ( A 0s
172	170 171	mpbid	Could not format ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s 0s
173	168 167 172	ltlesd	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 |-
174		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 |-
175	167 173 174	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 |-
176	175	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 |-
177	165 176	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 |-
178	177	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 |-
179	56 55 52	lesubsd	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 |-
180	178 179	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 |-
181	180	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 |-
182	181	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 |-
183	162 182	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 |-
184	140 183	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 |-
185	139 184	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 |-
186	185	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 )
187	186	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 )
188	1 187	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 )