Step | Hyp | Ref
| Expression |
1 | | mettrifi.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 12220 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁))) |
5 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
6 | 5 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) = ((𝐹‘𝑀)𝐷(𝐹‘𝑀))) |
7 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑀 → (𝑥 − 1) = (𝑀 − 1)) |
8 | 7 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝑀...(𝑥 − 1)) = (𝑀...(𝑀 − 1))) |
9 | 8 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
10 | 6, 9 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
11 | 4, 10 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ (𝑀 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
12 | 11 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))))) |
13 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) |
14 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛)) |
15 | 14 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) = ((𝐹‘𝑀)𝐷(𝐹‘𝑛))) |
16 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1)) |
17 | 16 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝑀...(𝑥 − 1)) = (𝑀...(𝑛 − 1))) |
18 | 17 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
19 | 15, 18 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
20 | 13, 19 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ (𝑛 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
21 | 20 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))))) |
22 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁))) |
23 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
24 | 23 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) = ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1)))) |
25 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1)) |
26 | 25 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (𝑀...(𝑥 − 1)) = (𝑀...((𝑛 + 1) − 1))) |
27 | 26 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
28 | 24, 27 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
29 | 22, 28 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
30 | 29 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))))) |
31 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
32 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐹‘𝑥) = (𝐹‘𝑁)) |
33 | 32 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) = ((𝐹‘𝑀)𝐷(𝐹‘𝑁))) |
34 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1)) |
35 | 34 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑀...(𝑥 − 1)) = (𝑀...(𝑁 − 1))) |
36 | 35 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
37 | 33, 36 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
38 | 31, 37 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ (𝑁 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
39 | 38 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))))) |
40 | | 0le0 10987 |
. . . . . . . 8
⊢ 0 ≤
0 |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 0) |
42 | | mettrifi.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
43 | | eluzfz1 12219 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
44 | 1, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
45 | | mettrifi.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑋) |
46 | 45 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ 𝑋) |
47 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
48 | 47 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ 𝑋 ↔ (𝐹‘𝑀) ∈ 𝑋)) |
49 | 48 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ 𝑋 → (𝐹‘𝑀) ∈ 𝑋)) |
50 | 44, 46, 49 | sylc 63 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑋) |
51 | | met0 21958 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑀) ∈ 𝑋) → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) = 0) |
52 | 42, 50, 51 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) = 0) |
53 | | eluzel2 11568 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
55 | 54 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
56 | 55 | ltm1d 10835 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
57 | | peano2zm 11297 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
58 | 54, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
59 | | fzn 12228 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
60 | 54, 58, 59 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
61 | 56, 60 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
62 | 61 | sumeq1d 14279 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ ∅ ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
63 | | sum0 14299 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = 0 |
64 | 62, 63 | syl6eq 2660 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = 0) |
65 | 41, 52, 64 | 3brtr4d 4615 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
66 | 65 | a1d 25 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
67 | 66 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ ℤ → (𝜑 → (𝑀 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
68 | | peano2fzr 12225 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) |
69 | 68 | ex 449 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁))) |
70 | 69 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁))) |
71 | 70 | imim1d 80 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
72 | 42 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝐷 ∈ (Met‘𝑋)) |
73 | 50 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹‘𝑀) ∈ 𝑋) |
74 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
75 | 46 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ 𝑋) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
77 | 76 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ 𝑋 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑋)) |
78 | 77 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ 𝑋 → (𝐹‘(𝑛 + 1)) ∈ 𝑋)) |
79 | 74, 75, 78 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑛 + 1)) ∈ 𝑋) |
80 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
81 | 80 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ 𝑋 ↔ (𝐹‘𝑛) ∈ 𝑋)) |
82 | 81 | cbvralv 3147 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(𝑀...𝑁)(𝐹‘𝑘) ∈ 𝑋 ↔ ∀𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ∈ 𝑋) |
83 | 75, 82 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ∈ 𝑋) |
84 | 70 | 3impia 1253 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) |
85 | | rsp 2913 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
(𝑀...𝑁)(𝐹‘𝑛) ∈ 𝑋 → (𝑛 ∈ (𝑀...𝑁) → (𝐹‘𝑛) ∈ 𝑋)) |
86 | 83, 84, 85 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹‘𝑛) ∈ 𝑋) |
87 | | mettri 21967 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘𝑀) ∈ 𝑋 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋)) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1))))) |
88 | 72, 73, 79, 86, 87 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1))))) |
89 | | metcl 21947 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑀) ∈ 𝑋 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑋) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ) |
90 | 72, 73, 79, 89 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ) |
91 | | metcl 21947 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑀) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ∈ ℝ) |
92 | 72, 73, 86, 91 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ∈ ℝ) |
93 | | metcl 21947 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑋) → ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ) |
94 | 72, 86, 79, 93 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ) |
95 | 92, 94 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∈ ℝ) |
96 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...𝑛) ∈ Fin) |
97 | 72 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐷 ∈ (Met‘𝑋)) |
98 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) |
99 | 84, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑛)) |
100 | | fzss2 12252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑛) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) |
102 | 101 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ (𝑀...𝑁)) |
103 | 45 | 3ad2antl1 1216 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑋) |
104 | 102, 103 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹‘𝑘) ∈ 𝑋) |
105 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ (ℤ≥‘𝑀)) |
106 | 105 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
107 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝑘 + 1) ∈
(ℤ≥‘𝑀)) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝑘 + 1) ∈
(ℤ≥‘𝑀)) |
109 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
110 | 74, 109 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
111 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
112 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (𝑀...𝑛) → 𝑛 ∈ (ℤ≥‘𝑘)) |
113 | 112 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑘)) |
114 | | eluzp1p1 11589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘𝑘) → (𝑛 + 1) ∈
(ℤ≥‘(𝑘 + 1))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝑛 + 1) ∈
(ℤ≥‘(𝑘 + 1))) |
116 | | uztrn 11580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘(𝑛 + 1)) ∧ (𝑛 + 1) ∈
(ℤ≥‘(𝑘 + 1))) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) |
117 | 111, 115,
116 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) |
118 | | elfzuzb 12207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘(𝑘 + 1)))) |
119 | 108, 117,
118 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
120 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑘 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
121 | 120 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → ((𝐹‘𝑛) ∈ 𝑋 ↔ (𝐹‘(𝑘 + 1)) ∈ 𝑋)) |
122 | 121 | rspccva 3281 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
(𝑀...𝑁)(𝐹‘𝑛) ∈ 𝑋 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑋) |
123 | 83, 122 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑋) |
124 | 119, 123 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹‘(𝑘 + 1)) ∈ 𝑋) |
125 | | metcl 21947 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
126 | 97, 104, 124, 125 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
127 | 96, 126 | fsumrecl 14312 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
128 | | letr 10010 |
. . . . . . . . . . . 12
⊢ ((((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ ∧ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∈ ℝ ∧ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) → ((((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∧ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
129 | 90, 95, 127, 128 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∧ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
130 | 88, 129 | mpand 707 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
131 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...(𝑛 − 1)) ∈ Fin) |
132 | | fzssp1 12255 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀...(𝑛 − 1)) ⊆ (𝑀...((𝑛 − 1) + 1)) |
133 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
134 | 133 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ ℤ) |
135 | 134 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ ℂ) |
136 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
137 | | npcan 10169 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
138 | 135, 136,
137 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝑛 − 1) + 1) = 𝑛) |
139 | 138 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...((𝑛 − 1) + 1)) = (𝑀...𝑛)) |
140 | 132, 139 | syl5sseq 3616 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...(𝑛 − 1)) ⊆ (𝑀...𝑛)) |
141 | 140 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...(𝑛 − 1))) → 𝑘 ∈ (𝑀...𝑛)) |
142 | 141, 126 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...(𝑛 − 1))) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
143 | 131, 142 | fsumrecl 14312 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
144 | 92, 143, 94 | leadd1d 10500 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ (Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))))) |
145 | | simp2 1055 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
146 | 126 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℂ) |
147 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
148 | 147 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
149 | 80, 148 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
150 | 145, 146,
149 | fsumm1 14324 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = (Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1))))) |
151 | 150 | breq2d 4595 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ (Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))))) |
152 | 144, 151 | bitr4d 270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
153 | | pncan 10166 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
154 | 135, 136,
153 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝑛 + 1) − 1) = 𝑛) |
155 | 154 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...((𝑛 + 1) − 1)) = (𝑀...𝑛)) |
156 | 155 | sumeq1d 14279 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
157 | 156 | breq2d 4595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
158 | 130, 152,
157 | 3imtr4d 282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
159 | 158 | 3expia 1259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
160 | 159 | a2d 29 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
161 | 71, 160 | syld 46 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
162 | 161 | expcom 450 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝑛 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))))) |
163 | 162 | a2d 29 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))))) |
164 | 12, 21, 30, 39, 67, 163 | uzind4 11622 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))))) |
165 | 1, 164 | mpcom 37 |
. 2
⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))) |
166 | 3, 165 | mpd 15 |
1
⊢ (𝜑 → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |