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