Theorem eirrlem2 7331

Description: Lemma for eirr 7335.

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	nnnn0 6054	. . . . 5 |- Q e. NN0
3		facclt 6877	. . . . 5 |- (Q e. NN0 -> (!` Q) e. NN)
4	2, 3	ax-mp 7	. . . 4 |- (!` Q) e. NN
5	4	nncn 5880	. . 3 |- (!` Q) e. CC
6		eirrlem2.2	. . . . 5 |- P e. ZZ
7		zcnt 6087	. . . . 5 |- (P e. ZZ -> P e. CC)
8	6, 7	ax-mp 7	. . . 4 |- P e. CC
9	1	nncn 5880	. . . 4 |- Q e. CC
10	1	nnne0 5899	. . . 4 |- Q =/= 0
11	8, 9, 10	divcl 5679	. . 3 |- (P / Q) e. CC
12		nn0uz 6370	. . . . 5 |- NN0 = (ZZ>` 0)
13	2, 12	eleqtr 1538	. . . 4 |- Q e. (ZZ>` 0)
14		fzssuzt 6437	. . . . 5 |- (0...Q) (_ (ZZ>` 0)
15		elnn0uz 6373	. . . . . . 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 7258	. . . . . . . 8 |- (k e. NN0 -> (F` k) = ((1^k) / (!` k)))
18		ax1cn 5241	. . . . . . . . 9 |- 1 e. CC
19		eftclt 7245	. . . . . . . . 9 |- ((1 e. CC /\ k e. NN0) -> ((1^k) / (!` k)) e. CC)
20	18, 19	mpan 693	. . . . . . . 8 |- (k e. NN0 -> ((1^k) / (!` k)) e. CC)
21	17, 20	eqeltrd 1540	. . . . . . 7 |- (k e. NN0 -> (F` k) e. CC)
22	15, 21	sylbir 201	. . . . . 6 |- (k e. (ZZ>` 0) -> (F` k) e. CC)
23	22	rgen 1690	. . . . 5 |- A.k e. (ZZ>` 0)(F` k) e. CC
24		ssralv 2104	. . . . 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		fsumclt 6953	. . . 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 695	. . 3 |- sum_k e. (0...Q)(F` k) e. CC
28	5, 11, 27	subdi 5401	. 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		facnn2t 6876	. . . . . . . . 9 |- (Q e. NN -> (!` Q) = ((!` (Q - 1)) x. Q))
30	1, 29	ax-mp 7	. . . . . . . 8 |- (!` Q) = ((!` (Q - 1)) x. Q)
31	30	opreq2i 3957	. . . . . . 7 |- (((!` (Q - 1)) x. P) / (!` Q)) = (((!` (Q - 1)) x. P) / ((!` (Q - 1)) x. Q))
32	9, 10	pm3.2i 285	. . . . . . . 8 |- (Q e. CC /\ Q =/= 0)
33		nnm1nn0t 6123	. . . . . . . . . 10 |- (Q e. NN -> (Q - 1) e. NN0)
34		facclt 6877	. . . . . . . . . 10 |- ((Q - 1) e. NN0 -> (!` (Q - 1)) e. NN)
35		nncnt 5878	. . . . . . . . . . 11 |- ((!` (Q - 1)) e. NN -> (!` (Q - 1)) e. CC)
36		nnne0t 5897	. . . . . . . . . . 11 |- ((!` (Q - 1)) e. NN -> (!` (Q - 1)) =/= 0)
37	35, 36	jca 288	. . . . . . . . . 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		divcan5t 5737	. . . . . . . 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 913	. . . . . . 7 |- (((!` (Q - 1)) x. P) / ((!` (Q - 1)) x. Q)) = (P / Q)
42	31, 41	eqtr 1487	. . . . . 6 |- (((!` (Q - 1)) x. P) / (!` Q)) = (P / Q)
43	42	opreq2i 3957	. . . . 5 |- ((!` Q) x. (((!` (Q - 1)) x. P) / (!` Q))) = ((!` Q) x. (P / Q))
44	39	pm3.26i 320	. . . . . . 7 |- (!` (Q - 1)) e. CC
45	44, 8	mulcl 5293	. . . . . 6 |- ((!` (Q - 1)) x. P) e. CC
46	4	nnne0 5899	. . . . . 6 |- (!` Q) =/= 0
47	5, 45, 46	divcan2 5685	. . . . 5 |- ((!` Q) x. (((!` (Q - 1)) x. P) / (!` Q))) = ((!` (Q - 1)) x. P)
48	43, 47	eqtr3 1489	. . . 4 |- ((!` Q) x. (P / Q)) = ((!` (Q - 1)) x. P)
49		nnzt 6100	. . . . . . 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		zmulclt 6127	. . . . 5 |- (((!` (Q - 1)) e. ZZ /\ P e. ZZ) -> ((!` (Q - 1)) x. P) e. ZZ)
53	51, 6, 52	mp2an 695	. . . 4 |- ((!` (Q - 1)) x. P) e. ZZ
54	48, 53	eqeltr 1536	. . 3 |- ((!` Q) x. (P / Q)) e. ZZ
55		fsummulc1 6971	. . . . 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 913	. . . 4 |- ((!` Q) x. sum_k e. (0...Q)(F` k)) = sum_k e. (0...Q)((!` Q) x. (F` k))
57		elfznn0t 6428	. . . . . . . . 9 |- (k e. (0...Q) -> k e. NN0)
58		1expt 6516	. . . . . . . . . . . . 13 |- (k e. NN0 -> (1^k) = 1)
59	58	opreq1d 3960	. . . . . . . . . . . 12 |- (k e. NN0 -> ((1^k) / (!` k)) = (1 / (!` k)))
60	17, 59	eqtrd 1499	. . . . . . . . . . 11 |- (k e. NN0 -> (F` k) = (1 / (!` k)))
61	60	opreq2d 3961	. . . . . . . . . 10 |- (k e. NN0 -> ((!` Q) x. (F` k)) = ((!` Q) x. (1 / (!` k))))
62		facclt 6877	. . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. NN)
63	5	a1i 8	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` Q) e. CC)
64		nncnt 5878	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) e. CC)
65		nnne0t 5897	. . . . . . . . . . . 12 |- ((!` k) e. NN -> (!` k) =/= 0)
66	63, 64, 65	3jca 817	. . . . . . . . . . 11 |- ((!` k) e. NN -> ((!` Q) e. CC /\ (!` k) e. CC /\ (!` k) =/= 0))
67		divrect 5702	. . . . . . . . . . 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 1502	. . . . . . . . 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		permnnt 6911	. . . . . . . . 9 |- ((Q e. NN0 /\ k e. (0...Q)) -> ((!` Q) / (!` k)) e. NN)
72	2, 71	mpan 693	. . . . . . . 8 |- (k e. (0...Q) -> ((!` Q) / (!` k)) e. NN)
73	70, 72	eqeltrd 1540	. . . . . . 7 |- (k e. (0...Q) -> ((!` Q) x. (F` k)) e. NN)
74		nnzt 6100	. . . . . . 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 1690	. . . . 5 |- A.k e. (0...Q)((!` Q) x. (F` k)) e. ZZ
77		zaddclt 6112	. . . . . 6 |- ((x e. ZZ