| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bfp.2 | . . 3
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) | 
| 2 |  | cmetmet 25321 | . . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 4 |  | nnuz 12922 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 5 |  | bfp.10 | . . . . 5
⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ ×
{𝐴})) | 
| 6 |  | 1zzd 12650 | . . . . 5
⊢ (𝜑 → 1 ∈
ℤ) | 
| 7 |  | bfp.9 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 8 |  | bfp.6 | . . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶𝑋) | 
| 9 | 4, 5, 6, 7, 8 | algrf 16611 | . . . 4
⊢ (𝜑 → 𝐺:ℕ⟶𝑋) | 
| 10 | 8, 7 | ffvelcdmd 7104 | . . . . . 6
⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑋) | 
| 11 |  | metcl 24343 | . . . . . 6
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝐴) ∈ 𝑋) → (𝐴𝐷(𝐹‘𝐴)) ∈ ℝ) | 
| 12 | 3, 7, 10, 11 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐴𝐷(𝐹‘𝐴)) ∈ ℝ) | 
| 13 |  | bfp.4 | . . . . 5
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 14 | 12, 13 | rerpdivcld 13109 | . . . 4
⊢ (𝜑 → ((𝐴𝐷(𝐹‘𝐴)) / 𝐾) ∈ ℝ) | 
| 15 |  | bfp.5 | . . . 4
⊢ (𝜑 → 𝐾 < 1) | 
| 16 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑗 = 1 → (𝐺‘𝑗) = (𝐺‘1)) | 
| 17 |  | fvoveq1 7455 | . . . . . . . . 9
⊢ (𝑗 = 1 → (𝐺‘(𝑗 + 1)) = (𝐺‘(1 + 1))) | 
| 18 | 16, 17 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑗 = 1 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) = ((𝐺‘1)𝐷(𝐺‘(1 + 1)))) | 
| 19 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑗 = 1 → (𝐾↑𝑗) = (𝐾↑1)) | 
| 20 | 19 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑗 = 1 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1))) | 
| 21 | 18, 20 | breq12d 5155 | . . . . . . 7
⊢ (𝑗 = 1 → (((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) ↔ ((𝐺‘1)𝐷(𝐺‘(1 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)))) | 
| 22 | 21 | imbi2d 340 | . . . . . 6
⊢ (𝑗 = 1 → ((𝜑 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗))) ↔ (𝜑 → ((𝐺‘1)𝐷(𝐺‘(1 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1))))) | 
| 23 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝐺‘𝑗) = (𝐺‘𝑘)) | 
| 24 |  | fvoveq1 7455 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝐺‘(𝑗 + 1)) = (𝐺‘(𝑘 + 1))) | 
| 25 | 23, 24 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) = ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) | 
| 26 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝐾↑𝑗) = (𝐾↑𝑘)) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))) | 
| 28 | 25, 27 | breq12d 5155 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) ↔ ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)))) | 
| 29 | 28 | imbi2d 340 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝜑 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗))) ↔ (𝜑 → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))))) | 
| 30 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐺‘𝑗) = (𝐺‘(𝑘 + 1))) | 
| 31 |  | fvoveq1 7455 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐺‘(𝑗 + 1)) = (𝐺‘((𝑘 + 1) + 1))) | 
| 32 | 30, 31 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) = ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1)))) | 
| 33 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐾↑𝑗) = (𝐾↑(𝑘 + 1))) | 
| 34 | 33 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))) | 
| 35 | 32, 34 | breq12d 5155 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) ↔ ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 36 | 35 | imbi2d 340 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗))) ↔ (𝜑 → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))) | 
| 37 | 12 | leidd 11830 | . . . . . . 7
⊢ (𝜑 → (𝐴𝐷(𝐹‘𝐴)) ≤ (𝐴𝐷(𝐹‘𝐴))) | 
| 38 | 4, 5, 6, 7 | algr0 16610 | . . . . . . . 8
⊢ (𝜑 → (𝐺‘1) = 𝐴) | 
| 39 |  | 1nn 12278 | . . . . . . . . . 10
⊢ 1 ∈
ℕ | 
| 40 | 4, 5, 6, 7, 8 | algrp1 16612 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ∈ ℕ) →
(𝐺‘(1 + 1)) = (𝐹‘(𝐺‘1))) | 
| 41 | 39, 40 | mpan2 691 | . . . . . . . . 9
⊢ (𝜑 → (𝐺‘(1 + 1)) = (𝐹‘(𝐺‘1))) | 
| 42 | 38 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘1)) = (𝐹‘𝐴)) | 
| 43 | 41, 42 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (𝐺‘(1 + 1)) = (𝐹‘𝐴)) | 
| 44 | 38, 43 | oveq12d 7450 | . . . . . . 7
⊢ (𝜑 → ((𝐺‘1)𝐷(𝐺‘(1 + 1))) = (𝐴𝐷(𝐹‘𝐴))) | 
| 45 | 13 | rpred 13078 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 46 | 45 | recnd 11290 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℂ) | 
| 47 | 46 | exp1d 14182 | . . . . . . . . 9
⊢ (𝜑 → (𝐾↑1) = 𝐾) | 
| 48 | 47 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · 𝐾)) | 
| 49 | 12 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → (𝐴𝐷(𝐹‘𝐴)) ∈ ℂ) | 
| 50 | 13 | rpne0d 13083 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ≠ 0) | 
| 51 | 49, 46, 50 | divcan1d 12045 | . . . . . . . 8
⊢ (𝜑 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · 𝐾) = (𝐴𝐷(𝐹‘𝐴))) | 
| 52 | 48, 51 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)) = (𝐴𝐷(𝐹‘𝐴))) | 
| 53 | 37, 44, 52 | 3brtr4d 5174 | . . . . . 6
⊢ (𝜑 → ((𝐺‘1)𝐷(𝐺‘(1 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1))) | 
| 54 | 9 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ 𝑋) | 
| 55 |  | peano2nn 12279 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) | 
| 56 |  | ffvelcdm 7100 | . . . . . . . . . . . . 13
⊢ ((𝐺:ℕ⟶𝑋 ∧ (𝑘 + 1) ∈ ℕ) → (𝐺‘(𝑘 + 1)) ∈ 𝑋) | 
| 57 | 9, 55, 56 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘(𝑘 + 1)) ∈ 𝑋) | 
| 58 | 54, 57 | jca 511 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘) ∈ 𝑋 ∧ (𝐺‘(𝑘 + 1)) ∈ 𝑋)) | 
| 59 |  | bfp.7 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 60 | 59 | ralrimivva 3201 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 61 | 60 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 62 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘))) | 
| 63 | 62 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝐺‘𝑘) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦))) | 
| 64 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐺‘𝑘) → (𝑥𝐷𝑦) = ((𝐺‘𝑘)𝐷𝑦)) | 
| 65 | 64 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝐺‘𝑘) → (𝐾 · (𝑥𝐷𝑦)) = (𝐾 · ((𝐺‘𝑘)𝐷𝑦))) | 
| 66 | 63, 65 | breq12d 5155 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑘) → (((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑘)𝐷𝑦)))) | 
| 67 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → (𝐹‘𝑦) = (𝐹‘(𝐺‘(𝑘 + 1)))) | 
| 68 | 67 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1))))) | 
| 69 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → ((𝐺‘𝑘)𝐷𝑦) = ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) | 
| 70 | 69 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → (𝐾 · ((𝐺‘𝑘)𝐷𝑦)) = (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))) | 
| 71 | 68, 70 | breq12d 5155 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → (((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑘)𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))))) | 
| 72 | 66, 71 | rspc2v 3632 | . . . . . . . . . . 11
⊢ (((𝐺‘𝑘) ∈ 𝑋 ∧ (𝐺‘(𝑘 + 1)) ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))))) | 
| 73 | 58, 61, 72 | sylc 65 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))) | 
| 74 | 3 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋)) | 
| 75 | 8 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:𝑋⟶𝑋) | 
| 76 | 75, 54 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑋) | 
| 77 | 75, 57 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝐺‘(𝑘 + 1))) ∈ 𝑋) | 
| 78 |  | metcl 24343 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘(𝐺‘𝑘)) ∈ 𝑋 ∧ (𝐹‘(𝐺‘(𝑘 + 1))) ∈ 𝑋) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ∈ ℝ) | 
| 79 | 74, 76, 77, 78 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ∈ ℝ) | 
| 80 | 45 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐾 ∈ ℝ) | 
| 81 |  | metcl 24343 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐺‘𝑘) ∈ 𝑋 ∧ (𝐺‘(𝑘 + 1)) ∈ 𝑋) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℝ) | 
| 82 | 74, 54, 57, 81 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℝ) | 
| 83 | 80, 82 | remulcld 11292 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∈ ℝ) | 
| 84 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝐴)) / 𝐾) ∈ ℝ) | 
| 85 | 55 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) | 
| 86 | 85 | nnnn0d 12589 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈
ℕ0) | 
| 87 | 80, 86 | reexpcld 14204 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑(𝑘 + 1)) ∈ ℝ) | 
| 88 | 84, 87 | remulcld 11292 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) ∈ ℝ) | 
| 89 |  | letr 11356 | . . . . . . . . . . 11
⊢ ((((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ∈ ℝ ∧ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∈ ℝ ∧ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) ∈ ℝ) → ((((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∧ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 90 | 79, 83, 88, 89 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∧ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 91 | 73, 90 | mpand 695 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 92 |  | nnnn0 12535 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 93 |  | reexpcl 14120 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐾↑𝑘) ∈
ℝ) | 
| 94 | 45, 92, 93 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑𝑘) ∈ ℝ) | 
| 95 | 84, 94 | remulcld 11292 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ∈ ℝ) | 
| 96 | 13 | rpgt0d 13081 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐾) | 
| 97 | 96 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < 𝐾) | 
| 98 |  | lemul1 12120 | . . . . . . . . . . 11
⊢ ((((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℝ ∧ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ∈ ℝ ∧ (𝐾 ∈ ℝ ∧ 0 < 𝐾)) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ↔ (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) ≤ ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾))) | 
| 99 | 82, 95, 80, 97, 98 | syl112anc 1375 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ↔ (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) ≤ ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾))) | 
| 100 | 82 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℂ) | 
| 101 | 46 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐾 ∈ ℂ) | 
| 102 | 100, 101 | mulcomd 11283 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) = (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))) | 
| 103 | 84 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝐴)) / 𝐾) ∈ ℂ) | 
| 104 | 94 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑𝑘) ∈ ℂ) | 
| 105 | 103, 104,
101 | mulassd 11285 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · ((𝐾↑𝑘) · 𝐾))) | 
| 106 |  | expp1 14110 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐾↑(𝑘 + 1)) = ((𝐾↑𝑘) · 𝐾)) | 
| 107 | 46, 92, 106 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑(𝑘 + 1)) = ((𝐾↑𝑘) · 𝐾)) | 
| 108 | 107 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · ((𝐾↑𝑘) · 𝐾))) | 
| 109 | 105, 108 | eqtr4d 2779 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))) | 
| 110 | 102, 109 | breq12d 5155 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) ≤ ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾) ↔ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 111 | 99, 110 | bitrd 279 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ↔ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 112 | 4, 5, 6, 7, 8 | algrp1 16612 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘(𝑘 + 1)) = (𝐹‘(𝐺‘𝑘))) | 
| 113 | 4, 5, 6, 7, 8 | algrp1 16612 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ) → (𝐺‘((𝑘 + 1) + 1)) = (𝐹‘(𝐺‘(𝑘 + 1)))) | 
| 114 | 55, 113 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((𝑘 + 1) + 1)) = (𝐹‘(𝐺‘(𝑘 + 1)))) | 
| 115 | 112, 114 | oveq12d 7450 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) = ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1))))) | 
| 116 | 115 | breq1d 5152 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) ↔ ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 117 | 91, 111, 116 | 3imtr4d 294 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))) | 
| 118 | 117 | expcom 413 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝜑 → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))) | 
| 119 | 118 | a2d 29 | . . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝜑 → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))) → (𝜑 → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))) | 
| 120 | 22, 29, 36, 29, 53, 119 | nnind 12285 | . . . . 5
⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)))) | 
| 121 | 120 | impcom 407 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))) | 
| 122 | 3, 9, 14, 13, 15, 121 | geomcau 37767 | . . 3
⊢ (𝜑 → 𝐺 ∈ (Cau‘𝐷)) | 
| 123 |  | bfp.8 | . . . 4
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 124 | 123 | cmetcau 25324 | . . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐺 ∈ (Cau‘𝐷)) → 𝐺 ∈ dom
(⇝𝑡‘𝐽)) | 
| 125 | 1, 122, 124 | syl2anc 584 | . 2
⊢ (𝜑 → 𝐺 ∈ dom
(⇝𝑡‘𝐽)) | 
| 126 |  | metxmet 24345 | . . . 4
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 127 | 123 | methaus 24534 | . . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) | 
| 128 | 3, 126, 127 | 3syl 18 | . . 3
⊢ (𝜑 → 𝐽 ∈ Haus) | 
| 129 |  | lmfun 23390 | . . 3
⊢ (𝐽 ∈ Haus → Fun
(⇝𝑡‘𝐽)) | 
| 130 |  | funfvbrb 7070 | . . 3
⊢ (Fun
(⇝𝑡‘𝐽) → (𝐺 ∈ dom
(⇝𝑡‘𝐽) ↔ 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺))) | 
| 131 | 128, 129,
130 | 3syl 18 | . 2
⊢ (𝜑 → (𝐺 ∈ dom
(⇝𝑡‘𝐽) ↔ 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺))) | 
| 132 | 125, 131 | mpbid 232 | 1
⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) |