Metamath Proof Explorer


Theorem pntrsumbnd2

Description: A bound on a sum over R . Equation 10.1.16 of Shapiro, p. 403. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypothesis pntrval.r R = a + ψ a a
Assertion pntrsumbnd2 c + k m n = k m R n n n + 1 c

Proof

Step Hyp Ref Expression
1 pntrval.r R = a + ψ a a
2 1 pntrsumbnd b + m n = 1 m R n n n + 1 b
3 2rp 2 +
4 rpmulcl 2 + b + 2 b +
5 3 4 mpan b + 2 b +
6 oveq2 m = k 1 1 m = 1 k 1
7 6 sumeq1d m = k 1 n = 1 m R n n n + 1 = n = 1 k 1 R n n n + 1
8 7 fveq2d m = k 1 n = 1 m R n n n + 1 = n = 1 k 1 R n n n + 1
9 8 breq1d m = k 1 n = 1 m R n n n + 1 b n = 1 k 1 R n n n + 1 b
10 simplr b + m n = 1 m R n n n + 1 b k m n = 1 m R n n n + 1 b
11 nnz k k
12 11 adantl b + m n = 1 m R n n n + 1 b k k
13 peano2zm k k 1
14 12 13 syl b + m n = 1 m R n n n + 1 b k k 1
15 9 10 14 rspcdva b + m n = 1 m R n n n + 1 b k n = 1 k 1 R n n n + 1 b
16 5 ad2antrr b + k m 2 b +
17 16 rpge0d b + k m 0 2 b
18 sumeq1 k m = n = k m R n n n + 1 = n R n n n + 1
19 sum0 n R n n n + 1 = 0
20 18 19 eqtrdi k m = n = k m R n n n + 1 = 0
21 20 abs00bd k m = n = k m R n n n + 1 = 0
22 21 breq1d k m = n = k m R n n n + 1 2 b 0 2 b
23 17 22 syl5ibrcom b + k m k m = n = k m R n n n + 1 2 b
24 23 imp b + k m k m = n = k m R n n n + 1 2 b
25 24 a1d b + k m k m = n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
26 fzn0 k m m k
27 fzfid b + k m m k 1 m Fin
28 elfznn n 1 m n
29 simpr b + k m m k n n
30 29 nnrpd b + k m m k n n +
31 1 pntrf R : +
32 31 ffvelrni n + R n
33 30 32 syl b + k m m k n R n
34 29 peano2nnd b + k m m k n n + 1
35 29 34 nnmulcld b + k m m k n n n + 1
36 33 35 nndivred b + k m m k n R n n n + 1
37 28 36 sylan2 b + k m m k n 1 m R n n n + 1
38 27 37 fsumrecl b + k m m k n = 1 m R n n n + 1
39 38 recnd b + k m m k n = 1 m R n n n + 1
40 39 abscld b + k m m k n = 1 m R n n n + 1
41 fzfid b + k m m k 1 k 1 Fin
42 elfznn n 1 k 1 n
43 42 36 sylan2 b + k m m k n 1 k 1 R n n n + 1
44 41 43 fsumrecl b + k m m k n = 1 k 1 R n n n + 1
45 44 recnd b + k m m k n = 1 k 1 R n n n + 1
46 45 abscld b + k m m k n = 1 k 1 R n n n + 1
47 simplll b + k m m k b +
48 47 rpred b + k m m k b
49 le2add n = 1 m R n n n + 1 n = 1 k 1 R n n n + 1 b b n = 1 m R n n n + 1 b n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 b + b
50 40 46 48 48 49 syl22anc b + k m m k n = 1 m R n n n + 1 b n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 b + b
51 48 recnd b + k m m k b
52 51 2timesd b + k m m k 2 b = b + b
53 52 breq2d b + k m m k n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 2 b n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 b + b
54 fzfid b + k m m k k m Fin
55 simpllr b + k m m k k
56 elfzuz n k m n k
57 eluznn k n k n
58 55 56 57 syl2an b + k m m k n k m n
59 58 36 syldan b + k m m k n k m R n n n + 1
60 54 59 fsumrecl b + k m m k n = k m R n n n + 1
61 60 recnd b + k m m k n = k m R n n n + 1
62 55 nnred b + k m m k k
63 62 ltm1d b + k m m k k 1 < k
64 fzdisj k 1 < k 1 k 1 k m =
65 63 64 syl b + k m m k 1 k 1 k m =
66 55 nncnd b + k m m k k
67 ax-1cn 1
68 npcan k 1 k - 1 + 1 = k
69 66 67 68 sylancl b + k m m k k - 1 + 1 = k
70 69 55 eqeltrd b + k m m k k - 1 + 1
71 nnuz = 1
72 70 71 eleqtrdi b + k m m k k - 1 + 1 1
73 55 nnzd b + k m m k k
74 73 13 syl b + k m m k k 1
75 simplr b + k m k
76 75 nncnd b + k m k
77 76 67 68 sylancl b + k m k - 1 + 1 = k
78 77 fveq2d b + k m k - 1 + 1 = k
79 78 eleq2d b + k m m k - 1 + 1 m k
80 79 biimpar b + k m m k m k - 1 + 1
81 peano2uzr k 1 m k - 1 + 1 m k 1
82 74 80 81 syl2anc b + k m m k m k 1
83 fzsplit2 k - 1 + 1 1 m k 1 1 m = 1 k 1 k - 1 + 1 m
84 72 82 83 syl2anc b + k m m k 1 m = 1 k 1 k - 1 + 1 m
85 69 oveq1d b + k m m k k - 1 + 1 m = k m
86 85 uneq2d b + k m m k 1 k 1 k - 1 + 1 m = 1 k 1 k m
87 84 86 eqtrd b + k m m k 1 m = 1 k 1 k m
88 37 recnd b + k m m k n 1 m R n n n + 1
89 65 87 27 88 fsumsplit b + k m m k n = 1 m R n n n + 1 = n = 1 k 1 R n n n + 1 + n = k m R n n n + 1
90 45 61 89 mvrladdd b + k m m k n = 1 m R n n n + 1 n = 1 k 1 R n n n + 1 = n = k m R n n n + 1
91 90 fveq2d b + k m m k n = 1 m R n n n + 1 n = 1 k 1 R n n n + 1 = n = k m R n n n + 1
92 39 45 abs2dif2d b + k m m k n = 1 m R n n n + 1 n = 1 k 1 R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1
93 91 92 eqbrtrrd b + k m m k n = k m R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1
94 61 abscld b + k m m k n = k m R n n n + 1
95 40 46 readdcld b + k m m k n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1
96 2re 2
97 96 a1i b + k m m k 2
98 97 48 remulcld b + k m m k 2 b
99 letr n = k m R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 2 b n = k m R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 2 b n = k m R n n n + 1 2 b
100 94 95 98 99 syl3anc b + k m m k n = k m R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 2 b n = k m R n n n + 1 2 b
101 93 100 mpand b + k m m k n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 2 b n = k m R n n n + 1 2 b
102 53 101 sylbird b + k m m k n = 1 m R n n n + 1 + n = 1 k 1 R n n n + 1 b + b n = k m R n n n + 1 2 b
103 50 102 syld b + k m m k n = 1 m R n n n + 1 b n = 1 k 1 R n n n + 1 b n = k m R n n n + 1 2 b
104 103 ancomsd b + k m m k n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
105 26 104 sylan2b b + k m k m n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
106 25 105 pm2.61dane b + k m n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
107 106 imp b + k m n = 1 k 1 R n n n + 1 b n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
108 107 an4s b + k n = 1 k 1 R n n n + 1 b m n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
109 108 expr b + k n = 1 k 1 R n n n + 1 b m n = 1 m R n n n + 1 b n = k m R n n n + 1 2 b
110 109 ralimdva b + k n = 1 k 1 R n n n + 1 b m n = 1 m R n n n + 1 b m n = k m R n n n + 1 2 b
111 110 impancom b + k m n = 1 m R n n n + 1 b n = 1 k 1 R n n n + 1 b m n = k m R n n n + 1 2 b
112 111 an32s b + m n = 1 m R n n n + 1 b k n = 1 k 1 R n n n + 1 b m n = k m R n n n + 1 2 b
113 15 112 mpd b + m n = 1 m R n n n + 1 b k m n = k m R n n n + 1 2 b
114 113 ralrimiva b + m n = 1 m R n n n + 1 b k m n = k m R n n n + 1 2 b
115 breq2 c = 2 b n = k m R n n n + 1 c n = k m R n n n + 1 2 b
116 115 2ralbidv c = 2 b k m n = k m R n n n + 1 c k m n = k m R n n n + 1 2 b
117 116 rspcev 2 b + k m n = k m R n n n + 1 2 b c + k m n = k m R n n n + 1 c
118 5 114 117 syl2an2r b + m n = 1 m R n n n + 1 b c + k m n = k m R n n n + 1 c
119 118 rexlimiva b + m n = 1 m R n n n + 1 b c + k m n = k m R n n n + 1 c
120 2 119 ax-mp c + k m n = k m R n n n + 1 c