Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mettrifi Structured version   Visualization version   GIF version

Theorem mettrifi 37743
Description: Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
Hypotheses
Ref Expression
mettrifi.2 (𝜑𝐷 ∈ (Met‘𝑋))
mettrifi.3 (𝜑𝑁 ∈ (ℤ𝑀))
mettrifi.4 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹𝑘) ∈ 𝑋)
Assertion
Ref Expression
mettrifi (𝜑 → ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
Distinct variable groups:   𝐷,𝑘   𝑘,𝐹   𝑘,𝑀   𝑘,𝑁   𝜑,𝑘   𝑘,𝑋

Proof of Theorem mettrifi
Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mettrifi.3 . . 3 (𝜑𝑁 ∈ (ℤ𝑀))
2 eluzfz2 13568 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
31, 2syl 17 . 2 (𝜑𝑁 ∈ (𝑀...𝑁))
4 eleq1 2826 . . . . . 6 (𝑥 = 𝑀 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁)))
5 fveq2 6906 . . . . . . . 8 (𝑥 = 𝑀 → (𝐹𝑥) = (𝐹𝑀))
65oveq2d 7446 . . . . . . 7 (𝑥 = 𝑀 → ((𝐹𝑀)𝐷(𝐹𝑥)) = ((𝐹𝑀)𝐷(𝐹𝑀)))
7 oveq1 7437 . . . . . . . . 9 (𝑥 = 𝑀 → (𝑥 − 1) = (𝑀 − 1))
87oveq2d 7446 . . . . . . . 8 (𝑥 = 𝑀 → (𝑀...(𝑥 − 1)) = (𝑀...(𝑀 − 1)))
98sumeq1d 15732 . . . . . . 7 (𝑥 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
106, 9breq12d 5160 . . . . . 6 (𝑥 = 𝑀 → (((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹𝑀)𝐷(𝐹𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
114, 10imbi12d 344 . . . . 5 (𝑥 = 𝑀 → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ (𝑀 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
1211imbi2d 340 . . . 4 (𝑥 = 𝑀 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))))
13 eleq1 2826 . . . . . 6 (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁)))
14 fveq2 6906 . . . . . . . 8 (𝑥 = 𝑛 → (𝐹𝑥) = (𝐹𝑛))
1514oveq2d 7446 . . . . . . 7 (𝑥 = 𝑛 → ((𝐹𝑀)𝐷(𝐹𝑥)) = ((𝐹𝑀)𝐷(𝐹𝑛)))
16 oveq1 7437 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
1716oveq2d 7446 . . . . . . . 8 (𝑥 = 𝑛 → (𝑀...(𝑥 − 1)) = (𝑀...(𝑛 − 1)))
1817sumeq1d 15732 . . . . . . 7 (𝑥 = 𝑛 → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
1915, 18breq12d 5160 . . . . . 6 (𝑥 = 𝑛 → (((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
2013, 19imbi12d 344 . . . . 5 (𝑥 = 𝑛 → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ (𝑛 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
2120imbi2d 340 . . . 4 (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))))
22 eleq1 2826 . . . . . 6 (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁)))
23 fveq2 6906 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (𝐹𝑥) = (𝐹‘(𝑛 + 1)))
2423oveq2d 7446 . . . . . . 7 (𝑥 = (𝑛 + 1) → ((𝐹𝑀)𝐷(𝐹𝑥)) = ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))))
25 oveq1 7437 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
2625oveq2d 7446 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (𝑀...(𝑥 − 1)) = (𝑀...((𝑛 + 1) − 1)))
2726sumeq1d 15732 . . . . . . 7 (𝑥 = (𝑛 + 1) → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
2824, 27breq12d 5160 . . . . . 6 (𝑥 = (𝑛 + 1) → (((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
2922, 28imbi12d 344 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
3029imbi2d 340 . . . 4 (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))))
31 eleq1 2826 . . . . . 6 (𝑥 = 𝑁 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
32 fveq2 6906 . . . . . . . 8 (𝑥 = 𝑁 → (𝐹𝑥) = (𝐹𝑁))
3332oveq2d 7446 . . . . . . 7 (𝑥 = 𝑁 → ((𝐹𝑀)𝐷(𝐹𝑥)) = ((𝐹𝑀)𝐷(𝐹𝑁)))
34 oveq1 7437 . . . . . . . . 9 (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
3534oveq2d 7446 . . . . . . . 8 (𝑥 = 𝑁 → (𝑀...(𝑥 − 1)) = (𝑀...(𝑁 − 1)))
3635sumeq1d 15732 . . . . . . 7 (𝑥 = 𝑁 → Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
3733, 36breq12d 5160 . . . . . 6 (𝑥 = 𝑁 → (((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
3831, 37imbi12d 344 . . . . 5 (𝑥 = 𝑁 → ((𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) ↔ (𝑁 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
3938imbi2d 340 . . . 4 (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑥)) ≤ Σ𝑘 ∈ (𝑀...(𝑥 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))))
40 0le0 12364 . . . . . . . 8 0 ≤ 0
4140a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 0)
42 mettrifi.2 . . . . . . . 8 (𝜑𝐷 ∈ (Met‘𝑋))
43 eluzfz1 13567 . . . . . . . . . 10 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
441, 43syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (𝑀...𝑁))
45 mettrifi.4 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹𝑘) ∈ 𝑋)
4645ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹𝑘) ∈ 𝑋)
47 fveq2 6906 . . . . . . . . . . 11 (𝑘 = 𝑀 → (𝐹𝑘) = (𝐹𝑀))
4847eleq1d 2823 . . . . . . . . . 10 (𝑘 = 𝑀 → ((𝐹𝑘) ∈ 𝑋 ↔ (𝐹𝑀) ∈ 𝑋))
4948rspcv 3617 . . . . . . . . 9 (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹𝑘) ∈ 𝑋 → (𝐹𝑀) ∈ 𝑋))
5044, 46, 49sylc 65 . . . . . . . 8 (𝜑 → (𝐹𝑀) ∈ 𝑋)
51 met0 24368 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑀) ∈ 𝑋) → ((𝐹𝑀)𝐷(𝐹𝑀)) = 0)
5242, 50, 51syl2anc 584 . . . . . . 7 (𝜑 → ((𝐹𝑀)𝐷(𝐹𝑀)) = 0)
53 eluzel2 12880 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
541, 53syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
5554zred 12719 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
5655ltm1d 12197 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) < 𝑀)
57 peano2zm 12657 . . . . . . . . . . 11 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
58 fzn 13576 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
5954, 57, 58syl2anc2 585 . . . . . . . . . 10 (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
6056, 59mpbid 232 . . . . . . . . 9 (𝜑 → (𝑀...(𝑀 − 1)) = ∅)
6160sumeq1d 15732 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ ∅ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
62 sum0 15753 . . . . . . . 8 Σ𝑘 ∈ ∅ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = 0
6361, 62eqtrdi 2790 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = 0)
6441, 52, 633brtr4d 5179 . . . . . 6 (𝜑 → ((𝐹𝑀)𝐷(𝐹𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
6564a1d 25 . . . . 5 (𝜑 → (𝑀 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
6665a1i 11 . . . 4 (𝑀 ∈ ℤ → (𝜑 → (𝑀 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑀)) ≤ Σ𝑘 ∈ (𝑀...(𝑀 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
67 peano2fzr 13573 . . . . . . . . . 10 ((𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁))
6867ex 412 . . . . . . . . 9 (𝑛 ∈ (ℤ𝑀) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁)))
6968adantl 481 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁)))
7069imim1d 82 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
71423ad2ant1 1132 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝐷 ∈ (Met‘𝑋))
72503ad2ant1 1132 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹𝑀) ∈ 𝑋)
73 simp3 1137 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑛 + 1) ∈ (𝑀...𝑁))
74463ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹𝑘) ∈ 𝑋)
75 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑘 = (𝑛 + 1) → (𝐹𝑘) = (𝐹‘(𝑛 + 1)))
7675eleq1d 2823 . . . . . . . . . . . . . 14 (𝑘 = (𝑛 + 1) → ((𝐹𝑘) ∈ 𝑋 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑋))
7776rspcv 3617 . . . . . . . . . . . . 13 ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹𝑘) ∈ 𝑋 → (𝐹‘(𝑛 + 1)) ∈ 𝑋))
7873, 74, 77sylc 65 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑛 + 1)) ∈ 𝑋)
79 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
8079eleq1d 2823 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((𝐹𝑘) ∈ 𝑋 ↔ (𝐹𝑛) ∈ 𝑋))
8180cbvralvw 3234 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (𝑀...𝑁)(𝐹𝑘) ∈ 𝑋 ↔ ∀𝑛 ∈ (𝑀...𝑁)(𝐹𝑛) ∈ 𝑋)
8274, 81sylib 218 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (𝑀...𝑁)(𝐹𝑛) ∈ 𝑋)
83693impia 1116 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁))
84 rsp 3244 . . . . . . . . . . . . 13 (∀𝑛 ∈ (𝑀...𝑁)(𝐹𝑛) ∈ 𝑋 → (𝑛 ∈ (𝑀...𝑁) → (𝐹𝑛) ∈ 𝑋))
8582, 83, 84sylc 65 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹𝑛) ∈ 𝑋)
86 mettri 24377 . . . . . . . . . . . 12 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹𝑀) ∈ 𝑋 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋)) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))))
8771, 72, 78, 85, 86syl13anc 1371 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))))
88 metcl 24357 . . . . . . . . . . . . 13 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑀) ∈ 𝑋 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑋) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ)
8971, 72, 78, 88syl3anc 1370 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ)
90 metcl 24357 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑀) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → ((𝐹𝑀)𝐷(𝐹𝑛)) ∈ ℝ)
9171, 72, 85, 90syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹𝑀)𝐷(𝐹𝑛)) ∈ ℝ)
92 metcl 24357 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑛) ∈ 𝑋 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑋) → ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ)
9371, 85, 78, 92syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ)
9491, 93readdcld 11287 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∈ ℝ)
95 fzfid 14010 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...𝑛) ∈ Fin)
9671adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐷 ∈ (Met‘𝑋))
97 elfzuz3 13557 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝑛))
9883, 97syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ𝑛))
99 fzss2 13600 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑛) → (𝑀...𝑛) ⊆ (𝑀...𝑁))
10098, 99syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...𝑛) ⊆ (𝑀...𝑁))
101100sselda 3994 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ (𝑀...𝑁))
102453ad2antl1 1184 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹𝑘) ∈ 𝑋)
103101, 102syldan 591 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹𝑘) ∈ 𝑋)
104 elfzuz 13556 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ (ℤ𝑀))
105104adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ (ℤ𝑀))
106 peano2uz 12940 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ𝑀) → (𝑘 + 1) ∈ (ℤ𝑀))
107105, 106syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝑘 + 1) ∈ (ℤ𝑀))
108 elfzuz3 13557 . . . . . . . . . . . . . . . . . . 19 ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
10973, 108syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
110109adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑁 ∈ (ℤ‘(𝑛 + 1)))
111 elfzuz3 13557 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝑀...𝑛) → 𝑛 ∈ (ℤ𝑘))
112111adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑛 ∈ (ℤ𝑘))
113 eluzp1p1 12903 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ𝑘) → (𝑛 + 1) ∈ (ℤ‘(𝑘 + 1)))
114112, 113syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝑛 + 1) ∈ (ℤ‘(𝑘 + 1)))
115 uztrn 12893 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘(𝑛 + 1)) ∧ (𝑛 + 1) ∈ (ℤ‘(𝑘 + 1))) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
116110, 114, 115syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
117 elfzuzb 13554 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ‘(𝑘 + 1))))
118107, 116, 117sylanbrc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝑘 + 1) ∈ (𝑀...𝑁))
119 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑘 + 1) → (𝐹𝑛) = (𝐹‘(𝑘 + 1)))
120119eleq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → ((𝐹𝑛) ∈ 𝑋 ↔ (𝐹‘(𝑘 + 1)) ∈ 𝑋))
121120rspccva 3620 . . . . . . . . . . . . . . . 16 ((∀𝑛 ∈ (𝑀...𝑁)(𝐹𝑛) ∈ 𝑋 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
12282, 121sylan 580 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
123118, 122syldan 591 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
124 metcl 24357 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
12596, 103, 123, 124syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
12695, 125fsumrecl 15766 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
127 letr 11352 . . . . . . . . . . . 12 ((((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ∈ ℝ ∧ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∈ ℝ ∧ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) → ((((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∧ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
12889, 94, 126, 127syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ∧ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
12987, 128mpand 695 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
130 fzfid 14010 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...(𝑛 − 1)) ∈ Fin)
131 fzssp1 13603 . . . . . . . . . . . . . . . 16 (𝑀...(𝑛 − 1)) ⊆ (𝑀...((𝑛 − 1) + 1))
132 eluzelz 12885 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ𝑀) → 𝑛 ∈ ℤ)
1331323ad2ant2 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ ℤ)
134133zcnd 12720 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ ℂ)
135 ax-1cn 11210 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
136 npcan 11514 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
137134, 135, 136sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝑛 − 1) + 1) = 𝑛)
138137oveq2d 7446 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...((𝑛 − 1) + 1)) = (𝑀...𝑛))
139131, 138sseqtrid 4047 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...(𝑛 − 1)) ⊆ (𝑀...𝑛))
140139sselda 3994 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...(𝑛 − 1))) → 𝑘 ∈ (𝑀...𝑛))
141140, 125syldan 591 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...(𝑛 − 1))) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
142130, 141fsumrecl 15766 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
14391, 142, 93leadd1d 11854 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ (Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1))))))
144 simp2 1136 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (ℤ𝑀))
145125recnd 11286 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℂ)
146 fvoveq1 7453 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1)))
14779, 146oveq12d 7448 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1))))
148144, 145, 147fsumm1 15783 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = (Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))))
149148breq2d 5159 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ (Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1))))))
150143, 149bitr4d 282 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ (((𝐹𝑀)𝐷(𝐹𝑛)) + ((𝐹𝑛)𝐷(𝐹‘(𝑛 + 1)))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
151 pncan 11511 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
152134, 135, 151sylancl 586 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → ((𝑛 + 1) − 1) = 𝑛)
153152oveq2d 7446 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝑀...((𝑛 + 1) − 1)) = (𝑀...𝑛))
154153sumeq1d 15732 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) = Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
155154breq2d 5159 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ↔ ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...𝑛)((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
156129, 150, 1553imtr4d 294 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
1571563expia 1120 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
158157a2d 29 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑀)) → (((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
15970, 158syld 47 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
160159expcom 413 . . . . 5 (𝑛 ∈ (ℤ𝑀) → (𝜑 → ((𝑛 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))))
161160a2d 29 . . . 4 (𝑛 ∈ (ℤ𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑀...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹‘(𝑛 + 1))) ≤ Σ𝑘 ∈ (𝑀...((𝑛 + 1) − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))))
16212, 21, 30, 39, 66, 161uzind4 12945 . . 3 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))))
1631, 162mpcom 38 . 2 (𝜑 → (𝑁 ∈ (𝑀...𝑁) → ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1)))))
1643, 163mpd 15 1 (𝜑 → ((𝐹𝑀)𝐷(𝐹𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wral 3058  wss 3962  c0 4338   class class class wbr 5147  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   < clt 11292  cle 11293  cmin 11489  cz 12610  cuz 12875  ...cfz 13543  Σcsu 15718  Metcmet 21367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-xadd 13152  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-xmet 21374  df-met 21375
This theorem is referenced by:  geomcau  37745
  Copyright terms: Public domain W3C validator