Metamath Proof Explorer

Theorem ioodvbdlimc1lem1

Description: If F has bounded derivative on ( A (,) B ) then a sequence of points in its image converges to its limsup . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc1lem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ioodvbdlimc1lem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ioodvbdlimc1lem1.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
ioodvbdlimc1lem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
ioodvbdlimc1lem1.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
ioodvbdlimc1lem1.dvbd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑦 )
ioodvbdlimc1lem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ioodvbdlimc1lem1.r ⊢ ( 𝜑 → 𝑅 : ( ℤ≥ ‘ 𝑀 ) ⟶ ( 𝐴 (,) 𝐵 ) )
ioodvbdlimc1lem1.s ⊢ 𝑆 = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) )
ioodvbdlimc1lem1.rcnv ⊢ ( 𝜑 → 𝑅 ∈ dom ⇝ )
ioodvbdlimc1lem1.k ⊢ 𝐾 = inf ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } , ℝ , < )
Assertion ioodvbdlimc1lem1 ( 𝜑 → 𝑆 ⇝ ( lim sup ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ioodvbdlimc1lem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ioodvbdlimc1lem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ioodvbdlimc1lem1.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 ioodvbdlimc1lem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
5 ioodvbdlimc1lem1.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
6 ioodvbdlimc1lem1.dvbd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑦 )
7 ioodvbdlimc1lem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8 ioodvbdlimc1lem1.r ⊢ ( 𝜑 → 𝑅 : ( ℤ≥ ‘ 𝑀 ) ⟶ ( 𝐴 (,) 𝐵 ) )
9 ioodvbdlimc1lem1.s ⊢ 𝑆 = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) )
10 ioodvbdlimc1lem1.rcnv ⊢ ( 𝜑 → 𝑅 ∈ dom ⇝ )
11 ioodvbdlimc1lem1.k ⊢ 𝐾 = inf ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } , ℝ , < )
12 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
13 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
14 4 13 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
16 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑅 ‘ 𝑗 ) ∈ ( 𝐴 (,) 𝐵 ) )
17 15 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ∈ ℝ )
18 17 9 fmptd ⊢ ( 𝜑 → 𝑆 : ( ℤ≥ ‘ 𝑀 ) ⟶ ℝ )
19 ssrab2 ⊢ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } ⊆ ( ℤ≥ ‘ 𝑀 )
20 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
22 2fveq3 ⊢ ( 𝑧 = 𝑥 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
23 22 cbvmptv ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
24 23 rneqi ⊢ ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) = ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
25 24 supeq1i ⊢ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < )
26 ioomidp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) )
27 1 2 3 26 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) )
28 27 ne0d ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
29 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
30 29 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
31 dvfre ⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
32 14 30 31 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
33 5 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
34 32 33 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
35 ax-resscn ⊢ ℝ ⊆ ℂ
36 35 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
37 34 36 fssd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
38 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
39 38 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ )
40 eqid ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
41 eqid ⊢ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < )
42 28 39 6 40 41 suprnmpt ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ∈ ℝ ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ) )
43 42 simpld ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ∈ ℝ )
44 25 43 eqeltrid ⊢ ( 𝜑 → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ∈ ℝ )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ∈ ℝ )
46 peano2re ⊢ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ∈ ℝ → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ )
48 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
49 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
50 48 49 readdcld ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℝ )
51 44 46 syl ⊢ ( 𝜑 → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ )
52 48 ltp1d ⊢ ( 𝜑 → 0 < ( 0 + 1 ) )
53 37 27 ffvelrnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
54 53 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
55 53 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) )
56 42 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) )
57 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
58 25 a1i ⊢ ( 𝑦 = 𝑥 → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) )
59 57 58 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ↔ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ) )
60 59 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ↔ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) )
61 56 60 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) )
62 2fveq3 ⊢ ( 𝑦 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) )
63 62 breq1d ⊢ ( 𝑦 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ↔ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ) )
64 63 rspcva ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) )
65 27 61 64 syl2anc ⊢ ( 𝜑 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) )
66 48 54 44 55 65 letrd ⊢ ( 𝜑 → 0 ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) )
67 48 44 49 66 leadd1dd ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) )
68 48 50 51 52 67 ltletrd ⊢ ( 𝜑 → 0 < ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) )
69 68 gt0ne0d ⊢ ( 𝜑 → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ≠ 0 )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ≠ 0 )
71 21 47 70 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ∈ ℝ )
72 rpgt0 ⊢ ( 𝑥 ∈ ℝ+ → 0 < 𝑥 )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 < 𝑥 )
74 68 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 < ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) )
75 21 47 73 74 divgt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
76 71 75 elrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ∈ ℝ+ )
77 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
78 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑅 ∈ dom ⇝ )
79 12 climcau ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ dom ⇝ ) → ∀ 𝑤 ∈ ℝ+ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < 𝑤 )
80 77 78 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑤 ∈ ℝ+ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < 𝑤 )
81 breq2 ⊢ ( 𝑤 = ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < 𝑤 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
82 81 rexralbidv ⊢ ( 𝑤 = ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) → ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < 𝑤 ↔ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
83 82 rspcva ⊢ ( ( ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ∈ ℝ+ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < 𝑤 ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
84 76 80 83 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
85 rabn0 ⊢ ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } ≠ ∅ ↔ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
86 84 85 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } ≠ ∅ )
87 infssuzcl ⊢ ( ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } ≠ ∅ ) → inf ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } , ℝ , < ) ∈ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } )
88 19 86 87 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → inf ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } , ℝ , < ) ∈ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } )
89 11 88 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐾 ∈ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } )
90 19 89 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
91 2fveq3 ⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) )
92 uzss ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
93 90 92 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
94 93 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
95 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
96 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑅 : ( ℤ≥ ‘ 𝑀 ) ⟶ ( 𝐴 (,) 𝐵 ) )
97 96 94 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ( 𝐴 (,) 𝐵 ) )
98 95 97 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ∈ ℝ )
99 9 91 94 98 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑆 ‘ 𝑖 ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) )
100 2fveq3 ⊢ ( 𝑗 = 𝐾 → ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) )
101 90 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
102 96 101 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ( 𝐴 (,) 𝐵 ) )
103 95 102 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ∈ ℝ )
104 9 100 101 103 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑆 ‘ 𝐾 ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) )
105 99 104 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) = ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) )
106 105 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) )
107 98 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ∈ ℂ )
108 103 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ∈ ℂ )
109 107 108 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℂ )
110 109 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ∈ ℝ )
111 110 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ∈ ℝ )
112 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ∈ ℝ )
113 112 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ∈ ℝ )
114 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑅 : ( ℤ≥ ‘ 𝑀 ) ⟶ ( 𝐴 (,) 𝐵 ) )
115 114 90 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑅 ‘ 𝐾 ) ∈ ( 𝐴 (,) 𝐵 ) )
116 29 115 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ )
117 116 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ )
118 29 97 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ )
119 118 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ )
120 117 119 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ∈ ℝ )
121 113 120 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) ∈ ℝ )
122 20 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → 𝑥 ∈ ℝ )
123 107 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ∈ ℂ )
124 108 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ∈ ℂ )
125 123 124 abssubd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ) ) )
126 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → 𝐴 ∈ ℝ )
127 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → 𝐵 ∈ ℝ )
128 95 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
129 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
130 61 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) )
131 97 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ( 𝐴 (,) 𝐵 ) )
132 118 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ* )
133 132 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ* )
134 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
135 134 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐵 ∈ ℝ* )
136 135 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → 𝐵 ∈ ℝ* )
137 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) )
138 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℝ* )
140 134 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
141 iooltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑅 ‘ 𝐾 ) ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 ‘ 𝐾 ) < 𝐵 )
142 139 140 115 141 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑅 ‘ 𝐾 ) < 𝐵 )
143 142 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) < 𝐵 )
144 133 136 117 137 143 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ( ( 𝑅 ‘ 𝑖 ) (,) 𝐵 ) )
145 126 127 128 129 113 130 131 144 dvbdfbdioolem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( 𝐵 − 𝐴 ) ) ) )
146 145 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) )
147 125 146 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) )
148 113 46 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ )
149 148 120 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) ∈ ℝ )
150 119 117 posdifd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ↔ 0 < ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) )
151 137 150 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → 0 < ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) )
152 120 151 elrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ∈ ℝ+ )
153 113 ltp1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) < ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) )
154 113 148 152 153 ltmul1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) < ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) )
155 29 102 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ )
156 118 155 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ∈ ℝ )
157 156 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ∈ ℂ )
158 157 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℝ )
159 158 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℝ )
160 71 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ∈ ℝ )
161 120 leabsd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) )
162 117 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ℂ )
163 118 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℂ )
164 163 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℂ )
165 162 164 abssubd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
166 161 165 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
167 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝐾 ) )
168 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝐾 ) )
169 168 oveq2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) = ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) )
170 169 fveq2d ⊢ ( 𝑘 = 𝐾 → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
171 170 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
172 167 171 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
173 172 elrab ⊢ ( 𝐾 ∈ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
174 89 173 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
175 174 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
176 175 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
177 176 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
178 120 159 160 166 177 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
179 51 68 elrpd ⊢ ( 𝜑 → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ+ )
180 179 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ+ )
181 120 122 180 ltmuldiv2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) < 𝑥 ↔ ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
182 178 181 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) < 𝑥 )
183 121 149 122 154 182 lttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝐾 ) − ( 𝑅 ‘ 𝑖 ) ) ) < 𝑥 )
184 111 121 122 147 183 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
185 fveq2 ⊢ ( ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) )
186 185 oveq1d ⊢ ( ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) = ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) )
187 108 subidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) = 0 )
188 186 187 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) = 0 )
189 188 abs00bd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) = 0 )
190 72 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → 0 < 𝑥 )
191 189 190 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
192 191 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
193 simpll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
194 155 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ )
195 118 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ )
196 id ⊢ ( ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑖 ) → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑖 ) )
197 196 eqcomd ⊢ ( ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑖 ) → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) )
198 197 necon3bi ⊢ ( ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) → ( 𝑅 ‘ 𝐾 ) ≠ ( 𝑅 ‘ 𝑖 ) )
199 198 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) ≠ ( 𝑅 ‘ 𝑖 ) )
200 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) )
201 194 195 199 200 lttri5d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) )
202 110 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ∈ ℝ )
203 112 156 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℝ )
204 203 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℝ )
205 20 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 𝑥 ∈ ℝ )
206 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 𝐴 ∈ ℝ )
207 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 𝐵 ∈ ℝ )
208 95 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
209 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
210 44 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) ∈ ℝ )
211 61 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) )
212 102 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ( 𝐴 (,) 𝐵 ) )
213 116 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ* )
214 213 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ* )
215 207 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 𝐵 ∈ ℝ* )
216 118 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ )
217 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) )
218 138 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐴 ∈ ℝ* )
219 iooltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑅 ‘ 𝑖 ) ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑅 ‘ 𝑖 ) < 𝐵 )
220 218 135 97 219 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑖 ) < 𝐵 )
221 220 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝑖 ) < 𝐵 )
222 214 215 216 217 221 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝑖 ) ∈ ( ( 𝑅 ‘ 𝐾 ) (,) 𝐵 ) )
223 206 207 208 209 210 211 212 222 dvbdfbdioolem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( 𝐵 − 𝐴 ) ) ) )
224 223 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) ≤ ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
225 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 1 ∈ ℝ )
226 210 225 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ )
227 155 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑅 ‘ 𝐾 ) ∈ ℝ )
228 216 227 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ∈ ℝ )
229 226 228 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℝ )
230 210 46 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ )
231 227 216 posdifd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ↔ 0 < ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
232 217 231 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → 0 < ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) )
233 228 232 elrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ∈ ℝ+ )
234 210 ltp1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) < ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) )
235 210 230 233 234 ltmul1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
236 158 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) ∈ ℝ )
237 71 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ∈ ℝ )
238 228 leabsd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) )
239 176 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
240 228 236 237 238 239 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
241 179 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ∈ ℝ+ )
242 228 205 241 ltmuldiv2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < 𝑥 ↔ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
243 240 242 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < 𝑥 )
244 204 229 205 235 243 lttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) · ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝐾 ) ) ) < 𝑥 )
245 202 204 205 224 244 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐾 ) < ( 𝑅 ‘ 𝑖 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
246 193 201 245 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
247 192 246 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝑖 ) < ( 𝑅 ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
248 184 247 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝑖 ) ) − ( 𝐹 ‘ ( 𝑅 ‘ 𝐾 ) ) ) ) < 𝑥 )
249 106 248 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) < 𝑥 )
250 249 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) < 𝑥 )
251 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑆 ‘ 𝑘 ) = ( 𝑆 ‘ 𝐾 ) )
252 251 oveq2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) )
253 252 fveq2d ⊢ ( 𝑘 = 𝐾 → ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) )
254 253 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) < 𝑥 ) )
255 167 254 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) ) < 𝑥 ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) < 𝑥 ) )
256 255 rspcev ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝐾 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝐾 ) ) ) < 𝑥 ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) ) < 𝑥 )
257 90 250 256 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) ) < 𝑥 )
258 257 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑆 ‘ 𝑖 ) − ( 𝑆 ‘ 𝑘 ) ) ) < 𝑥 )
259 12 18 258 caurcvg ⊢ ( 𝜑 → 𝑆 ⇝ ( lim sup ‘ 𝑆 ) )