Theorem efaddlem6 7302

Description: Lemma for efadd 7325. 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 7318. 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

Step	Hyp	Ref	Expression
1		efaddlem5.1	. . . . . . . 8 |- N e. NN
2	1	nnnn0 6064	. . . . . . 7 |- N e. NN0
3		nn0uz 6383	. . . . . . 7 |- NN0 = (ZZ>` 0)
4	2, 3	eleqtr 1544	. . . . . 6 |- N e. (ZZ>` 0)
5		elfznn0t 6441	. . . . . . . 8 |- (j e. (0...N) -> j e. NN0)
6		efaddlem5.2	. . . . . . . . 9 |- A e. CC
7		eftclt 7262	. . . . . . . . 9 |- ((A e. CC /\ j e. NN0) -> ((A^j) / (!` j)) e. CC)
8	6, 7	mpan 694	. . . . . . . 8 |- (j e. NN0 -> ((A^j) / (!` j)) e. CC)
9	5, 8	syl 10	. . . . . . 7 |- (j e. (0...N) -> ((A^j) / (!` j)) e. CC)
10	9	rgen 1696	. . . . . 6 |- A.j e. (0...N)((A^j) / (!` j)) e. CC
11	4, 10	pm3.2i 285	. . . . 5 |- (N e. (ZZ>` 0) /\ A.j e. (0...N)((A^j) / (!` j)) e. CC)
12		elfznn0t 6441	. . . . . . . 8 |- (k e. (0...N) -> k e. NN0)
13		efaddlem5.3	. . . . . . . . 9 |- B e. CC
14		eftclt 7262	. . . . . . . . 9 |- ((B e. CC /\ k e. NN0) -> ((B^k) / (!` k)) e. CC)
15	13, 14	mpan 694	. . . . . . . 8 |- (k e. NN0 -> ((B^k) / (!` k)) e. CC)
16	12, 15	syl 10	. . . . . . 7 |- (k e. (0...N) -> ((B^k) / (!` k)) e. CC)
17	16	rgen 1696	. . . . . 6 |- A.k e. (0...N)((B^k) / (!` k)) e. CC
18	4, 17	pm3.2i 285	. . . . 5 |- (N e. (ZZ>` 0) /\ A.k e. (0...N)((B^k) / (!` k)) e. CC)
19		fsum2mul 6990	. . . . 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))))
20	11, 18, 19	mp2an 696	. . . 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 5746	. . . . . . . . 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 6526	. . . . . . . . . . . 12 |- ((A e. CC /\ j e. NN0) -> (A^j) e. CC)
23	6, 22	mpan 694	. . . . . . . . . . 11 |- (j e. NN0 -> (A^j) e. CC)
24		facclt 6892	. . . . . . . . . . . 12 |- (j e. NN0 -> (!` j) e. NN)
25		nncnt 5888	. . . . . . . . . . . 12 |- ((!` j) e. NN -> (!` j) e. CC)
26	24, 25	syl 10	. . . . . . . . . . 11 |- (j e. NN0 -> (!` j) e. CC)
27	23, 26	jca 288	. . . . . . . . . 10 |- (j e. NN0 -> ((A^j) e. CC /\ (!` j) e. CC))
28		expclt 6526	. . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
29	13, 28	mpan 694	. . . . . . . . . . 11 |- (k e. NN0 -> (B^k) e. CC)
30		facclt 6892	. . . . . . . . . . . 12 |- (k e. NN0 -> (!` k) e. NN)
31		nncnt 5888	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) e. CC)
32	30, 31	syl 10	. . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. CC)
33	29, 32	jca 288	. . . . . . . . . 10 |- (k e. NN0 -> ((B^k) e. CC /\ (!` k) e. CC))
34	27, 33	anim12i 333	. . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) e. CC /\ (!` j) e. CC) /\ ((B^k) e. CC /\ (!` k) e. CC)))
35		facne0t 6893	. . . . . . . . . 10 |- (j e. NN0 -> (!` j) =/= 0)
36		facne0t 6893	. . . . . . . . . 10 |- (k e. NN0 -> (!` k) =/= 0)
37	35, 36	anim12i 333	. . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) =/= 0 /\ (!` k) =/= 0))
38	21, 34, 37	sylanc 471	. . . . . . . 8 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) / (!` j)) x. ((B^k) / (!` k))) = (((A^j) x. (B^k)) / ((!` j) x. (!` k))))
39	38, 5, 12	syl2an 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))))
40	39	sumeq2dv 6945	. . . . . 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))))
41	40	sumeq2i 6941	. . . . 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)))
42	1	nngt0 5908	. . . . . 6 |- 0 < N
43		divclt 5691	. . . . . . . . . . 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 5256	. . . . . . . . . . . 12 |- (((A^j) e. CC /\ (B^k) e. CC) -> ((A^j) x. (B^k)) e. CC)
45	44, 23, 29	syl2an 454	. . . . . . . . . . 11 |- ((j e. NN0 /\ k e. NN0) -> ((A^j) x. (B^k)) e. CC)
46		axmulcl 5256	. . . . . . . . . . . 12 |- (((!` j) e. CC /\ (!` k) e. CC) -> ((!` j) x. (!` k)) e. CC)
47	46, 26, 32	syl2an 454	. . . . . . . . . . 11 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) e. CC)
48		muln0bt 5676	. . . . . . . . . . . . 13 |- (((!` j) e. CC /\ (!` k) e. CC) -> (((!` j) =/= 0 /\ (!` k) =/= 0) <-> ((!` j) x. (!` k)) =/= 0))
49	48, 26, 32	syl2an 454	. . . . . . . . . . . 12 |- ((j e. NN0 /\ k e. NN0) -> (((!` j) =/= 0 /\ (!` k) =/= 0) <-> ((!` j) x. (!` k)) =/= 0))
50	37, 49	mpbid 195	. . . . . . . . . . 11 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) =/= 0)
51	43, 45, 47, 50	syl3anc 857	. . . . . . . . . 10 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
52	51, 12	sylan2 451	. . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...N)) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
53	52	r19.21aiva 1712	. . . . . . . 8 |- (j e. NN0 -> A.k e. (0...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
54		fsumclt 6968	. . . . . . . . 9 |- ((N e. (ZZ>` 0) /\ A.k e. (0...N)(((A^j) x. (B^k)) / ((