Theorem efaddlem27 7323

Description: Lemma for efadd 7325. Show that the convergence of the sequence of partial sum products H to exp` (A + B). The key theorem used is 2climnn 7055.

Hypotheses

Ref	Expression
efaddlem27.1	|- A e. CC
efaddlem27.2	|- B e. CC
efaddlem27.3	|- F = {<.n, y>. | (n e. NN0 /\ y = sum_j e. (0...n)(((A + B)^j) / (!` j)))}
efaddlem27.4	|- H = {<.n, y>. | (n e. NN0 /\ y = (sum_j e. (0...n)((A^j) / (!` j)) x. sum_k e. (0...n)((B^k) / (!` k))))}

Assertion

Ref	Expression
efaddlem27	|- H ~~> (exp` (A + B))

Distinct variable groups:   j,k,n,y,A   B,j,k,n,y

Proof of Theorem efaddlem27

Step	Hyp	Ref	Expression
1		efaddlem27.1	. . . . 5 |- A e. CC
2		efaddlem27.2	. . . . 5 |- B e. CC
3	1, 2	addcl 5303	. . . 4 |- (A + B) e. CC
4		efclt 7271	. . . 4 |- ((A + B) e. CC -> (exp` (A + B)) e. CC)
5	3, 4	ax-mp 7	. . 3 |- (exp` (A + B)) e. CC
6		nnnn0t 6063	. . . . 5 |- (m e. NN -> m e. NN0)
7		opreq2 3964	. . . . . . . . 9 |- (n = m -> (0...n) = (0...m))
8	7	sumeq1d 6943	. . . . . . . 8 |- (n = m -> sum_j e. (0...n)(((A + B)^j) / (!` j)) = sum_j e. (0...m)(((A + B)^j) / (!` j)))
9		efaddlem27.3	. . . . . . . 8 |- F = {<.n, y>. | (n e. NN0 /\ y = sum_j e. (0...n)(((A + B)^j) / (!` j)))}
10		sumex 6934	. . . . . . . 8 |- sum_j e. (0...m)(((A + B)^j) / (!` j)) e. V
11	8, 9, 10	fvopab4 3775	. . . . . . 7 |- (m e. NN0 -> (F` m) = sum_j e. (0...m)(((A + B)^j) / (!` j)))
12		elfznn0t 6441	. . . . . . . . . 10 |- (j e. (0...m) -> j e. NN0)
13		eftclt 7262	. . . . . . . . . . 11 |- (((A + B) e. CC /\ j e. NN0) -> (((A + B)^j) / (!` j)) e. CC)
14	3, 13	mpan 694	. . . . . . . . . 10 |- (j e. NN0 -> (((A + B)^j) / (!` j)) e. CC)
15	12, 14	syl 10	. . . . . . . . 9 |- (j e. (0...m) -> (((A + B)^j) / (!` j)) e. CC)
16	15	rgen 1696	. . . . . . . 8 |- A.j e. (0...m)(((A + B)^j) / (!` j)) e. CC
17		fsum0clt 6969	. . . . . . . 8 |- ((m e. NN0 /\ A.j e. (0...m)(((A + B)^j) / (!` j)) e. CC) -> sum_j e. (0...m)(((A + B)^j) / (!` j)) e. CC)
18	16, 17	mpan2 695	. . . . . . 7 |- (m e. NN0 -> sum_j e. (0...m)(((A + B)^j) / (!` j)) e. CC)
19	11, 18	eqeltrd 1546	. . . . . 6 |- (m e. NN0 -> (F` m) e. CC)
20	7	sumeq1d 6943	. . . . . . . . 9 |- (n = m -> sum_j e. (0...n)((A^j) / (!` j)) = sum_j e. (0...m)((A^j) / (!` j)))
21	7	sumeq1d 6943	. . . . . . . . 9 |- (n = m -> sum_k e. (0...n)((B^k) / (!` k)) = sum_k e. (0...m)((B^k) / (!` k)))
22	20, 21	opreq12d 3973	. . . . . . . 8 |- (n = m -> (sum_j e. (0...n)((A^j) / (!` j)) x. sum_k e. (0...n)((B^k) / (!` k))) = (sum_j e. (0...m)((A^j) / (!` j)) x. sum_k e. (0...m)((B^k) / (!` k))))
23		efaddlem27.4	. . . . . . . 8 |- H = {<.n, y>. | (n e. NN0 /\ y = (sum_j e. (0...n)((A^j) / (!` j)) x. sum_k e. (0...n)((B^k) / (!` k))))}
24		oprex 3978	. . . . . . . 8 |- (sum_j e. (0...m)((A^j) / (!` j)) x. sum_k e. (0...m)((B^k) / (!` k))) e. V
25	22, 23, 24	fvopab4 3775	. . . . . . 7 |- (m e. NN0 -> (H` m) = (sum_j e. (0...m)((A^j) / (!` j)) x. sum_k e. (0...m)((B^k) / (!` k))))
26		axmulcl 5256	. . . . . . . 8 |- ((sum_j e. (0...m)((A^j) / (!` j)) e. CC /\ sum_k e. (0...m)((B^k) / (!` k)) e. CC) -> (sum_j e. (0...m)((A^j) / (!` j)) x. sum_k e. (0...m)((B^k) / (!` k))) e. CC)
27		eftclt 7262	. . . . . . . . . . . 12 |- ((A e. CC /\ j e. NN0) -> ((A^j) / (!` j)) e. CC)
28	1, 27	mpan 694	. . . . . . . . . . 11 |- (j e. NN0 -> ((A^j) / (!` j)) e. CC)
29	12, 28	syl 10	. . . . . . . . . 10 |- (j e. (0...m) -> ((A^j) / (!` j)) e. CC)
30	29	rgen 1696	. . . . . . . . 9 |- A.j e. (0...m)((A^j) / (!` j)) e. CC
31		fsum0clt 6969	. . . . . . . . 9 |- ((m e. NN0 /\ A.j e. (0...m)((A^j) / (!` j)) e. CC) -> sum_j e. (0...m)((A^j) / (!` j)) e. CC)
32	30, 31	mpan2 695	. . . . . . . 8 |- (m e. NN0 -> sum_j e. (0...m)((A^j) / (!` j)) e. CC)
33		elfznn0t 6441	. . . . . . . . . . 11 |- (k e. (0...m) -> k e. NN0)
34		eftclt 7262	. . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> ((B^k) / (!` k)) e. CC)
35	2, 34	mpan 694	. . . . . . . . . . 11 |- (k e. NN0 -> ((B^k) / (!` k)) e. CC)
36	33, 35	syl 10	. . . . . . . . . 10 |- (k e. (0...m) -> ((B^k) / (!` k)) e. CC)
37	36	rgen 1696	. . . . . . . . 9 |- A.k e. (0...m)((B^k) / (!` k)) e. CC
38		fsum0clt 6969	. . . . . . . . 9 |- ((m e. NN0 /\ A.k e. (0...m)((B^k) / (!` k)) e. CC) -> sum_k e. (0...m)((B^k) / (!` k)) e. CC)
39	37, 38	mpan2 695	. . . . . . . 8 |- (m e. NN0 -> sum_k e. (0...m)((B^k) / (!` k)) e. CC)
40	26, 32, 39	sylanc 471	. . . . . . 7 |- (m e. NN0 -> (sum_j e. (0...m)((A^j) / (!` j)) x. sum_k e. (0...m)((B^k) / (!` k))) e. CC)
41	25, 40	eqeltrd 1546	. . . . . 6 |- (m e. NN0 -> (H` m) e. CC)
42	19, 41	jca 288	. . . . 5 |- (m e. NN0 -> ((F` m) e. CC /\ (H` m) e. CC))
43	6, 42	syl 10	. . . 4 |- (m e. NN -> ((F` m) e. CC /\ (H` m) e. CC))
44	43	rgen 1696	. . 3 |- A.m e. NN ((F` m) e. CC /\ (H` m) e. CC)
45	5, 44	pm3.2i 285	. 2 |- ((exp` (A + B)) e. CC /\ A.m e. NN ((F` m) e. CC /\ (H` m) e. CC))
46		eqid 1474	. . . . . . 7 |- (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2) = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
47		eqid 1474	. . . . . . 7 |- (2 x. ((2^(3^2)) x. ((4 x. (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2))^((4 x. (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)) + 3)))) = (2 x. ((2^(3^2)) x. ((4 x. (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2))^((4 x. (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)) + 3))))
48	1, 2, 46, 47	efaddlem25 7321	. . . . . 6 |- ((x e. RR /\ 0 < x) -> E.f e. NN A.m e. NN (f <_ m -> (abs` ((sum_j e. (0...m)((A^j) / (!` j)) x. sum_k e. (0...m)((B^k) / (!` k))) - sum_j e. (0...m)(((A + B)^j) / (!` j)))) < x))
49	25, 11	opreq12d 3973	. . . . . . . . . . . 12 |- (m e. NN0 -> ((H` m) - (F` m)) = ((sum_j e. (0