HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem efaddlem6 7285
Description: Lemma for efadd 7308. Compute the difference between the truncated series for (exp` A) x. (exp` B) and exp` (A + B). A main goal of the proof is to show that this difference goes to zero as N approaches infinity; this is finally accomplished in efaddlem22 7301. Warning: The HTML proof page is 0.6 megabyte in size.
Hypotheses
Ref Expression
efaddlem5.1 |- N e. NN
efaddlem5.2 |- A e. CC
efaddlem5.3 |- B e. CC
Assertion
Ref Expression
efaddlem6 |- ((sum_j e. (0...N)((A^j) / (!` j)) x. sum_k e. (0...N)((B^k) / (!` k))) - sum_j e. (0...N)(((A + B)^j) / (!` j))) = sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))
Distinct variable groups:   j,k,A   B,j,k   j,N,k
Proof of Theorem efaddlem6
StepHypRef Expression
1 efaddlem5.1 . . . . . . . 8 |- N e. NN
21nnnn0 6054 . . . . . . 7 |- N e. NN0
3 nn0uz 6370 . . . . . . 7 |- NN0 = (ZZ>` 0)
42, 3eleqtr 1538 . . . . . 6 |- N e. (ZZ>` 0)
5 elfznn0t 6428 . . . . . . . 8 |- (j e. (0...N) -> j e. NN0)
6 efaddlem5.2 . . . . . . . . 9 |- A e. CC
7 eftclt 7245 . . . . . . . . 9 |- ((A e. CC /\ j e. NN0) -> ((A^j) / (!` j)) e. CC)
86, 7mpan 693 . . . . . . . 8 |- (j e. NN0 -> ((A^j) / (!` j)) e. CC)
95, 8syl 10 . . . . . . 7 |- (j e. (0...N) -> ((A^j) / (!` j)) e. CC)
109rgen 1690 . . . . . 6 |- A.j e. (0...N)((A^j) / (!` j)) e. CC
114, 10pm3.2i 285 . . . . 5 |- (N e. (ZZ>` 0) /\ A.j e. (0...N)((A^j) / (!` j)) e. CC)
12 elfznn0t 6428 . . . . . . . 8 |- (k e. (0...N) -> k e. NN0)
13 efaddlem5.3 . . . . . . . . 9 |- B e. CC
14 eftclt 7245 . . . . . . . . 9 |- ((B e. CC /\ k e. NN0) -> ((B^k) / (!` k)) e. CC)
1513, 14mpan 693 . . . . . . . 8 |- (k e. NN0 -> ((B^k) / (!` k)) e. CC)
1612, 15syl 10 . . . . . . 7 |- (k e. (0...N) -> ((B^k) / (!` k)) e. CC)
1716rgen 1690 . . . . . 6 |- A.k e. (0...N)((B^k) / (!` k)) e. CC
184, 17pm3.2i 285 . . . . 5 |- (N e. (ZZ>` 0) /\ A.k e. (0...N)((B^k) / (!` k)) e. CC)
19 fsum2mul 6975 . . . . 5 |- (((N e. (ZZ>` 0) /\ A.j e. (0...N)((A^j) / (!` j)) e. CC) /\ (N e. (ZZ>` 0) /\ A.k e. (0...N)((B^k) / (!` k)) e. CC)) -> sum_j e. (0...N)sum_k e. (0...N)(((A^j) / (!` j)) x. ((B^k) / (!` k))) = (sum_j e. (0...N)((A^j) / (!` j)) x. sum_k e. (0...N)((B^k) / (!` k))))
2011, 18, 19mp2an 695 . . . 4 |- sum_j e. (0...N)sum_k e. (0...N)(((A^j) / (!` j)) x. ((B^k) / (!` k))) = (sum_j e. (0...N)((A^j) / (!` j)) x. sum_k e. (0...N)((B^k) / (!` k)))
21 divmuldivt 5736 . . . . . . . . 9 |- (((((A^j) e. CC /\ (!` j) e. CC) /\ ((B^k) e. CC /\ (!` k) e. CC)) /\ ((!` j) =/= 0 /\ (!` k) =/= 0)) -> (((A^j) / (!` j)) x. ((B^k) / (!` k))) = (((A^j) x. (B^k)) / ((!` j) x. (!` k))))
22 expclt 6513 . . . . . . . . . . . 12 |- ((A e. CC /\ j e. NN0) -> (A^j) e. CC)
236, 22mpan 693 . . . . . . . . . . 11 |- (j e. NN0 -> (A^j) e. CC)
24 facclt 6877 . . . . . . . . . . . 12 |- (j e. NN0 -> (!` j) e. NN)
25 nncnt 5878 . . . . . . . . . . . 12 |- ((!` j) e. NN -> (!` j) e. CC)
2624, 25syl 10 . . . . . . . . . . 11 |- (j e. NN0 -> (!` j) e. CC)
2723, 26jca 288 . . . . . . . . . 10 |- (j e. NN0 -> ((A^j) e. CC /\ (!` j) e. CC))
28 expclt 6513 . . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
2913, 28mpan 693 . . . . . . . . . . 11 |- (k e. NN0 -> (B^k) e. CC)
30 facclt 6877 . . . . . . . . . . . 12 |- (k e. NN0 -> (!` k) e. NN)
31 nncnt 5878 . . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) e. CC)
3230, 31syl 10 . . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. CC)
3329, 32jca 288 . . . . . . . . . 10 |- (k e. NN0 -> ((B^k) e. CC /\ (!` k) e. CC))
3427, 33anim12i 333 . . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) e. CC /\ (!` j) e. CC) /\ ((B^k) e. CC /\ (!` k) e. CC)))
35 facne0t 6878 . . . . . . . . . 10 |- (j e. NN0 -> (!` j) =/= 0)
36 facne0t 6878 . . . . . . . . . 10 |- (k e. NN0 -> (!` k) =/= 0)
3735, 36anim12i 333 . . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) =/= 0 /\ (!` k) =/= 0))
3821, 34, 37sylanc 471 . . . . . . . 8 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) / (!` j)) x. ((B^k) / (!` k))) = (((A^j) x. (B^k)) / ((!` j) x. (!` k))))
3938, 5, 12syl2an 454 . . . . . . 7 |- ((j e. (0...N) /\ k e. (0...N)) -> (((A^j) / (!` j)) x. ((B^k) / (!` k))) = (((A^j) x. (B^k)) / ((!` j) x. (!` k))))
4039sumeq2dv 6930 . . . . . 6 |- (j e. (0...N) -> sum_k e. (0...N)(((A^j) / (!` j)) x. ((B^k) / (!` k))) = sum_k e. (0...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))))
4140sumeq2i 6926 . . . . 5 |- sum_j e. (0...N)sum_k e. (0...N)(((A^j) / (!` j)) x. ((B^k) / (!` k))) = sum_j e. (0...N)sum_k e. (0...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))
421nngt0 5898 . . . . . 6 |- 0 < N
43 divclt 5681 . . . . . . . . . . 11 |- ((((A^j) x. (B^k)) e. CC /\ ((!` j) x. (!` k)) e. CC /\ ((!` j) x. (!` k)) =/= 0) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
44 axmulcl 5245 . . . . . . . . . . . 12 |- (((A^j) e. CC /\ (B^k) e. CC) -> ((A^j) x. (B^k)) e. CC)
4544, 23, 29syl2an 454 . . . . . . . . . . 11 |- ((j e. NN0 /\ k e. NN0) -> ((A^j) x. (B^k)) e. CC)
46 axmulcl 5245 . . . . . . . . . . . 12 |- (((!` j) e. CC /\ (!` k) e. CC) -> ((!` j) x. (!` k)) e. CC)
4746, 26, 32syl2an 454 . . . . . . . . . . 11 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) e. CC)
48 muln0bt 5666 . . . . . . . . . . . . 13 |- (((!` j) e. CC /\ (!` k) e. CC) -> (((!` j) =/= 0 /\ (!` k) =/= 0) <-> ((!` j) x. (!` k)) =/= 0))
4948, 26, 32syl2an 454 . . . . . . . . . . . 12 |- ((j e. NN0 /\ k e. NN0) -> (((!` j) =/= 0 /\ (!` k) =/= 0) <-> ((!` j) x. (!` k)) =/= 0))
5037, 49mpbid 195 . . . . . . . . . . 11 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) =/= 0)
5143, 45, 47, 50syl3anc 856 . . . . . . . . . 10 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
5251, 12sylan2 451 . . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...N)) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
5352r19.21aiva 1706 . . . . . . . 8 |- (j e. NN0 -> A.k e. (0...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
54 fsumclt 6953 . . . . . . . . 9 |- ((N e. (ZZ>` 0) /\ A.k e. (0...N)(((A^j) x. (B^k)) / ((