Metamath Proof Explorer


Theorem binomcxplemdvsum

Description: Lemma for binomcxp . The derivative of the generalized sum in binomcxplemnn0 . Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a φ A +
binomcxp.b φ B
binomcxp.lt φ B < A
binomcxp.c φ C
binomcxplem.f F = j 0 C C 𝑐 j
binomcxplem.s S = b k 0 F k b k
binomcxplem.r R = sup r | seq 0 + S r dom * <
binomcxplem.e E = b k k F k b k 1
binomcxplem.d D = abs -1 0 R
binomcxplem.p P = b D k 0 S b k
Assertion binomcxplemdvsum φ D P = b D k E b k

Proof

Step Hyp Ref Expression
1 binomcxp.a φ A +
2 binomcxp.b φ B
3 binomcxp.lt φ B < A
4 binomcxp.c φ C
5 binomcxplem.f F = j 0 C C 𝑐 j
6 binomcxplem.s S = b k 0 F k b k
7 binomcxplem.r R = sup r | seq 0 + S r dom * <
8 binomcxplem.e E = b k k F k b k 1
9 binomcxplem.d D = abs -1 0 R
10 binomcxplem.p P = b D k 0 S b k
11 nfcv _ b abs -1
12 nfcv _ b 0
13 nfcv _ b .
14 nfcv _ b +
15 nfmpt1 _ b b k 0 F k b k
16 6 15 nfcxfr _ b S
17 nfcv _ b r
18 16 17 nffv _ b S r
19 12 14 18 nfseq _ b seq 0 + S r
20 19 nfel1 b seq 0 + S r dom
21 nfcv _ b
22 20 21 nfrabw _ b r | seq 0 + S r dom
23 nfcv _ b *
24 nfcv _ b <
25 22 23 24 nfsup _ b sup r | seq 0 + S r dom * <
26 7 25 nfcxfr _ b R
27 12 13 26 nfov _ b 0 R
28 11 27 nfima _ b abs -1 0 R
29 9 28 nfcxfr _ b D
30 nfcv _ y D
31 nfcv _ y k 0 S b k
32 nfcv _ b 0
33 nfcv _ b y
34 16 33 nffv _ b S y
35 nfcv _ b m
36 34 35 nffv _ b S y m
37 32 36 nfsumw _ b m 0 S y m
38 simpl b = y k 0 b = y
39 38 fveq2d b = y k 0 S b = S y
40 39 fveq1d b = y k 0 S b k = S y k
41 40 sumeq2dv b = y k 0 S b k = k 0 S y k
42 nfcv _ m S y k
43 nfcv _ k
44 nfmpt1 _ k k 0 F k b k
45 43 44 nfmpt _ k b k 0 F k b k
46 6 45 nfcxfr _ k S
47 nfcv _ k y
48 46 47 nffv _ k S y
49 nfcv _ k m
50 48 49 nffv _ k S y m
51 fveq2 k = m S y k = S y m
52 42 50 51 cbvsumi k 0 S y k = m 0 S y m
53 41 52 syl6eq b = y k 0 S b k = m 0 S y m
54 29 30 31 37 53 cbvmptf b D k 0 S b k = y D m 0 S y m
55 10 54 eqtri P = y D m 0 S y m
56 ovexd φ j 0 C C 𝑐 j V
57 5 a1i φ F = j 0 C C 𝑐 j
58 5 a1i φ k 0 F = j 0 C C 𝑐 j
59 simpr φ k 0 j = k j = k
60 59 oveq2d φ k 0 j = k C C 𝑐 j = C C 𝑐 k
61 simpr φ k 0 k 0
62 4 adantr φ k 0 C
63 62 61 bcccl φ k 0 C C 𝑐 k
64 58 60 61 63 fvmptd φ k 0 F k = C C 𝑐 k
65 64 63 eqeltrd φ k 0 F k
66 56 57 65 fmpt2d φ F : 0
67 nfcv _ r
68 nfcv _ z
69 nfv z seq 0 + S r dom
70 nfcv _ r 0
71 nfcv _ r +
72 nfcv _ r b k 0 F k b k
73 6 72 nfcxfr _ r S
74 nfcv _ r z
75 73 74 nffv _ r S z
76 70 71 75 nfseq _ r seq 0 + S z
77 76 nfel1 r seq 0 + S z dom
78 fveq2 r = z S r = S z
79 78 seqeq3d r = z seq 0 + S r = seq 0 + S z
80 79 eleq1d r = z seq 0 + S r dom seq 0 + S z dom
81 67 68 69 77 80 cbvrabw r | seq 0 + S r dom = z | seq 0 + S z dom
82 81 supeq1i sup r | seq 0 + S r dom * < = sup z | seq 0 + S z dom * <
83 7 82 eqtri R = sup z | seq 0 + S z dom * <
84 6 fveq1i S z = b k 0 F k b k z
85 seqeq3 S z = b k 0 F k b k z seq 0 + S z = seq 0 + b k 0 F k b k z
86 84 85 ax-mp seq 0 + S z = seq 0 + b k 0 F k b k z
87 86 eleq1i seq 0 + S z dom seq 0 + b k 0 F k b k z dom
88 87 rabbii z | seq 0 + S z dom = z | seq 0 + b k 0 F k b k z dom
89 88 supeq1i sup z | seq 0 + S z dom * < = sup z | seq 0 + b k 0 F k b k z dom * <
90 7 82 89 3eqtrri sup z | seq 0 + b k 0 F k b k z dom * < = R
91 90 eleq1i sup z | seq 0 + b k 0 F k b k z dom * < R
92 90 oveq2i x + sup z | seq 0 + b k 0 F k b k z dom * < = x + R
93 92 oveq1i x + sup z | seq 0 + b k 0 F k b k z dom * < 2 = x + R 2
94 eqid x + 1 = x + 1
95 91 93 94 ifbieq12i if sup z | seq 0 + b k 0 F k b k z dom * < x + sup z | seq 0 + b k 0 F k b k z dom * < 2 x + 1 = if R x + R 2 x + 1
96 oveq1 w = b w k = b k
97 96 oveq2d w = b F k w k = F k b k
98 97 mpteq2dv w = b k 0 F k w k = k 0 F k b k
99 98 cbvmptv w k 0 F k w k = b k 0 F k b k
100 99 fveq1i w k 0 F k w k z = b k 0 F k b k z
101 seqeq3 w k 0 F k w k z = b k 0 F k b k z seq 0 + w k 0 F k w k z = seq 0 + b k 0 F k b k z
102 100 101 ax-mp seq 0 + w k 0 F k w k z = seq 0 + b k 0 F k b k z
103 102 eleq1i seq 0 + w k 0 F k w k z dom seq 0 + b k 0 F k b k z dom
104 103 rabbii z | seq 0 + w k 0 F k w k z dom = z | seq 0 + b k 0 F k b k z dom
105 104 supeq1i sup z | seq 0 + w k 0 F k w k z dom * < = sup z | seq 0 + b k 0 F k b k z dom * <
106 105 eleq1i sup z | seq 0 + w k 0 F k w k z dom * < sup z | seq 0 + b k 0 F k b k z dom * <
107 105 oveq2i x + sup z | seq 0 + w k 0 F k w k z dom * < = x + sup z | seq 0 + b k 0 F k b k z dom * <
108 107 oveq1i x + sup z | seq 0 + w k 0 F k w k z dom * < 2 = x + sup z | seq 0 + b k 0 F k b k z dom * < 2
109 106 108 94 ifbieq12i if sup z | seq 0 + w k 0 F k w k z dom * < x + sup z | seq 0 + w k 0 F k w k z dom * < 2 x + 1 = if sup z | seq 0 + b k 0 F k b k z dom * < x + sup z | seq 0 + b k 0 F k b k z dom * < 2 x + 1
110 109 oveq2i x + if sup z | seq 0 + w k 0 F k w k z dom * < x + sup z | seq 0 + w k 0 F k w k z dom * < 2 x + 1 = x + if sup z | seq 0 + b k 0 F k b k z dom * < x + sup z | seq 0 + b k 0 F k b k z dom * < 2 x + 1
111 110 oveq1i x + if sup z | seq 0 + w k 0 F k w k z dom * < x + sup z | seq 0 + w k 0 F k w k z dom * < 2 x + 1 2 = x + if sup z | seq 0 + b k 0 F k b k z dom * < x + sup z | seq 0 + b k 0 F k b k z dom * < 2 x + 1 2
112 111 oveq2i 0 ball abs x + if sup z | seq 0 + w k 0 F k w k z dom * < x + sup z | seq 0 + w k 0 F k w k z dom * < 2 x + 1 2 = 0 ball abs x + if sup z | seq 0 + b k 0 F k b k z dom * < x + sup z | seq 0 + b k 0 F k b k z dom * < 2 x + 1 2
113 6 55 66 83 9 95 112 pserdv2 φ D P = y D n n F n y n 1
114 cnvimass abs -1 0 R dom abs
115 9 114 eqsstri D dom abs
116 absf abs :
117 116 fdmi dom abs =
118 115 117 sseqtri D
119 118 sseli y D y
120 8 a1i φ y E = b k k F k b k 1
121 simplr φ y b = y k b = y
122 121 oveq1d φ y b = y k b k 1 = y k 1
123 122 oveq2d φ y b = y k k F k b k 1 = k F k y k 1
124 123 mpteq2dva φ y b = y k k F k b k 1 = k k F k y k 1
125 simpr φ y y
126 nnex V
127 126 mptex k k F k y k 1 V
128 127 a1i φ y k k F k y k 1 V
129 120 124 125 128 fvmptd φ y E y = k k F k y k 1
130 129 adantr φ y n E y = k k F k y k 1
131 simpr φ y n k = n k = n
132 131 fveq2d φ y n k = n F k = F n
133 131 132 oveq12d φ y n k = n k F k = n F n
134 131 oveq1d φ y n k = n k 1 = n 1
135 134 oveq2d φ y n k = n y k 1 = y n 1
136 133 135 oveq12d φ y n k = n k F k y k 1 = n F n y n 1
137 simpr φ y n n
138 ovexd φ y n n F n y n 1 V
139 130 136 137 138 fvmptd φ y n E y n = n F n y n 1
140 139 sumeq2dv φ y n E y n = n n F n y n 1
141 119 140 sylan2 φ y D n E y n = n n F n y n 1
142 141 mpteq2dva φ y D n E y n = y D n n F n y n 1
143 113 142 eqtr4d φ D P = y D n E y n
144 nfcv _ b
145 nfmpt1 _ b b k k F k b k 1
146 8 145 nfcxfr _ b E
147 146 33 nffv _ b E y
148 nfcv _ b n
149 147 148 nffv _ b E y n
150 144 149 nfsumw _ b n E y n
151 nfcv _ y k E b k
152 simpl y = b n y = b
153 152 fveq2d y = b n E y = E b
154 153 fveq1d y = b n E y n = E b n
155 154 sumeq2dv y = b n E y n = n E b n
156 nfmpt1 _ k k k F k b k 1
157 43 156 nfmpt _ k b k k F k b k 1
158 8 157 nfcxfr _ k E
159 nfcv _ k b
160 158 159 nffv _ k E b
161 nfcv _ k n
162 160 161 nffv _ k E b n
163 nfcv _ n E b k
164 fveq2 n = k E b n = E b k
165 162 163 164 cbvsumi n E b n = k E b k
166 155 165 syl6eq y = b n E y n = k E b k
167 30 29 150 151 166 cbvmptf y D n E y n = b D k E b k
168 143 167 syl6eq φ D P = b D k E b k