Metamath Proof Explorer

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 ( 𝐴 ∈ ℝs ↔ ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 𝐴 -s 𝑥𝑂 ) ) ) ) )

Proof

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