Theorem ef01tllem1 7333

Description: Lemma for ef01tlub 7335.

Hypotheses

Ref	Expression
ef1tllem.1	|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
ef01tllem1.2	|- G = {<.j, y>. | (j e. NN0 /\ y = ((A^(j - M)) / (!` j)))}
ef01tllem1.3	|- M e. NN
ef01tllem1.4	|- A e. RR
ef01tllem1.5	|- A =/= 0

Assertion

Ref	Expression
ef01tllem1	|- (<.M, + >. seq G) ~~> (sum_k e. (ZZ>` M)(F` k) / (A^M))

Distinct variable groups:   A,j,k,y   k,F   k,G   j,M,k,y

Proof of Theorem ef01tllem1

Step	Hyp	Ref	Expression
1		ef01tllem1.3	. . . . 5 |- M e. NN
2		nnzt 6108	. . . . 5 |- (M e. NN -> M e. ZZ)
3	1, 2	ax-mp 7	. . . 4 |- M e. ZZ
4		ef01tllem1.4	. . . . . 6 |- A e. RR
5	4	recn 5294	. . . . 5 |- A e. CC
6		ef1tllem.1	. . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
7	6	eftlext 7328	. . . . 5 |- ((A e. CC /\ M e. NN) -> E.x(<.M, + >. seq F) ~~> x)
8	5, 1, 7	mp2an 696	. . . 4 |- E.x(<.M, + >. seq F) ~~> x
9		nn0ex 6060	. . . . . 6 |- NN0 e. V
10	9, 6	fopabex2 3604	. . . . 5 |- F e. V
11	10	isumclim2t 7142	. . . 4 |- ((M e. ZZ /\ E.x(<.M, + >. seq F) ~~> x) -> (<.M, + >. seq F) ~~> sum_k e. (ZZ>` M)(F` k))
12	3, 8, 11	mp2an 696	. . 3 |- (<.M, + >. seq F) ~~> sum_k e. (ZZ>` M)(F` k)
13	1	nnnn0 6062	. . . . . 6 |- M e. NN0
14		expclt 6521	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> (A^M) e. CC)
15	5, 13, 14	mp2an 696	. . . . 5 |- (A^M) e. CC
16		ef01tllem1.5	. . . . . 6 |- A =/= 0
17		expne0t 6526	. . . . . . 7 |- ((A e. CC /\ M e. NN) -> (A =/= 0 <-> (A^M) =/= 0))
18	5, 1, 17	mp2an 696	. . . . . 6 |- (A =/= 0 <-> (A^M) =/= 0)
19	16, 18	mpbi 189	. . . . 5 |- (A^M) =/= 0
20	15, 19	reccl 5690	. . . 4 |- (1 / (A^M)) e. CC
21		elnn0uz 6381	. . . . . . . . . 10 |- (M e. NN0 <-> M e. (ZZ>` 0))
22	13, 21	mpbi 189	. . . . . . . . 9 |- M e. (ZZ>` 0)
23		uztrn 6368	. . . . . . . . 9 |- ((k e. (ZZ>` M) /\ M e. (ZZ>` 0)) -> k e. (ZZ>` 0))
24	22, 23	mpan2 695	. . . . . . . 8 |- (k e. (ZZ>` M) -> k e. (ZZ>` 0))
25		elnn0uz 6381	. . . . . . . 8 |- (k e. NN0 <-> k e. (ZZ>` 0))
26	24, 25	sylibr 200	. . . . . . 7 |- (k e. (ZZ>` M) -> k e. NN0)
27	6	eftval 7266	. . . . . . . 8 |- (k e. NN0 -> (F` k) = ((A^k) / (!` k)))
28		eftclt 7253	. . . . . . . . 9 |- ((A e. CC /\ k e. NN0) -> ((A^k) / (!` k)) e. CC)
29	5, 28	mpan 694	. . . . . . . 8 |- (k e. NN0 -> ((A^k) / (!` k)) e. CC)
30	27, 29	eqeltrd 1545	. . . . . . 7 |- (k e. NN0 -> (F` k) e. CC)
31	26, 30	syl 10	. . . . . 6 |- (k e. (ZZ>` M) -> (F` k) e. CC)
32		opreq1 3959	. . . . . . . . . . . 12 |- (j = k -> (j - M) = (k - M))
33	32	opreq2d 3967	. . . . . . . . . . 11 |- (j = k -> (A^(j - M)) = (A^(k - M)))
34		fveq2 3715	. . . . . . . . . . 11 |- (j = k -> (!` j) = (!` k))
35	33, 34	opreq12d 3969	. . . . . . . . . 10 |- (j = k -> ((A^(j - M)) / (!` j)) = ((A^(k - M)) / (!` k)))
36		ef01tllem1.2	. . . . . . . . . 10 |- G = {<.j, y>. | (j e. NN0 /\ y = ((A^(j - M)) / (!` j)))}
37		oprex 3974	. . . . . . . . . 10 |- ((A^(k - M)) / (!` k)) e. V
38	35, 36, 37	fvopab4 3771	. . . . . . . . 9 |- (k e. NN0 -> (G` k) = ((A^(k - M)) / (!` k)))
39	26, 38	syl 10	. . . . . . . 8 |- (k e. (ZZ>` M) -> (G` k) = ((A^(k - M)) / (!` k)))
40		expsubt 6537	. . . . . . . . . 10 |- (((A e. CC /\ k e. NN0 /\ M e. NN0) /\ (A =/= 0 /\ M <_ k)) -> (A^(k - M)) = ((A^k) / (A^M)))
41	5	a1i 8	. . . . . . . . . . 11 |- (k e. (ZZ>` M) -> A e. CC)
42	13	a1i 8	. . . . . . . . . . 11 |- (k e. (ZZ>` M) -> M e. NN0)
43	41, 26, 42	3jca 818	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> (A e. CC /\ k e. NN0 /\ M e. NN0))
44		eluzle 6365	. . . . . . . . . . 11 |- (k e. (ZZ>` M) -> M <_ k)
45	44, 16	jctil 292	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> (A =/= 0 /\ M <_ k))
46	40, 43, 45	sylanc 471	. . . . . . . . 9 |- (k e. (ZZ>` M) -> (A^(k - M)) = ((A^k) / (A^M)))
47	46	opreq1d 3966	. . . . . . . 8 |- (k e. (ZZ>` M) -> ((A^(k - M)) / (!` k)) = (((A^k) / (A^M)) / (!` k)))
48		divdiv23t 5756	. . . . . . . . . 10 |- ((((A^k) e. CC /\ (A^M) e. CC /\ (!` k) e. CC) /\ ((A^M) =/= 0 /\ (!` k) =/= 0)) -> (((A^k) / (A^M)) / (!` k)) = (((A^k) / (!` k)) / (A^M)))
49		expclt 6521	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
50	5, 49	mpan 694	. . . . . . . . . . 11 |- (k e. NN0 -> (A^k) e. CC)
51	15	a1i 8	. . . . . . . . . . 11 |- (k e. NN0 -> (A^M) e. CC)
52		facclt 6885	. . . . . . . . . . . 12 |- (k e. NN0 -> (!` k) e. NN)
53		nncnt 5886	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) e. CC)
54	52, 53	syl 10	. . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. CC)
55	50, 51, 54	3jca 818	. . . . . . . . . 10 |- (k e. NN0 -> ((A^k) e. CC /\ (A^M) e. CC /\ (!` k) e. CC))
56		facne0t 6886	. . . . . . . . . . 11 |- (k e. NN0 -> (!` k) =/= 0)
57	56, 19	jctil 292	. . . . . . . . . 10 |- (k e. NN0 -> ((A^M) =/= 0 /\ (!` k) =/= 0))
58	48, 55, 57	sylanc 471	. . . . . . . . 9 |- (k e. NN0 -> (((A^k) / (A^M)) / (!` k)) = (((A^k) / (!` k)) / (A^M)))
59	26, 58	syl 10	. . . . . . . 8 |- (k e. (ZZ>` M) -> (((A^k) / (A^M)) / (!` k)) = (((A^k) / (!` k)) / (A^M)))
60	39, 47, 59	3eqtrd 1508	. . . . . . 7 |- (k e. (ZZ>` M) -> (G` k) = (((A^k) / (!` k)) / (A^M)))
61	27	opreq2d 3967	. . . . . . . . 9 |- (k e. NN0 -> ((1 / (A^M)) x. (F` k)) = ((1 / (A^M)) x. ((A^k) / (!` k))))
62		divrec2t 5711	. . . . . . . . . 10 |- ((((A^k) / (!` k)) e. CC /\ (A^M) e. CC /\ (A^M) =/= 0) -> (((A^k) / (!` k)) / (A^M)) = ((1 / (A^M)) x. ((A^k) / (!` k))))
63		divclt 5689	. . . . . . . . . . 11 |- (((A^k) e. CC /\ (!` k) e. CC /\ (!` k) =/= 0) -> ((A^k) / (!` k)) e. CC)
64	63, 50, 54, 56	syl3anc 857	. . . . . . . . . 10 |- (k e. NN0 -> ((A^k) / (!` k)) e. CC)
65	19	a1i 8	. . . . . . . . . 10 |- (k e. NN0 -> (A^M) =/= 0)
66	62, 64, 51, 65	syl3anc 857	. . . . . . . . 9 |- (k e. NN0 -> (((A^k) / (!` k)) / (A^M)) = ((1 / (A^M)) x. ((A^k) / (!` k))))
67	61, 66	eqtr4d 1507	. . . . . . . 8 |- (k e. NN0 -> ((1 / (A^M)) x. (F` k)) = (((A^k) / (!` k)) / (A^M)))
68	26, 67	syl 10	. . . . . . 7 |- (k e. (ZZ>` M) -> ((1 / (A^M)) x. (F` k)) = (((A^k) / (!` k)) / (A^M)))
69	60, 68	eqtr4d 1507	. . . . . 6 |- (k e. (ZZ>` M) -> (G` k) = ((1 / (A^M)) x. (F` k)))
70	31, 69	jca 288	. . . . 5 |- (k e. (ZZ>` M) -> ((F` k) e. CC /\ (G` k) = ((1 / (A^M)) x. (F` k))))
71	70	rgen 1695	. . . 4 |- A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = ((1 / (A^M)) x. (F` k)))
72		sumex 6927	. . . . 5 |- sum_k e. (ZZ>` M)(F` k) e. V
73	9, 36	fopabex2 3604	. . . . 5 |- G e. V
74	72, 10, 73	iserzmulc1 7080	. . . 4 |- (