Theorem eirrlem2 7513

Description: Lemma for eirr 7517.

Hypotheses

Ref	Expression
eirrlem2.1	|- F = {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))}
eirrlem2.2	|- P e. ZZ
eirrlem2.3	|- Q e. NN

Assertion

Ref	Expression
eirrlem2	|- ((!` Q) x. ((P / Q) - sum_k e. (0...Q)(F` k))) e. ZZ

Distinct variable groups:   k,F   Q,j,k,y

Proof of Theorem eirrlem2

Step	Hyp	Ref	Expression
1		eirrlem2.3	. . . . . 6 |- Q e. NN
2	1	nnnn0i 6217	. . . . 5 |- Q e. NN0
3		faccl 7063	. . . . 5 |- (Q e. NN0 -> (!` Q) e. NN)
4	2, 3	ax-mp 7	. . . 4 |- (!` Q) e. NN
5	4	nncni 6019	. . 3 |- (!` Q) e. CC
6		eirrlem2.2	. . . . 5 |- P e. ZZ
7		zcn 6250	. . . . 5 |- (P e. ZZ -> P e. CC)
8	6, 7	ax-mp 7	. . . 4 |- P e. CC
9	1	nncni 6019	. . . 4 |- Q e. CC
10	1	nnne0i 6038	. . . 4 |- Q =/= 0
11	8, 9, 10	divcli 5799	. . 3 |- (P / Q) e. CC
12		nn0uz 6498	. . . . 5 |- NN0 = (ZZ>` 0)
13	2, 12	eleqtri 1583	. . . 4 |- Q e. (ZZ>` 0)
14		fzssuz 6565	. . . . 5 |- (0...Q) (_ (ZZ>` 0)
15		elnn0uz 6501	. . . . . . 7 |- (k e. NN0 <-> k e. (ZZ>` 0))
16		eirrlem2.1	. . . . . . . . 9 |- F = {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))}
17	16	eftval 7439	. . . . . . . 8 |- (k e. NN0 -> (F` k) = ((1^k) / (!` k)))
18		ax1cn 5358	. . . . . . . . 9 |- 1 e. CC
19		eftcl 7426	. . . . . . . . 9 |- ((1 e. CC /\ k e. NN0) -> ((1^k) / (!` k)) e. CC)
20	18, 19	mpan 698	. . . . . . . 8 |- (k e. NN0 -> ((1^k) / (!` k)) e. CC)
21	17, 20	eqeltrd 1585	. . . . . . 7 |- (k e. NN0 -> (F` k) e. CC)
22	15, 21	sylbir 199	. . . . . 6 |- (k e. (ZZ>` 0) -> (F` k) e. CC)
23	22	rgen 1736	. . . . 5 |- A.k e. (ZZ>` 0)(F` k) e. CC
24		ssralv 2158	. . . . 5 |- ((0...Q) (_ (ZZ>` 0) -> (A.k e. (ZZ>` 0)(F` k) e. CC -> A.k e. (0...Q)(F` k) e. CC))
25	14, 23, 24	mp2 43	. . . 4 |- A.k e. (0...Q)(F` k) e. CC
26		fsumcl 7138	. . . 4 |- ((Q e. (ZZ>` 0) /\ A.k e. (0...Q)(F` k) e. CC) -> sum_k e. (0...Q)(F` k) e. CC)
27	13, 25, 26	mp2an 700	. . 3 |- sum_k e. (0...Q)(F` k) e. CC
28	5, 11, 27	subdii 5518	. 2 |- ((!` Q) x. ((P / Q) - sum_k e. (0...Q)(F` k))) = (((!` Q) x. (P / Q)) - ((!` Q) x. sum_k e. (0...Q)(F` k)))
29		facnn2 7062	. . . . . . . . 9 |- (Q e. NN -> (!` Q) = ((!` (Q - 1)) x. Q))
30	1, 29	ax-mp 7	. . . . . . . 8 |- (!` Q) = ((!` (Q - 1)) x. Q)
31	30	opreq2i 4048	. . . . . . 7 |- (((!` (Q - 1)) x. P) / (!` Q)) = (((!` (Q - 1)) x. P) / ((!` (Q - 1)) x. Q))
32	9, 10	pm3.2i 283	. . . . . . . 8 |- (Q e. CC /\ Q =/= 0)
33		nnm1nn0 6286	. . . . . . . . . 10 |- (Q e. NN -> (Q - 1) e. NN0)
34		faccl 7063	. . . . . . . . . 10 |- ((Q - 1) e. NN0 -> (!` (Q - 1)) e. NN)
35		nncn 6017	. . . . . . . . . . 11 |- ((!` (Q - 1)) e. NN -> (!` (Q - 1)) e. CC)
36		nnne0 6036	. . . . . . . . . . 11 |- ((!` (Q - 1)) e. NN -> (!` (Q - 1)) =/= 0)
37	35, 36	jca 286	. . . . . . . . . 10 |- ((!` (Q - 1)) e. NN -> ((!` (Q - 1)) e. CC /\ (!` (Q - 1)) =/= 0))
38	33, 34, 37	3syl 20	. . . . . . . . 9 |- (Q e. NN -> ((!` (Q - 1)) e. CC /\ (!` (Q - 1)) =/= 0))
39	1, 38	ax-mp 7	. . . . . . . 8 |- ((!` (Q - 1)) e. CC /\ (!` (Q - 1)) =/= 0)
40		divcan5 5863	. . . . . . . 8 |- ((P e. CC /\ (Q e. CC /\ Q =/= 0) /\ ((!` (Q - 1)) e. CC /\ (!` (Q - 1)) =/= 0)) -> (((!` (Q - 1)) x. P) / ((!` (Q - 1)) x. Q)) = (P / Q))
41	8, 32, 39, 40	mp3an 919	. . . . . . 7 |- (((!` (Q - 1)) x. P) / ((!` (Q - 1)) x. Q)) = (P / Q)
42	31, 41	eqtri 1532	. . . . . 6 |- (((!` (Q - 1)) x. P) / (!` Q)) = (P / Q)
43	42	opreq2i 4048	. . . . 5 |- ((!` Q) x. (((!` (Q - 1)) x. P) / (!` Q))) = ((!` Q) x. (P / Q))
44	39	pm3.26i 318	. . . . . . 7 |- (!` (Q - 1)) e. CC
45	44, 8	mulcli 5410	. . . . . 6 |- ((!` (Q - 1)) x. P) e. CC
46	4	nnne0i 6038	. . . . . 6 |- (!` Q) =/= 0
47	45, 5, 46	divcan2i 5805	. . . . 5 |- ((!` Q) x. (((!` (Q - 1)) x. P) / (!` Q))) = ((!` (Q - 1)) x. P)
48	43, 47	eqtr3i 1534	. . . 4 |- ((!` Q) x. (P / Q)) = ((!` (Q - 1)) x. P)
49		nnz 6263	. . . . . . 7 |- ((!` (Q - 1)) e. NN -> (!` (Q - 1)) e. ZZ)
50	33, 34, 49	3syl 20	. . . . . 6 |- (Q e. NN -> (!` (Q - 1)) e. ZZ)
51	1, 50	ax-mp 7	. . . . 5 |- (!` (Q - 1)) e. ZZ
52		zmulcl 6290	. . . . 5 |- (((!` (Q - 1)) e. ZZ /\ P e. ZZ) -> ((!` (Q - 1)) x. P) e. ZZ)
53	51, 6, 52	mp2an 700	. . . 4 |- ((!` (Q - 1)) x. P) e. ZZ
54	48, 53	eqeltri 1581	. . 3 |- ((!` Q) x. (P / Q)) e. ZZ
55		fsummulc1 7156	. . . . 5 |- ((Q e. (ZZ>` 0) /\ (!` Q) e. CC /\ A.k e. (0...Q)(F` k) e. CC) -> ((!` Q) x. sum_k e. (0...Q)(F` k)) = sum_k e. (0...Q)((!` Q) x. (F` k)))
56	13, 5, 25, 55	mp3an 919	. . . 4 |- ((!` Q) x. sum_k e. (0...Q)(F` k)) = sum_k e. (0...Q)((!` Q) x. (F` k))
57		elfznn0 6556	. . . . . . . . 9 |- (k e. (0...Q) -> k e. NN0)
58		1exp 6707	. . . . . . . . . . . . 13 |- (k e. NN0 -> (1^k) = 1)
59	58	opreq1d 4051	. . . . . . . . . . . 12 |- (k e. NN0 -> ((1^k) / (!` k)) = (1 / (!` k)))
60	17, 59	eqtrd 1544	. . . . . . . . . . 11 |- (k e. NN0 -> (F` k) = (1 / (!` k)))
61	60	opreq2d 4052	. . . . . . . . . 10 |- (k e. NN0 -> ((!` Q) x. (F` k)) = ((!` Q) x. (1 / (!` k))))
62		faccl 7063	. . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. NN)
63	5	a1i 8	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` Q) e. CC)
64		nncn 6017	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) e. CC)
65		nnne0 6036	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) =/= 0)
66	63, 64, 65	3jca 822	. . . . . . . . . . 11 |- ((!` k) e. NN -> ((!` Q) e. CC /\ (!` k) e. CC /\ (!` k) =/= 0))
67		divrec 5822	. . . . . . . . . . 11 |- (((!` Q) e. CC /\ (!` k) e. CC /\ (!` k) =/= 0) -> ((!` Q) / (!` k)) = ((!` Q) x. (1 / (!` k))))
68	62, 66, 67	3syl 20	. . . . . . . . . 10 |- (k e. NN0 -> ((!` Q) / (!` k)) = ((!` Q) x. (1 / (!` k))))
69	61, 68	eqtr4d 1547	. . . . . . . . 9 |- (k e. NN0 -> ((!` Q) x. (F` k)) = ((!` Q) / (!` k)))
70	57, 69	syl 10	. . . . . . . 8 |- (k e. (0...Q) -> ((!` Q) x. (F` k)) = ((!` Q) / (!` k)))
71		permnn 7096	. . . . . . . . 9 |- ((Q e. NN0 /\ k e. (0...Q)) -> ((!` Q) / (!` k)) e. NN)
72	2, 71	mpan 698	. . . . . . . 8 |- (k e. (0...Q) -> ((!` Q) / (!` k)) e. NN)
73	70, 72	eqeltrd 1585	. . . . . . 7 |- (k e. (0...Q) -> ((!` Q) x. (F` k)) e. NN)
74		nnz 6263	. . . . . . 7 |- (((!` Q) x. (F` k)) e. NN -> ((!` Q) x. (F` k)) e. ZZ)
75	73, 74	syl 10	. . . . . 6 |- (k e. (0...Q) -> ((!` Q) x. (F` k)) e. ZZ)
76	75	rgen 1736	. . . . 5 |- A.k e. (0...Q)((!` Q) x. (F` k)) e. ZZ
77		zaddcl 6275	. . . . . 6 |- ((x e.