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 φ D Met X
mettrifi.3 φ N M
mettrifi.4 φ k M N F k X
Assertion mettrifi φ F M D F N k = M N 1 F k D F k + 1

Proof

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