This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mettrifi

Description: Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Hypotheses mettrifi.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
mettrifi.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
mettrifi.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
Assertion mettrifi ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 mettrifi.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
2 mettrifi.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 mettrifi.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
4 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
5 2 4 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
6 eleq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑀 ) )
8 7 oveq2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) )
9 oveq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 − 1 ) = ( 𝑀 − 1 ) )
10 9 oveq2d ⊢ ( 𝑥 = 𝑀 → ( 𝑀 ... ( 𝑥 − 1 ) ) = ( 𝑀 ... ( 𝑀 − 1 ) ) )
11 10 sumeq1d ⊢ ( 𝑥 = 𝑀 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
12 8 11 breq12d ⊢ ( 𝑥 = 𝑀 → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
13 6 12 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ↔ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
15 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
16 fveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑛 ) )
17 16 oveq2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
18 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 − 1 ) = ( 𝑛 − 1 ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑀 ... ( 𝑥 − 1 ) ) = ( 𝑀 ... ( 𝑛 − 1 ) ) )
20 19 sumeq1d ⊢ ( 𝑥 = 𝑛 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
21 17 20 breq12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
22 15 21 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ↔ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
23 22 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
24 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
25 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
26 25 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
27 oveq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 − 1 ) = ( ( 𝑛 + 1 ) − 1 ) )
28 27 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑀 ... ( 𝑥 − 1 ) ) = ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) )
29 28 sumeq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
30 26 29 breq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
31 24 30 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
32 31 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
33 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
34 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑁 ) )
35 34 oveq2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) )
36 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 − 1 ) = ( 𝑁 − 1 ) )
37 36 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑀 ... ( 𝑥 − 1 ) ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
38 37 sumeq1d ⊢ ( 𝑥 = 𝑁 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
39 35 38 breq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
40 33 39 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ↔ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
41 40 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑥 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
42 0le0 ⊢ 0 ≤ 0
43 42 a1i ⊢ ( 𝜑 → 0 ≤ 0 )
44 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
45 2 44 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
46 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
47 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
48 47 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 ) )
49 48 rspcv ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 → ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 ) )
50 45 46 49 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 )
51 met0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) = 0 )
52 1 50 51 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) = 0 )
53 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
54 2 53 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
55 54 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
56 55 ltm1d ⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
57 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
58 fzn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
59 54 57 58 syl2anc2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
60 56 59 mpbid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ )
61 60 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ∅ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
62 sum0 ⊢ Σ 𝑘 ∈ ∅ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = 0
63 61 62 eqtrdi ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = 0 )
64 43 52 63 3brtr4d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
65 64 a1d ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
66 65 a1i ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑀 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
67 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
68 67 ex ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
70 69 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
71 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
72 50 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 )
73 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
74 46 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
75 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
76 75 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑋 ) )
77 76 rspcv ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑋 ) )
78 73 74 77 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑋 )
79 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
80 79 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) )
81 80 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ∀ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
82 74 81 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ∀ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
83 69 3impia ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
84 rsp ⊢ ( ∀ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) )
85 82 83 84 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
86 mettri ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
87 71 72 78 85 86 syl13anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
88 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
89 71 72 78 88 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
90 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑀 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
91 71 72 85 90 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
92 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
93 71 85 78 92 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
94 91 93 readdcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
95 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
96 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
97 elfzuz3 ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
98 83 97 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
99 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
100 98 99 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
101 100 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
102 3 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
103 101 102 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
104 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
105 104 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
106 peano2uz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
107 105 106 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
108 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
109 73 108 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
110 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
111 elfzuz3 ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) )
112 111 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) )
113 eluzp1p1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑘 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
114 112 113 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
115 uztrn ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
116 110 114 115 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
117 elfzuzb ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) )
118 107 116 117 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
119 fveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
120 119 eleq1d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) )
121 120 rspccva ⊢ ( ( ∀ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
122 82 121 sylan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
123 118 122 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
124 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
125 96 103 123 124 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
126 95 125 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
127 letr ⊢ ( ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ∈ ℝ ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
128 89 94 126 127 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
129 87 128 mpand ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
130 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ... ( 𝑛 − 1 ) ) ∈ Fin )
131 fzssp1 ⊢ ( 𝑀 ... ( 𝑛 − 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑛 − 1 ) + 1 ) )
132 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ )
133 132 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ℤ )
134 133 zcnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ℂ )
135 ax-1cn ⊢ 1 ∈ ℂ
136 npcan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
137 134 135 136 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
138 137 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ... ( ( 𝑛 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑛 ) )
139 131 138 sseqtrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ... ( 𝑛 − 1 ) ) ⊆ ( 𝑀 ... 𝑛 ) )
140 139 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑛 ) )
141 140 125 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
142 130 141 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
143 91 142 93 leadd1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
144 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
145 125 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℂ )
146 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
147 79 146 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
148 144 145 147 fsumm1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
149 148 breq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
150 143 149 bitr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑛 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
151 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
152 134 135 151 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
153 152 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑛 ) )
154 153 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
155 154 breq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
156 129 150 155 3imtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
157 156 3expia ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
158 157 a2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
159 70 158 syld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
160 159 expcom ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
161 160 a2d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑛 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑛 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
162 14 23 32 41 66 161 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
163 2 162 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
164 5 163 mpd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) 𝐷 ( 𝐹 ‘ 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )