Theorem efaddlem5 7292

Description: Lemma for efadd 7316. Convert the truncated series for exp` (A + B) to a double summation using the binomial theorem binom 7018 and rearranging with fsum0diag2 7202.

Hypotheses

Ref	Expression
efaddlem5.1	|- N e. NN
efaddlem5.2	|- A e. CC
efaddlem5.3	|- B e. CC

Assertion

Ref	Expression
efaddlem5	|- sum_j e. (0...N)(((A + B)^j) / (!` j)) = sum_j e. (0...N)sum_k e. (0...(N - j))(((A^j) x. (B^k)) / ((!` j) x. (!` k)))

Distinct variable groups:   j,k,A   B,j,k   j,N,k

Proof of Theorem efaddlem5

Step	Hyp	Ref	Expression
1		elfznn0t 6436	. . . 4 |- (j e. (0...N) -> j e. NN0)
2		efaddlem5.2	. . . . . . 7 |- A e. CC
3		efaddlem5.3	. . . . . . 7 |- B e. CC
4	2, 3	binom 7018	. . . . . 6 |- (j e. NN0 -> ((A + B)^j) = sum_k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))))
5	4	opreq1d 3966	. . . . 5 |- (j e. NN0 -> (((A + B)^j) / (!` j)) = (sum_k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)))
6		fsumdivc 6981	. . . . . 6 |- (((j e. (ZZ>` 0) /\ (!` j) e. CC) /\ ((!` j) =/= 0 /\ A.k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))) e. CC)) -> (sum_k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)) = sum_k e. (0...j)(((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)))
7		elnn0uz 6381	. . . . . . 7 |- (j e. NN0 <-> j e. (ZZ>` 0))
8	7	biimp 151	. . . . . 6 |- (j e. NN0 -> j e. (ZZ>` 0))
9		facclt 6885	. . . . . . 7 |- (j e. NN0 -> (!` j) e. NN)
10		nncnt 5886	. . . . . . 7 |- ((!` j) e. NN -> (!` j) e. CC)
11	9, 10	syl 10	. . . . . 6 |- (j e. NN0 -> (!` j) e. CC)
12		facne0t 6886	. . . . . 6 |- (j e. NN0 -> (!` j) =/= 0)
13		axmulcl 5253	. . . . . . . 8 |- (((j C. k) e. CC /\ ((A^(j - k)) x. (B^k)) e. CC) -> ((j C. k) x. ((A^(j - k)) x. (B^k))) e. CC)
14		bcclt 6918	. . . . . . . . . 10 |- ((j e. NN0 /\ k e. ZZ) -> (j C. k) e. NN0)
15		elfzelz 6422	. . . . . . . . . 10 |- (k e. (0...j) -> k e. ZZ)
16	14, 15	sylan2 451	. . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...j)) -> (j C. k) e. NN0)
17		nn0cnt 6064	. . . . . . . . 9 |- ((j C. k) e. NN0 -> (j C. k) e. CC)
18	16, 17	syl 10	. . . . . . . 8 |- ((j e. NN0 /\ k e. (0...j)) -> (j C. k) e. CC)
19		axmulcl 5253	. . . . . . . . 9 |- (((A^(j - k)) e. CC /\ (B^k) e. CC) -> ((A^(j - k)) x. (B^k)) e. CC)
20		fznn0subt 6438	. . . . . . . . . 10 |- ((j e. NN0 /\ k e. (0...j)) -> (j - k) e. NN0)
21		expclt 6521	. . . . . . . . . . 11 |- ((A e. CC /\ (j - k) e. NN0) -> (A^(j - k)) e. CC)
22	2, 21	mpan 694	. . . . . . . . . 10 |- ((j - k) e. NN0 -> (A^(j - k)) e. CC)
23	20, 22	syl 10	. . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...j)) -> (A^(j - k)) e. CC)
24		elfznn0t 6436	. . . . . . . . . . 11 |- (k e. (0...j) -> k e. NN0)
25		expclt 6521	. . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
26	3, 25	mpan 694	. . . . . . . . . . 11 |- (k e. NN0 -> (B^k) e. CC)
27	24, 26	syl 10	. . . . . . . . . 10 |- (k e. (0...j) -> (B^k) e. CC)
28	27	adantl 388	. . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...j)) -> (B^k) e. CC)
29	19, 23, 28	sylanc 471	. . . . . . . 8 |- ((j e. NN0 /\ k e. (0...j)) -> ((A^(j - k)) x. (B^k)) e. CC)
30	13, 18, 29	sylanc 471	. . . . . . 7 |- ((j e. NN0 /\ k e. (0...j)) -> ((j C. k) x. ((A^(j - k)) x. (B^k))) e. CC)
31	30	r19.21aiva 1711	. . . . . 6 |- (j e. NN0 -> A.k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))) e. CC)
32	6, 8, 11, 12, 31	syl2anc 472	. . . . 5 |- (j e. NN0 -> (sum_k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)) = sum_k e. (0...j)(((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)))
33		div23t 5713	. . . . . . . 8 |- ((((j C. k) e. CC /\ ((A^(j - k)) x. (B^k)) e. CC /\ (!` j) e. CC) /\ (!` j) =/= 0) -> (((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)) = (((j C. k) / (!` j)) x. ((A^(j - k)) x. (B^k))))
34	11	adantr 389	. . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...j)) -> (!` j) e. CC)
35	18, 29, 34	3jca 818	. . . . . . . 8 |- ((j e. NN0 /\ k e. (0...j)) -> ((j C. k) e. CC /\ ((A^(j - k)) x. (B^k)) e. CC /\ (!` j) e. CC))
36	12	adantr 389	. . . . . . . 8 |- ((j e. NN0 /\ k e. (0...j)) -> (!` j) =/= 0)
37	33, 35, 36	sylanc 471	. . . . . . 7 |- ((j e. NN0 /\ k e. (0...j)) -> (((j C. k) x. ((A^(j - k)) x. (B^k))) / (!` j)) = (((j C. k) / (!` j)) x. ((A^(j - k)) x. (B^k))))
38		bcval3t 6906	. . . . . . . . . 10 |- ((j e. NN0 /\ k e. (0...j)) -> (j C. k) = ((!` j) / ((!` (j - k)) x. (!` k))))
39	38	opreq1d 3966	. . . . . . . . 9 |- ((j e. NN0 /\ k e. (0...j)) -> ((j C. k) / (!` j)) = (((!` j) / ((!` (j - k)) x. (!` k))) / (!` j)))
40		divdiv23t 5756	. . . . . . . . . 10 |- ((((!` j) e. CC /\ ((!` (j - k)) x. (!` k)) e. CC /\ (!` j) e. CC) /\ (((!` (j - k)) x. (!` k)) =/= 0 /\ (!` j) =/= 0)) -> (((!` j) / ((!` (j - k)) x. (!` k))) / (!` j)) = (((!` j) / (!` j)) / ((!` (j - k)) x. (!` k))))
41		nnmulclt 5897	. . . . . . . . . . . . 13 |- (((!` (j - k)) e. NN /\ (!` k) e. NN) -> ((!` (j - k)) x. (!` k)) e. NN)
42		facclt 6885	. . . . . . . . . . . . . 14 |- ((j - k) e. NN0 -> (!` (j - k)) e. NN)
43	20, 42	syl 10	. . . . . . . . . . . . 13 |- ((j e. NN0 /\ k e. (0...j)) -> (!` (j - k)) e. NN)
44		facclt 6885	. . . . . . . . . . . . . . 15 |- (k e. NN0 -> (!` k) e. NN)
45	24, 44	syl 10	. . . . . . . . . . . . . 14 |- (k e. (0...j) -> (!` k) e. NN)
46	45	adantl 388	. . . . . . . . . . . . 13 |- ((j e. NN0 /\ k e. (0...j)) -> (!` k) e. NN)
47	41, 43, 46	sylanc 471	. . . . . . . . . . . 12 |- ((j e. NN0 /\ k e. (0...j)) -> ((!` (j - k)) x. (!` k)) e. NN)
48		nncnt 5886	. . . . . . . . . . . 12 |- (((!` (j - k)) x. (!` k)) e. NN -> ((!` (j - k)) x. (!` k)) e. CC)
49	47, 48	syl 10	. . . . . . . . . . 11 |- ((j e. NN0 /\ k e. (0...j)) -> ((!` (j - k)) x. (!` k)) e. CC)
50	34, 49, 34	3jca 818	. . . . . . . . . 10 |- ((j e. NN0 /\ k e. (0...j)) -> ((!` j) e. CC /\ ((!` (j - k)) x. (!` k)) e. CC /\ (!` j) e. CC))
51		nnne0t 5905	. . . . . . . . . . . 12 |- (((!` (j - k)) x. (!` k)) e. NN -> ((!` (j - k)) x. (!` k)) =/= 0)
52	47, 51	syl 10	. . . . . . . . . . 11 |- ((j e. NN0 /\ k e. (0...j)) -> ((!` (j - k)) x. (!` k)) =/= 0)
53	52, 36	jca 288	. . . . . . . . . 10 |- (