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