Theorem eirrlem 12758

Description: Lemma for eirr 12759. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)

Hypotheses

Ref	Expression
eirr.1	|- F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
eirr.2	|- ( ph -> P e. ZZ )
eirr.3	|- ( ph -> Q e. NN )
eirr.4	|- ( ph -> _e = ( P / Q ) )

Assertion

Ref	Expression
eirrlem	|- -. ph

Distinct variable group:   Q, n

Allowed substitution hints:   ph( n)   P( n)   F( n)

Proof of Theorem eirrlem

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		esum 12638	. . . . . . . . . 10 |- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )
2		fveq2 5687	. . . . . . . . . . . . 13 |- ( n = k -> ( ! ` n ) = ( ! ` k ) )
3	2	oveq2d 6056	. . . . . . . . . . . 12 |- ( n = k -> ( 1 / ( ! ` n ) ) = ( 1 / ( ! ` k ) ) )
4		eirr.1	. . . . . . . . . . . 12 |- F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
5		ovex 6065	. . . . . . . . . . . 12 |- ( 1 / ( ! ` k ) ) e. _V
6	3, 4, 5	fvmpt 5765	. . . . . . . . . . 11 |- ( k e. NN0 -> ( F ` k ) = ( 1 / ( ! ` k ) ) )
7	6	sumeq2i 12448	. . . . . . . . . 10 |- sum_ k e. NN0 ( F ` k ) = sum_ k e. NN0 ( 1 / ( ! ` k ) )
8	1, 7	eqtr4i 2427	. . . . . . . . 9 |- _e = sum_ k e. NN0 ( F ` k )
9		nn0uz 10476	. . . . . . . . . 10 |- NN0 = ( ZZ>= ` 0 )
10		eqid 2404	. . . . . . . . . 10 |- ( ZZ>= ` ( Q + 1 ) ) = ( ZZ>= ` ( Q + 1 ) )
11		eirr.3	. . . . . . . . . . . 12 |- ( ph -> Q e. NN )
12	11	peano2nnd 9973	. . . . . . . . . . 11 |- ( ph -> ( Q + 1 ) e. NN )
13	12	nnnn0d 10230	. . . . . . . . . 10 |- ( ph -> ( Q + 1 ) e. NN0 )
14		eqidd 2405	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( F ` k ) )
15		nn0z 10260	. . . . . . . . . . . . . . . . 17 |- ( n e. NN0 -> n e. ZZ )
16		1exp 11364	. . . . . . . . . . . . . . . . 17 |- ( n e. ZZ -> ( 1 ^ n ) = 1 )
17	15, 16	syl 16	. . . . . . . . . . . . . . . 16 |- ( n e. NN0 -> ( 1 ^ n ) = 1 )
18	17	oveq1d 6055	. . . . . . . . . . . . . . 15 |- ( n e. NN0 -> ( ( 1 ^ n ) / ( ! ` n ) ) = ( 1 / ( ! ` n ) ) )
19	18	mpteq2ia 4251	. . . . . . . . . . . . . 14 |- ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
20	4, 19	eqtr4i 2427	. . . . . . . . . . . . 13 |- F = ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) )
21	20	eftval 12634	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( F ` k ) = ( ( 1 ^ k ) / ( ! ` k ) ) )
22	21	adantl 453	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( 1 ^ k ) / ( ! ` k ) ) )
23		ax-1cn 9004	. . . . . . . . . . . . 13 |- 1 e. CC
24	23	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. CC )
25		eftcl 12631	. . . . . . . . . . . 12 |- ( ( 1 e. CC /\ k e. NN0 ) -> ( ( 1 ^ k ) / ( ! ` k ) ) e. CC )
26	24, 25	sylan 458	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( ( 1 ^ k ) / ( ! ` k ) ) e. CC )
27	22, 26	eqeltrd 2478	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
28	20	efcllem 12635	. . . . . . . . . . 11 |- ( 1 e. CC -> seq 0 ( + , F ) e. dom ~~> )
29	24, 28	syl 16	. . . . . . . . . 10 |- ( ph -> seq 0 ( + , F ) e. dom ~~> )
30	9, 10, 13, 14, 27, 29	isumsplit 12575	. . . . . . . . 9 |- ( ph -> sum_ k e. NN0 ( F ` k ) = ( sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
31	8, 30	syl5eq 2448	. . . . . . . 8 |- ( ph -> _e = ( sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
32	11	nncnd 9972	. . . . . . . . . . . 12 |- ( ph -> Q e. CC )
33		pncan 9267	. . . . . . . . . . . 12 |- ( ( Q e. CC /\ 1 e. CC ) -> ( ( Q + 1 ) - 1 ) = Q )
34	32, 23, 33	sylancl 644	. . . . . . . . . . 11 |- ( ph -> ( ( Q + 1 ) - 1 ) = Q )
35	34	oveq2d 6056	. . . . . . . . . 10 |- ( ph -> ( 0 ... ( ( Q + 1 ) - 1 ) ) = ( 0 ... Q ) )
36	35	sumeq1d 12450	. . . . . . . . 9 |- ( ph -> sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) = sum_ k e. ( 0 ... Q ) ( F ` k ) )
37	36	oveq1d 6055	. . . . . . . 8 |- ( ph -> ( sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = ( sum_ k e. ( 0 ... Q ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
38	31, 37	eqtrd 2436	. . . . . . 7 |- ( ph -> _e = ( sum_ k e. ( 0 ... Q ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
39	38	oveq1d 6055	. . . . . 6 |- ( ph -> ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) = ( ( sum_ k e. ( 0 ... Q ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) - sum_ k e. ( 0 ... Q ) ( F ` k ) ) )
40		fzfid 11267	. . . . . . . 8 |- ( ph -> ( 0 ... Q ) e. Fin )
41		elfznn0 11039	. . . . . . . . 9 |- ( k e. ( 0 ... Q ) -> k e. NN0 )
42	41, 27	sylan2 461	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( F ` k ) e. CC )
43	40, 42	fsumcl 12482	. . . . . . 7 |- ( ph -> sum_ k e. ( 0 ... Q ) ( F ` k ) e. CC )
44	6	adantl 453	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( 1 / ( ! ` k ) ) )
45		faccl 11531	. . . . . . . . . . . . . 14 |- ( k e. NN0 -> ( ! ` k ) e. NN )
46	45	adantl 453	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. NN )
47	46	nnrpd 10603	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. RR+ )
48	47	rpreccld 10614	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( ! ` k ) ) e. RR+ )
49	44, 48	eqeltrd 2478	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. RR+ )
50	9, 10, 13, 14, 49, 29	isumrpcl 12578	. . . . . . . . 9 |- ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR+ )
51	50	rpred 10604	. . . . . . . 8 |- ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR )
52	51	recnd 9070	. . . . . . 7 |- ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. CC )
53	43, 52	pncan2d 9369	. . . . . 6 |- ( ph -> ( ( sum_ k e. ( 0 ... Q ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) - sum_ k e. ( 0 ... Q ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
54	39, 53	eqtrd 2436	. . . . 5 |- ( ph -> ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
55	54	oveq2d 6056	. . . 4 |- ( ph -> ( ( ! ` Q ) x. ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) = ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
56	11	nnnn0d 10230	. . . . . . 7 |- ( ph -> Q e. NN0 )
57		faccl 11531	. . . . . . 7 |- ( Q e. NN0 -> ( ! ` Q ) e. NN )
58	56, 57	syl 16	. . . . . 6 |- ( ph -> ( ! ` Q ) e. NN )
59	58	nncnd 9972	. . . . 5 |- ( ph -> ( ! ` Q ) e. CC )
60		ere 12646	. . . . . . 7 |- _e e. RR
61	60	recni 9058	. . . . . 6 |- _e e. CC
62	61	a1i 11	. . . . 5 |- ( ph -> _e e. CC )
63	59, 62, 43	subdid 9445	. . . 4 |- ( ph -> ( ( ! ` Q ) x. ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) = ( ( ( ! ` Q ) x. _e ) - ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) )
64	55, 63	eqtr3d 2438	. . 3 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = ( ( ( ! ` Q ) x. _e ) - ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) )
65		eirr.4	. . . . . . 7 |- ( ph -> _e = ( P / Q ) )
66	65	oveq2d 6056	. . . . . 6 |- ( ph -> ( ( ! ` Q ) x. _e ) = ( ( ! ` Q ) x. ( P / Q ) ) )
67		eirr.2	. . . . . . . 8 |- ( ph -> P e. ZZ )
68	67	zcnd 10332	. . . . . . 7 |- ( ph -> P e. CC )
69	11	nnne0d 10000	. . . . . . 7 |- ( ph -> Q =/= 0 )
70	59, 68, 32, 69	div12d 9782	. . . . . 6 |- ( ph -> ( ( ! ` Q ) x. ( P / Q ) ) = ( P x. ( ( ! ` Q ) / Q ) ) )
71	66, 70	eqtrd 2436	. . . . 5 |- ( ph -> ( ( ! ` Q ) x. _e ) = ( P x. ( ( ! ` Q ) / Q ) ) )
72	11	nnred 9971	. . . . . . . . 9 |- ( ph -> Q e. RR )
73	72	leidd 9549	. . . . . . . 8 |- ( ph -> Q <_ Q )
74		facdiv 11533	. . . . . . . 8 |- ( ( Q e. NN0 /\ Q e. NN /\ Q <_ Q ) -> ( ( ! ` Q ) / Q ) e. NN )
75	56, 11, 73, 74	syl3anc 1184	. . . . . . 7 |- ( ph -> ( ( ! ` Q ) / Q ) e. NN )
76	75	nnzd 10330	. . . . . 6 |- ( ph -> ( ( ! ` Q ) / Q ) e. ZZ )
77	67, 76	zmulcld 10337	. . . . 5 |- ( ph -> ( P x. ( ( ! ` Q ) / Q ) ) e. ZZ )
78	71, 77	eqeltrd 2478	. . . 4 |- ( ph -> ( ( ! ` Q ) x. _e ) e. ZZ )
79	40, 59, 42	fsummulc2 12522	. . . . 5 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) = sum_ k e. ( 0 ... Q ) ( ( ! ` Q ) x. ( F ` k ) ) )
80	41	adantl 453	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> k e. NN0 )
81	80, 6	syl 16	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( F ` k ) = ( 1 / ( ! ` k ) ) )
82	81	oveq2d 6056	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) = ( ( ! ` Q ) x. ( 1 / ( ! ` k ) ) ) )
83	59	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` Q ) e. CC )
84	41, 46	sylan2 461	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` k ) e. NN )
85	84	nncnd 9972	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` k ) e. CC )
86		facne0 11532	. . . . . . . . . . 11 |- ( k e. NN0 -> ( ! ` k ) =/= 0 )
87	80, 86	syl 16	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` k ) =/= 0 )
88	83, 85, 87	divrecd 9749	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) / ( ! ` k ) ) = ( ( ! ` Q ) x. ( 1 / ( ! ` k ) ) ) )
89	82, 88	eqtr4d 2439	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) = ( ( ! ` Q ) / ( ! ` k ) ) )
90		permnn 11572	. . . . . . . . 9 |- ( k e. ( 0 ... Q ) -> ( ( ! ` Q ) / ( ! ` k ) ) e. NN )
91	90	adantl 453	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) / ( ! ` k ) ) e. NN )
92	89, 91	eqeltrd 2478	. . . . . . 7 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) e. NN )
93	92	nnzd 10330	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) e. ZZ )
94	40, 93	fsumzcl 12484	. . . . 5 |- ( ph -> sum_ k e. ( 0 ... Q ) ( ( ! ` Q ) x. ( F ` k ) ) e. ZZ )
95	79, 94	eqeltrd 2478	. . . 4 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) e. ZZ )
96	78, 95	zsubcld 10336	. . 3 |- ( ph -> ( ( ( ! ` Q ) x. _e ) - ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) e. ZZ )
97	64, 96	eqeltrd 2478	. 2 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. ZZ )
98		0z 10249	. . . 4 |- 0 e. ZZ
99	98	a1i 11	. . 3 |- ( ph -> 0 e. ZZ )
100	58	nnrpd 10603	. . . . 5 |- ( ph -> ( ! ` Q ) e. RR+ )
101	100, 50	rpmulcld 10620	. . . 4 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. RR+ )
102	101	rpgt0d 10607	. . 3 |- ( ph -> 0 < ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
103	12	peano2nnd 9973	. . . . . . . 8 |- ( ph -> ( ( Q + 1 ) + 1 ) e. NN )
104	103	nnred 9971	. . . . . . 7 |- ( ph -> ( ( Q + 1 ) + 1 ) e. RR )
105		faccl 11531	. . . . . . . . 9 |- ( ( Q + 1 ) e. NN0 -> ( ! ` ( Q + 1 ) ) e. NN )
106	13, 105	syl 16	. . . . . . . 8 |- ( ph -> ( ! ` ( Q + 1 ) ) e. NN )
107	106, 12	nnmulcld 10003	. . . . . . 7 |- ( ph -> ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) e. NN )
108	104, 107	nndivred 10004	. . . . . 6 |- ( ph -> ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) e. RR )
109	58	nnrecred 10001	. . . . . 6 |- ( ph -> ( 1 / ( ! ` Q ) ) e. RR )
110		abs1 12057	. . . . . . . . . . . 12 |- ( abs ` 1 ) = 1
111	110	oveq1i 6050	. . . . . . . . . . 11 |- ( ( abs ` 1 ) ^ n ) = ( 1 ^ n )
112	111	oveq1i 6050	. . . . . . . . . 10 |- ( ( ( abs ` 1 ) ^ n ) / ( ! ` n ) ) = ( ( 1 ^ n ) / ( ! ` n ) )
113	112	mpteq2i 4252	. . . . . . . . 9 |- ( n e. NN0 |-> ( ( ( abs ` 1 ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) )
114	20, 113	eqtr4i 2427	. . . . . . . 8 |- F = ( n e. NN0 |-> ( ( ( abs ` 1 ) ^ n ) / ( ! ` n ) ) )
115		eqid 2404	. . . . . . . 8 |- ( n e. NN0 |-> ( ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) / ( ! ` ( Q + 1 ) ) ) x. ( ( 1 / ( ( Q + 1 ) + 1 ) ) ^ n ) ) ) = ( n e. NN0 |-> ( ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) / ( ! ` ( Q + 1 ) ) ) x. ( ( 1 / ( ( Q + 1 ) + 1 ) ) ^ n ) ) )
116		1le1 9606	. . . . . . . . . 10 |- 1 <_ 1
117	110, 116	eqbrtri 4191	. . . . . . . . 9 |- ( abs ` 1 ) <_ 1
118	117	a1i 11	. . . . . . . 8 |- ( ph -> ( abs ` 1 ) <_ 1 )
119	20, 114, 115, 12, 24, 118	eftlub 12665	. . . . . . 7 |- ( ph -> ( abs ` sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) <_ ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) )
120	50	rprege0d 10611	. . . . . . . 8 |- ( ph -> ( sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR /\ 0 <_ sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
121		absid 12056	. . . . . . . 8 |- ( ( sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR /\ 0 <_ sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
122	120, 121	syl 16	. . . . . . 7 |- ( ph -> ( abs ` sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
123	110	oveq1i 6050	. . . . . . . . . 10 |- ( ( abs ` 1 ) ^ ( Q + 1 ) ) = ( 1 ^ ( Q + 1 ) )
124	12	nnzd 10330	. . . . . . . . . . 11 |- ( ph -> ( Q + 1 ) e. ZZ )
125		1exp 11364	. . . . . . . . . . 11 |- ( ( Q + 1 ) e. ZZ -> ( 1 ^ ( Q + 1 ) ) = 1 )
126	124, 125	syl 16	. . . . . . . . . 10 |- ( ph -> ( 1 ^ ( Q + 1 ) ) = 1 )
127	123, 126	syl5eq 2448	. . . . . . . . 9 |- ( ph -> ( ( abs ` 1 ) ^ ( Q + 1 ) ) = 1 )
128	127	oveq1d 6055	. . . . . . . 8 |- ( ph -> ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) = ( 1 x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) )
129	108	recnd 9070	. . . . . . . . 9 |- ( ph -> ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) e. CC )
130	129	mulid2d 9062	. . . . . . . 8 |- ( ph -> ( 1 x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) = ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) )
131	128, 130	eqtrd 2436	. . . . . . 7 |- ( ph -> ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) = ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) )
132	119, 122, 131	3brtr3d 4201	. . . . . 6 |- ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) <_ ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) )
133	12	nnred 9971	. . . . . . . . . 10 |- ( ph -> ( Q + 1 ) e. RR )
134	133, 133	readdcld 9071	. . . . . . . . 9 |- ( ph -> ( ( Q + 1 ) + ( Q + 1 ) ) e. RR )
135	133, 133	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( ( Q + 1 ) x. ( Q + 1 ) ) e. RR )
136		1re 9046	. . . . . . . . . . 11 |- 1 e. RR
137	136	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. RR )
138	11	nnge1d 9998	. . . . . . . . . . 11 |- ( ph -> 1 <_ Q )
139		1nn 9967	. . . . . . . . . . . 12 |- 1 e. NN
140		nnleltp1 10285	. . . . . . . . . . . 12 |- ( ( 1 e. NN /\ Q e. NN ) -> ( 1 <_ Q <-> 1 < ( Q + 1 ) ) )
141	139, 11, 140	sylancr 645	. . . . . . . . . . 11 |- ( ph -> ( 1 <_ Q <-> 1 < ( Q + 1 ) ) )
142	138, 141	mpbid 202	. . . . . . . . . 10 |- ( ph -> 1 < ( Q + 1 ) )
143	137, 133, 133, 142	ltadd2dd 9185	. . . . . . . . 9 |- ( ph -> ( ( Q + 1 ) + 1 ) < ( ( Q + 1 ) + ( Q + 1 ) ) )
144	12	nncnd 9972	. . . . . . . . . . 11 |- ( ph -> ( Q + 1 ) e. CC )
145	144	2timesd 10166	. . . . . . . . . 10 |- ( ph -> ( 2 x. ( Q + 1 ) ) = ( ( Q + 1 ) + ( Q + 1 ) ) )
146		df-2 10014	. . . . . . . . . . . 12 |- 2 = ( 1 + 1 )
147	137, 72, 137, 138	leadd1dd 9596	. . . . . . . . . . . 12 |- ( ph -> ( 1 + 1 ) <_ ( Q + 1 ) )
148	146, 147	syl5eqbr 4205	. . . . . . . . . . 11 |- ( ph -> 2 <_ ( Q + 1 ) )
149		2re 10025	. . . . . . . . . . . . 13 |- 2 e. RR
150	149	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 2 e. RR )
151	12	nngt0d 9999	. . . . . . . . . . . 12 |- ( ph -> 0 < ( Q + 1 ) )
152		lemul1 9818	. . . . . . . . . . . 12 |- ( ( 2 e. RR /\ ( Q + 1 ) e. RR /\ ( ( Q + 1 ) e. RR /\ 0 < ( Q + 1 ) ) ) -> ( 2 <_ ( Q + 1 ) <-> ( 2 x. ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) ) )
153	150, 133, 133, 151, 152	syl112anc 1188	. . . . . . . . . . 11 |- ( ph -> ( 2 <_ ( Q + 1 ) <-> ( 2 x. ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) ) )
154	148, 153	mpbid 202	. . . . . . . . . 10 |- ( ph -> ( 2 x. ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) )
155	145, 154	eqbrtrrd 4194	. . . . . . . . 9 |- ( ph -> ( ( Q + 1 ) + ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) )
156	104, 134, 135, 143, 155	ltletrd 9186	. . . . . . . 8 |- ( ph -> ( ( Q + 1 ) + 1 ) < ( ( Q + 1 ) x. ( Q + 1 ) ) )
157		facp1 11526	. . . . . . . . . . . . 13 |- ( Q e. NN0 -> ( ! ` ( Q + 1 ) ) = ( ( ! ` Q ) x. ( Q + 1 ) ) )
158	56, 157	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( ! ` ( Q + 1 ) ) = ( ( ! ` Q ) x. ( Q + 1 ) ) )
159	158	oveq1d 6055	. . . . . . . . . . 11 |- ( ph -> ( ( ! ` ( Q + 1 ) ) / ( ! ` Q ) ) = ( ( ( ! ` Q ) x. ( Q + 1 ) ) / ( ! ` Q ) ) )
160	106	nncnd 9972	. . . . . . . . . . . 12 |- ( ph -> ( ! ` ( Q + 1 ) ) e. CC )
161	58	nnne0d 10000	. . . . . . . . . . . 12 |- ( ph -> ( ! ` Q ) =/= 0 )
162	160, 59, 161	divrecd 9749	. . . . . . . . . . 11 |- ( ph -> ( ( ! ` ( Q + 1 ) ) / ( ! ` Q ) ) = ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
163	144, 59, 161	divcan3d 9751	. . . . . . . . . . 11 |- ( ph -> ( ( ( ! ` Q ) x. ( Q + 1 ) ) / ( ! ` Q ) ) = ( Q + 1 ) )
164	159, 162, 163	3eqtr3rd 2445	. . . . . . . . . 10 |- ( ph -> ( Q + 1 ) = ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
165	164	oveq1d 6055	. . . . . . . . 9 |- ( ph -> ( ( Q + 1 ) x. ( Q + 1 ) ) = ( ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) x. ( Q + 1 ) ) )
166	109	recnd 9070	. . . . . . . . . 10 |- ( ph -> ( 1 / ( ! ` Q ) ) e. CC )
167	160, 166, 144	mul32d 9232	. . . . . . . . 9 |- ( ph -> ( ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) x. ( Q + 1 ) ) = ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
168	165, 167	eqtrd 2436	. . . . . . . 8 |- ( ph -> ( ( Q + 1 ) x. ( Q + 1 ) ) = ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
169	156, 168	breqtrd 4196	. . . . . . 7 |- ( ph -> ( ( Q + 1 ) + 1 ) < ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
170	107	nnred 9971	. . . . . . . 8 |- ( ph -> ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) e. RR )
171	107	nngt0d 9999	. . . . . . . 8 |- ( ph -> 0 < ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) )
172		ltdivmul 9838	. . . . . . . 8 |- ( ( ( ( Q + 1 ) + 1 ) e. RR /\ ( 1 / ( ! ` Q ) ) e. RR /\ ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) e. RR /\ 0 < ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) -> ( ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) < ( 1 / ( ! ` Q ) ) <-> ( ( Q + 1 ) + 1 ) < ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) ) )
173	104, 109, 170, 171, 172	syl112anc 1188	. . . . . . 7 |- ( ph -> ( ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) < ( 1 / ( ! ` Q ) ) <-> ( ( Q + 1 ) + 1 ) < ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) ) )
174	169, 173	mpbird 224	. . . . . 6 |- ( ph -> ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) < ( 1 / ( ! ` Q ) ) )
175	51, 108, 109, 132, 174	lelttrd 9184	. . . . 5 |- ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) < ( 1 / ( ! ` Q ) ) )
176	51, 137, 100	ltmuldiv2d 10648	. . . . 5 |- ( ph -> ( ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < 1 <-> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) < ( 1 / ( ! ` Q ) ) ) )
177	175, 176	mpbird 224	. . . 4 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < 1 )
178		0p1e1 10049	. . . 4 |- ( 0 + 1 ) = 1
179	177, 178	syl6breqr 4212	. . 3 |- ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < ( 0 + 1 ) )
180		btwnnz 10302	. . 3 |- ( ( 0 e. ZZ /\ 0 < ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) /\ ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < ( 0 + 1 ) ) -> -. ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. ZZ )
181	99, 102, 179, 180	syl3anc 1184	. 2 |- ( ph -> -. ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. ZZ )
182	97, 181	pm2.65i 167	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   =/= wne 2567   class class class wbr 4172   e. cmpt 4226   dom cdm 4837   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   ...cfz 10999   seq cseq 11278   ^cexp 11337   !cfa 11521   abscabs 11994   ~~> cli 12233   sum_csu 12434   _eceu 12620

This theorem is referenced by:  eirr  12759

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-ico 10878  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-shft 11837  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-ef 12625  df-e 12626