Theorem eirrlem3 7391

Description: Lemma for eirr 7394.

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
eirrlem3	|- ((!` Q) x. sum_k e. (ZZ>` (Q + 1))(F` k)) < 1

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

Proof of Theorem eirrlem3

Step	Hyp	Ref	Expression
1		eirrlem2.3	. . . . . . 7 |- Q e. NN
2		peano2nn 5935	. . . . . . 7 |- (Q e. NN -> (Q + 1) e. NN)
3	1, 2	ax-mp 7	. . . . . 6 |- (Q + 1) e. NN
4		eqid 1475	. . . . . 6 |- 1 = 1
5		eirrlem2.1	. . . . . . 7 |- F = {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))}
6	5	ef1tlub 7382	. . . . . 6 |- (((Q + 1) e. NN /\ 1 = 1) -> sum_k e. (ZZ>` (Q + 1))(F` k) <_ (((Q + 1) + 1) / ((!` (Q + 1)) x. (Q + 1))))
7	3, 4, 6	mp2an 697	. . . . 5 |- sum_k e. (ZZ>` (Q + 1))(F` k) <_ (((Q + 1) + 1) / ((!` (Q + 1)) x. (Q + 1)))
8	1	nncn 5932	. . . . . . . 8 |- Q e. CC
9		ax1cn 5269	. . . . . . . 8 |- 1 e. CC
10	8, 9, 9	addass 5324	. . . . . . 7 |- ((Q + 1) + 1) = (Q + (1 + 1))
11		df-2 5970	. . . . . . . 8 |- 2 = (1 + 1)
12	11	opreq2i 3972	. . . . . . 7 |- (Q + 2) = (Q + (1 + 1))
13	10, 12	eqtr4 1498	. . . . . 6 |- ((Q + 1) + 1) = (Q + 2)
14	1	nnnn0 6107	. . . . . . . . . 10 |- Q e. NN0
15		facclt 6940	. . . . . . . . . 10 |- (Q e. NN0 -> (!` Q) e. NN)
16	14, 15	ax-mp 7	. . . . . . . . 9 |- (!` Q) e. NN
17	16	nncn 5932	. . . . . . . 8 |- (!` Q) e. CC
18	3	nncn 5932	. . . . . . . 8 |- (Q + 1) e. CC
19	17, 18, 18	mulass 5325	. . . . . . 7 |- (((!` Q) x. (Q + 1)) x. (Q + 1)) = ((!` Q) x. ((Q + 1) x. (Q + 1)))
20		facp1t 6936	. . . . . . . . 9 |- (Q e. NN0 -> (!` (Q + 1)) = ((!` Q) x. (Q + 1)))
21	14, 20	ax-mp 7	. . . . . . . 8 |- (!` (Q + 1)) = ((!` Q) x. (Q + 1))
22	21	opreq1i 3971	. . . . . . 7 |- ((!` (Q + 1)) x. (Q + 1)) = (((!` Q) x. (Q + 1)) x. (Q + 1))
23	18	sqval 6614	. . . . . . . 8 |- ((Q + 1)^2) = ((Q + 1) x. (Q + 1))
24	23	opreq2i 3972	. . . . . . 7 |- ((!` Q) x. ((Q + 1)^2)) = ((!` Q) x. ((Q + 1) x. (Q + 1)))
25	19, 22, 24	3eqtr4 1505	. . . . . 6 |- ((!` (Q + 1)) x. (Q + 1)) = ((!` Q) x. ((Q + 1)^2))
26	13, 25	opreq12i 3973	. . . . 5 |- (((Q + 1) + 1) / ((!` (Q + 1)) x. (Q + 1))) = ((Q + 2) / ((!` Q) x. ((Q + 1)^2)))
27	7, 26	breqtr 2638	. . . 4 |- sum_k e. (ZZ>` (Q + 1))(F` k) <_ ((Q + 2) / ((!` Q) x. ((Q + 1)^2)))
28	16	nngt0 5950	. . . . 5 |- 0 < (!` Q)
29		nnzt 6153	. . . . . . . 8 |- ((Q + 1) e. NN -> (Q + 1) e. ZZ)
30	3, 29	ax-mp 7	. . . . . . 7 |- (Q + 1) e. ZZ
31	3	nnnn0 6107	. . . . . . . . . . 11 |- (Q + 1) e. NN0
32		nn0uz 6438	. . . . . . . . . . 11 |- NN0 = (ZZ>` 0)
33	31, 32	eleqtr 1546	. . . . . . . . . 10 |- (Q + 1) e. (ZZ>` 0)
34		uztrn 6428	. . . . . . . . . . 11 |- ((k e. (ZZ>` (Q + 1)) /\ (Q + 1) e. (ZZ>` 0)) -> k e. (ZZ>` 0))
35		elnn0uz 6441	. . . . . . . . . . 11 |- (k e. NN0 <-> k e. (ZZ>` 0))
36	34, 35	sylibr 200	. . . . . . . . . 10 |- ((k e. (ZZ>` (Q + 1)) /\ (Q + 1) e. (ZZ>` 0)) -> k e. NN0)
37	33, 36	mpan2 696	. . . . . . . . 9 |- (k e. (ZZ>` (Q + 1)) -> k e. NN0)
38	5	eftval 7316	. . . . . . . . . 10 |- (k e. NN0 -> (F` k) = ((1^k) / (!` k)))
39		1re 5435	. . . . . . . . . . 11 |- 1 e. RR
40		reeftclt 7374	. . . . . . . . . . 11 |- ((1 e. RR /\ k e. NN0) -> ((1^k) / (!` k)) e. RR)
41	39, 40	mpan 695	. . . . . . . . . 10 |- (k e. NN0 -> ((1^k) / (!` k)) e. RR)
42	38, 41	eqeltrd 1548	. . . . . . . . 9 |- (k e. NN0 -> (F` k) e. RR)
43	37, 42	syl 10	. . . . . . . 8 |- (k e. (ZZ>` (Q + 1)) -> (F` k) e. RR)
44	43	rgen 1698	. . . . . . 7 |- A.k e. (ZZ>` (Q + 1))(F` k) e. RR
45	5	eftlext 7378	. . . . . . . 8 |- ((1 e. CC /\ (Q + 1) e. NN) -> E.x(<.(Q + 1), + >. seq F) ~~> x)
46	9, 3, 45	mp2an 697	. . . . . . 7 |- E.x(<.(Q + 1), + >. seq F) ~~> x
47		nn0ex 6105	. . . . . . . . 9 |- NN0 e. V
48	47, 5	fopabex2 3612	. . . . . . . 8 |- F e. V
49	48	isumreclt 7210	. . . . . . 7 |- (((Q + 1) e. ZZ /\ A.k e. (ZZ>` (Q + 1))(F` k) e. RR /\ E.x(<.(Q + 1), + >. seq F) ~~> x) -> sum_k e. (ZZ>` (Q + 1))(F` k) e. RR)
50	30, 44, 46, 49	mp3an 916	. . . . . 6 |- sum_k e. (ZZ>` (Q + 1))(F` k) e. RR
51	1	nnre 5931	. . . . . . . 8 |- Q e. RR
52		2re 5979	. . . . . . . 8 |- 2 e. RR
53	51, 52	readdcl 5334	. . . . . . 7 |- (Q + 2) e. RR
54	16	nnre 5931	. . . . . . . 8 |- (!` Q) e. RR
55	3	nnre 5931	. . . . . . . . 9 |- (Q + 1) e. RR
56	55	resqcl 6623	. . . . . . . 8 |- ((Q + 1)^2) e. RR
57	54, 56	remulcl 5335	. . . . . . 7 |- ((!` Q) x. ((Q + 1)^2)) e. RR
58	18	sqcl 6615	. . . . . . . 8 |- ((Q + 1)^2) e. CC
59	16	nnne0 5951	. . . . . . . 8 |- (!` Q) =/= 0
60	3	nnne0 5951	. . . . . . . . 9 |- (Q + 1) =/= 0
61		sqne0t 6620	. . . . . . . . . 10 |- ((Q + 1) e. CC -> (((Q + 1)^2) =/= 0 <-> (Q + 1) =/= 0))
62	18, 61	ax-mp 7	. . . . . . . . 9 |- (((Q + 1)^2) =/= 0 <-> (Q + 1) =/= 0)
63	60, 62	mpbir 190	. . . . . . . 8 |- ((Q + 1)^2) =/= 0
64	17, 58, 59, 63	muln0 5699	. . . . . . 7 |- ((!` Q) x. ((Q + 1)^2)) =/= 0
65	53, 57, 64	redivcl 5798	. . . . . 6 |- ((Q + 2) / ((!` Q) x. ((Q + 1)^2))) e. RR
66	50, 65, 54	lemul2 5836	. . . . 5 |- (0 < (!` Q) -> (sum_k e. (ZZ>` (Q + 1))(F` k) <_ ((Q + 2) / ((!` Q) x. ((Q + 1)^2))) <-> ((!` Q) x. sum_k e. (ZZ>` (Q + 1))(F` k)) <_ ((!` Q) x. ((Q + 2) / ((!` Q) x. ((Q + 1)^2))))))
67	28, 66	ax-mp 7	. . . 4 |- (sum_k e. (ZZ>` (Q + 1))(F` k) <_ ((Q + 2) / ((!` Q) x. ((Q + 1)^2))) <-> ((!` Q) x. sum_k e. (ZZ>` (Q + 1))(F` k)) <_ ((!` Q) x. ((Q + 2) / ((!` Q) x. ((Q + 1)^2)))))
68	27, 67	mpbi 189	. . 3 |- ((!` Q) x. sum_k e. (ZZ>` (Q + 1))(F` k)) <_ ((!` Q) x. ((Q + 2) / ((!` Q) x. ((Q + 1)^2))))
69	53	recn 5314	. . . . 5 |- (Q + 2) e. CC
70	17, 58	mulcl 5321	. . . . 5 |- ((!` Q) x. ((Q + 1)^2)) e. CC
71	17, 69, 70, 64	divass 5746	. . . 4 |- (((!` Q) x. (Q + 2)) / ((!` Q) x. ((Q + 1)^2))) = ((!` Q) x. ((Q + 2) / ((!` Q) x. ((Q + 1)^2))))
72	58, 63	pm3.2i 285	. . . . 5 |- (((Q + 1)^2) e. CC /\ ((Q + 1)^2) =/= 0)
73	17, 59	pm3.2i 285	. . . . 5 |- ((!` Q) e. CC /\ (!` Q) =/= 0)
74		divcan5t 5781	. . . . 5 |- (((Q + 2) e. CC /\ (((Q + 1)^2) e. CC /\ ((Q + 1)^2) =/= 0) /\ ((!` Q) e. CC /\ (!` Q) =/= 0)) -> (((!` Q) x. (Q + 2)) / ((!` Q) x. ((Q + 1)^2))) = ((Q + 2) / ((Q + 1)^2)))
75	69, 72, 73, 74	mp3an 916	. . . 4 |- (((!` Q) x. (Q + 2)) / ((!` Q) x. ((Q + 1)^2))) = ((Q + 2) / ((Q + 1)^2))
76	71, 75	eqtr3 1497	. . 3 |- ((!` Q) x. ((Q + 2) / ((!` Q) x.