Theorem dfef2 7265

Description: Switch between definitions for df-ef 7256 that sum over NN0 or over NN. (Contributed by Steve Rodriguez, 30-Jun-2006.)

Hypothesis

Ref	Expression
dfef2.1	|- A e. CC

Assertion

Ref	Expression
dfef2	|- sum_k e. NN0 ((A^k) / (!` k)) = (1 + sum_k e. NN ({<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}` k))

Distinct variable group:   j,k,y,A

Proof of Theorem dfef2

Step	Hyp	Ref	Expression
1		opreq2 3967	. . . . . . 7 |- (j = k -> (A^j) = (A^k))
2		fveq2 3722	. . . . . . 7 |- (j = k -> (!` j) = (!` k))
3	1, 2	opreq12d 3976	. . . . . 6 |- (j = k -> ((A^j) / (!` j)) = ((A^k) / (!` k)))
4		eqid 1475	. . . . . 6 |- {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
5		oprex 3981	. . . . . 6 |- ((A^k) / (!` k)) e. V
6	3, 4, 5	fvopab4 3778	. . . . 5 |- (k e. NN0 -> ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}` k) = ((A^k) / (!` k)))
7		dfef2.1	. . . . . 6 |- A e. CC
8		eftclt 7261	. . . . . 6 |- ((A e. CC /\ k e. NN0) -> ((A^k) / (!` k)) e. CC)
9	7, 8	mpan 695	. . . . 5 |- (k e. NN0 -> ((A^k) / (!` k)) e. CC)
10	6, 9	eqeltrd 1547	. . . 4 |- (k e. NN0 -> ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}` k) e. CC)
11	10	rgen 1697	. . 3 |- A.k e. NN0 ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}` k) e. CC
12		eqid 1475	. . . . . 6 |- {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))} = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
13	12	efseq1ex 7264	. . . . 5 |- (A e. CC -> E.x( + seq1 {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) ~~> x)
14	7, 13	ax-mp 7	. . . 4 |- E.x( + seq1 {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) ~~> x
15		oprex 3981	. . . . . . . . . . 11 |- ((A^j) / (!` j)) e. V
16	15, 12	dmopab2 3617	. . . . . . . . . 10 |- dom {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))} = NN
17		reseq2 3367	. . . . . . . . . 10 |- (dom {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))} = NN -> ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` dom {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) = ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN))
18	16, 17	ax-mp 7	. . . . . . . . 9 |- ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` dom {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) = ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN)
19		eftclt 7261	. . . . . . . . . . . . 13 |- ((A e. CC /\ j e. NN0) -> ((A^j) / (!` j)) e. CC)
20	7, 19	mpan 695	. . . . . . . . . . . 12 |- (j e. NN0 -> ((A^j) / (!` j)) e. CC)
21	4, 20	fopab 3825	. . . . . . . . . . 11 |- {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}:NN0-->CC
22		ffun 3627	. . . . . . . . . . 11 |- ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}:NN0-->CC -> Fun {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))})
23	21, 22	ax-mp 7	. . . . . . . . . 10 |- Fun {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
24		nnnn0t 6074	. . . . . . . . . . . 12 |- (j e. NN -> j e. NN0)
25	24	anim1i 334	. . . . . . . . . . 11 |- ((j e. NN /\ y = ((A^j) / (!` j))) -> (j e. NN0 /\ y = ((A^j) / (!` j))))
26	25	ssopab2i 2821	. . . . . . . . . 10 |- {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))} (_ {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
27		funssres 3550	. . . . . . . . . 10 |- ((Fun {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} /\ {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))} (_ {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}) -> ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` dom {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))})
28	23, 26, 27	mp2an 697	. . . . . . . . 9 |- ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` dom {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
29	18, 28	eqtr3 1496	. . . . . . . 8 |- ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN) = {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}
30	29	opreq2i 3970	. . . . . . 7 |- ( + seq1 ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN)) = ( + seq1 {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))})
31		addex 5305	. . . . . . . 8 |- + e. V
32		nn0ex 6073	. . . . . . . . 9 |- NN0 e. V
33	32	opabex2 3608	. . . . . . . 8 |- {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} e. V
34	31, 33	seq1res 6291	. . . . . . 7 |- ( + seq1 ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} |` NN)) = ( + seq1 {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))})
35	30, 34	eqtr3 1496	. . . . . 6 |- ( + seq1 {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) = ( + seq1 {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))})
36	35	breq1i 2624	. . . . 5 |- (( + seq1 {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) ~~> x <-> ( + seq1 {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}) ~~> x)
37	36	exbii 1051	. . . 4 |- (E.x( + seq1 {<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}) ~~> x <-> E.x( + seq1 {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}) ~~> x)
38	14, 37	mpbi 189	. . 3 |- E.x( + seq1 {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}) ~~> x
39	33	isumnn0nn 7165	. . 3 |- ((A.k e. NN0 ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}` k) e. CC /\ E.x( + seq1 {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}) ~~> x) -> sum_k e. NN0 ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}` k) = (({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}` 0) + sum_k e. NN ({<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)