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 
|- ( ph -> D e. ( Met ` X ) )
mettrifi.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
mettrifi.4 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. X )
Assertion mettrifi 
|- ( ph -> ( ( F ` M ) D ( F ` N ) ) <_ sum_ k e. ( M ... ( N - 1 ) ) ( ( F ` k ) D ( F ` ( k + 1 ) ) ) )

Proof

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