Step |
Hyp |
Ref |
Expression |
1 |
|
pntlem1.r |
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) ) |
2 |
|
pntlem1.a |
|- ( ph -> A e. RR+ ) |
3 |
|
pntlem1.b |
|- ( ph -> B e. RR+ ) |
4 |
|
pntlem1.l |
|- ( ph -> L e. ( 0 (,) 1 ) ) |
5 |
|
pntlem1.d |
|- D = ( A + 1 ) |
6 |
|
pntlem1.f |
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) |
7 |
|
pntlem1.u |
|- ( ph -> U e. RR+ ) |
8 |
|
pntlem1.u2 |
|- ( ph -> U <_ A ) |
9 |
|
pntlem1.e |
|- E = ( U / D ) |
10 |
|
pntlem1.k |
|- K = ( exp ` ( B / E ) ) |
11 |
|
pntlem1.y |
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) ) |
12 |
|
pntlem1.x |
|- ( ph -> ( X e. RR+ /\ Y < X ) ) |
13 |
|
pntlem1.c |
|- ( ph -> C e. RR+ ) |
14 |
|
pntlem1.w |
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) ) |
15 |
|
pntlem1.z |
|- ( ph -> Z e. ( W [,) +oo ) ) |
16 |
|
pntlem1.m |
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) |
17 |
|
pntlem1.n |
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) |
18 |
|
pntlem1.U |
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U ) |
19 |
|
pntlem1.K |
|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) |
20 |
|
pntlem1.o |
|- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) |
21 |
|
pntlem1.v |
|- ( ph -> V e. RR+ ) |
22 |
|
pntlem1.V |
|- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) |
23 |
|
pntlem1.j |
|- ( ph -> J e. ( M ..^ N ) ) |
24 |
|
pntlem1.i |
|- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) |
25 |
1 2 3 4 5 6 7 8 9 10
|
pntlemc |
|- ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) ) |
26 |
25
|
simp3d |
|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) |
27 |
26
|
simp3d |
|- ( ph -> ( U - E ) e. RR+ ) |
28 |
1 2 3 4 5 6
|
pntlemd |
|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) ) |
29 |
28
|
simp1d |
|- ( ph -> L e. RR+ ) |
30 |
25
|
simp1d |
|- ( ph -> E e. RR+ ) |
31 |
29 30
|
rpmulcld |
|- ( ph -> ( L x. E ) e. RR+ ) |
32 |
|
8nn |
|- 8 e. NN |
33 |
|
nnrp |
|- ( 8 e. NN -> 8 e. RR+ ) |
34 |
32 33
|
ax-mp |
|- 8 e. RR+ |
35 |
|
rpdivcl |
|- ( ( ( L x. E ) e. RR+ /\ 8 e. RR+ ) -> ( ( L x. E ) / 8 ) e. RR+ ) |
36 |
31 34 35
|
sylancl |
|- ( ph -> ( ( L x. E ) / 8 ) e. RR+ ) |
37 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
pntlemb |
|- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) ) |
38 |
37
|
simp1d |
|- ( ph -> Z e. RR+ ) |
39 |
38
|
rpred |
|- ( ph -> Z e. RR ) |
40 |
37
|
simp2d |
|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) ) |
41 |
40
|
simp1d |
|- ( ph -> 1 < Z ) |
42 |
39 41
|
rplogcld |
|- ( ph -> ( log ` Z ) e. RR+ ) |
43 |
36 42
|
rpmulcld |
|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR+ ) |
44 |
27 43
|
rpmulcld |
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR+ ) |
45 |
44
|
rpred |
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR ) |
46 |
|
fzfid |
|- ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) e. Fin ) |
47 |
24 46
|
eqeltrid |
|- ( ph -> I e. Fin ) |
48 |
|
hashcl |
|- ( I e. Fin -> ( # ` I ) e. NN0 ) |
49 |
47 48
|
syl |
|- ( ph -> ( # ` I ) e. NN0 ) |
50 |
49
|
nn0red |
|- ( ph -> ( # ` I ) e. RR ) |
51 |
27
|
rpred |
|- ( ph -> ( U - E ) e. RR ) |
52 |
38 21
|
rpdivcld |
|- ( ph -> ( Z / V ) e. RR+ ) |
53 |
52
|
relogcld |
|- ( ph -> ( log ` ( Z / V ) ) e. RR ) |
54 |
53 52
|
rerpdivcld |
|- ( ph -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR ) |
55 |
51 54
|
remulcld |
|- ( ph -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR ) |
56 |
50 55
|
remulcld |
|- ( ph -> ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) e. RR ) |
57 |
|
fzfid |
|- ( ph -> ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) e. Fin ) |
58 |
20 57
|
eqeltrid |
|- ( ph -> O e. Fin ) |
59 |
7
|
rpred |
|- ( ph -> U e. RR ) |
60 |
59
|
adantr |
|- ( ( ph /\ n e. O ) -> U e. RR ) |
61 |
25
|
simp2d |
|- ( ph -> K e. RR+ ) |
62 |
|
elfzoelz |
|- ( J e. ( M ..^ N ) -> J e. ZZ ) |
63 |
23 62
|
syl |
|- ( ph -> J e. ZZ ) |
64 |
63
|
peano2zd |
|- ( ph -> ( J + 1 ) e. ZZ ) |
65 |
61 64
|
rpexpcld |
|- ( ph -> ( K ^ ( J + 1 ) ) e. RR+ ) |
66 |
38 65
|
rpdivcld |
|- ( ph -> ( Z / ( K ^ ( J + 1 ) ) ) e. RR+ ) |
67 |
66
|
rprege0d |
|- ( ph -> ( ( Z / ( K ^ ( J + 1 ) ) ) e. RR /\ 0 <_ ( Z / ( K ^ ( J + 1 ) ) ) ) ) |
68 |
|
flge0nn0 |
|- ( ( ( Z / ( K ^ ( J + 1 ) ) ) e. RR /\ 0 <_ ( Z / ( K ^ ( J + 1 ) ) ) ) -> ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) e. NN0 ) |
69 |
|
nn0p1nn |
|- ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) e. NN ) |
70 |
67 68 69
|
3syl |
|- ( ph -> ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) e. NN ) |
71 |
|
elfzuz |
|- ( n e. ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) ) |
72 |
71 20
|
eleq2s |
|- ( n e. O -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) ) |
73 |
|
eluznn |
|- ( ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) ) -> n e. NN ) |
74 |
70 72 73
|
syl2an |
|- ( ( ph /\ n e. O ) -> n e. NN ) |
75 |
60 74
|
nndivred |
|- ( ( ph /\ n e. O ) -> ( U / n ) e. RR ) |
76 |
38
|
adantr |
|- ( ( ph /\ n e. O ) -> Z e. RR+ ) |
77 |
74
|
nnrpd |
|- ( ( ph /\ n e. O ) -> n e. RR+ ) |
78 |
76 77
|
rpdivcld |
|- ( ( ph /\ n e. O ) -> ( Z / n ) e. RR+ ) |
79 |
1
|
pntrf |
|- R : RR+ --> RR |
80 |
79
|
ffvelrni |
|- ( ( Z / n ) e. RR+ -> ( R ` ( Z / n ) ) e. RR ) |
81 |
78 80
|
syl |
|- ( ( ph /\ n e. O ) -> ( R ` ( Z / n ) ) e. RR ) |
82 |
81 76
|
rerpdivcld |
|- ( ( ph /\ n e. O ) -> ( ( R ` ( Z / n ) ) / Z ) e. RR ) |
83 |
82
|
recnd |
|- ( ( ph /\ n e. O ) -> ( ( R ` ( Z / n ) ) / Z ) e. CC ) |
84 |
83
|
abscld |
|- ( ( ph /\ n e. O ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. RR ) |
85 |
75 84
|
resubcld |
|- ( ( ph /\ n e. O ) -> ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) e. RR ) |
86 |
77
|
relogcld |
|- ( ( ph /\ n e. O ) -> ( log ` n ) e. RR ) |
87 |
85 86
|
remulcld |
|- ( ( ph /\ n e. O ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR ) |
88 |
58 87
|
fsumrecl |
|- ( ph -> sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR ) |
89 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
|
pntlemr |
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) |
90 |
55
|
recnd |
|- ( ph -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC ) |
91 |
|
fsumconst |
|- ( ( I e. Fin /\ ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC ) -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) |
92 |
47 90 91
|
syl2anc |
|- ( ph -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) |
93 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
|
pntlemq |
|- ( ph -> I C_ O ) |
94 |
90
|
ralrimivw |
|- ( ph -> A. n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC ) |
95 |
58
|
olcd |
|- ( ph -> ( O C_ ( ZZ>= ` 1 ) \/ O e. Fin ) ) |
96 |
|
sumss2 |
|- ( ( ( I C_ O /\ A. n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC ) /\ ( O C_ ( ZZ>= ` 1 ) \/ O e. Fin ) ) -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) ) |
97 |
93 94 95 96
|
syl21anc |
|- ( ph -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) ) |
98 |
92 97
|
eqtr3d |
|- ( ph -> ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) = sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) ) |
99 |
55
|
adantr |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR ) |
100 |
99
|
adantlr |
|- ( ( ( ph /\ n e. O ) /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR ) |
101 |
|
0red |
|- ( ( ( ph /\ n e. O ) /\ -. n e. I ) -> 0 e. RR ) |
102 |
100 101
|
ifclda |
|- ( ( ph /\ n e. O ) -> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) e. RR ) |
103 |
|
breq1 |
|- ( ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) -> ( ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) |
104 |
|
breq1 |
|- ( 0 = if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) -> ( 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) |
105 |
27
|
rpregt0d |
|- ( ph -> ( ( U - E ) e. RR /\ 0 < ( U - E ) ) ) |
106 |
105
|
adantr |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) e. RR /\ 0 < ( U - E ) ) ) |
107 |
106
|
simpld |
|- ( ( ph /\ n e. I ) -> ( U - E ) e. RR ) |
108 |
|
1rp |
|- 1 e. RR+ |
109 |
|
rpaddcl |
|- ( ( 1 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 1 + ( L x. E ) ) e. RR+ ) |
110 |
108 31 109
|
sylancr |
|- ( ph -> ( 1 + ( L x. E ) ) e. RR+ ) |
111 |
110 21
|
rpmulcld |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR+ ) |
112 |
38 111
|
rpdivcld |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR+ ) |
113 |
112
|
rprege0d |
|- ( ph -> ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ 0 <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
114 |
|
flge0nn0 |
|- ( ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ 0 <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. NN0 ) |
115 |
|
nn0p1nn |
|- ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. NN ) |
116 |
113 114 115
|
3syl |
|- ( ph -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. NN ) |
117 |
|
elfzuz |
|- ( n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) |
118 |
117 24
|
eleq2s |
|- ( n e. I -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) |
119 |
|
eluznn |
|- ( ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) -> n e. NN ) |
120 |
116 118 119
|
syl2an |
|- ( ( ph /\ n e. I ) -> n e. NN ) |
121 |
120
|
nnrpd |
|- ( ( ph /\ n e. I ) -> n e. RR+ ) |
122 |
121
|
relogcld |
|- ( ( ph /\ n e. I ) -> ( log ` n ) e. RR ) |
123 |
122 120
|
nndivred |
|- ( ( ph /\ n e. I ) -> ( ( log ` n ) / n ) e. RR ) |
124 |
107 123
|
remulcld |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` n ) / n ) ) e. RR ) |
125 |
93
|
sselda |
|- ( ( ph /\ n e. I ) -> n e. O ) |
126 |
125 87
|
syldan |
|- ( ( ph /\ n e. I ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR ) |
127 |
|
simpr |
|- ( ( ph /\ n e. I ) -> n e. I ) |
128 |
127 24
|
eleqtrdi |
|- ( ( ph /\ n e. I ) -> n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) ) |
129 |
|
elfzle2 |
|- ( n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) -> n <_ ( |_ ` ( Z / V ) ) ) |
130 |
128 129
|
syl |
|- ( ( ph /\ n e. I ) -> n <_ ( |_ ` ( Z / V ) ) ) |
131 |
52
|
rpred |
|- ( ph -> ( Z / V ) e. RR ) |
132 |
131
|
adantr |
|- ( ( ph /\ n e. I ) -> ( Z / V ) e. RR ) |
133 |
128
|
elfzelzd |
|- ( ( ph /\ n e. I ) -> n e. ZZ ) |
134 |
|
flge |
|- ( ( ( Z / V ) e. RR /\ n e. ZZ ) -> ( n <_ ( Z / V ) <-> n <_ ( |_ ` ( Z / V ) ) ) ) |
135 |
132 133 134
|
syl2anc |
|- ( ( ph /\ n e. I ) -> ( n <_ ( Z / V ) <-> n <_ ( |_ ` ( Z / V ) ) ) ) |
136 |
130 135
|
mpbird |
|- ( ( ph /\ n e. I ) -> n <_ ( Z / V ) ) |
137 |
120
|
nnred |
|- ( ( ph /\ n e. I ) -> n e. RR ) |
138 |
|
ere |
|- _e e. RR |
139 |
138
|
a1i |
|- ( ( ph /\ n e. I ) -> _e e. RR ) |
140 |
112
|
rpred |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR ) |
141 |
140
|
adantr |
|- ( ( ph /\ n e. I ) -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR ) |
142 |
138
|
a1i |
|- ( ph -> _e e. RR ) |
143 |
38
|
rpsqrtcld |
|- ( ph -> ( sqrt ` Z ) e. RR+ ) |
144 |
143
|
rpred |
|- ( ph -> ( sqrt ` Z ) e. RR ) |
145 |
40
|
simp2d |
|- ( ph -> _e <_ ( sqrt ` Z ) ) |
146 |
111
|
rpred |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR ) |
147 |
65
|
rpred |
|- ( ph -> ( K ^ ( J + 1 ) ) e. RR ) |
148 |
22
|
simpld |
|- ( ph -> ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) ) |
149 |
148
|
simprd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) |
150 |
61
|
rpcnd |
|- ( ph -> K e. CC ) |
151 |
61 63
|
rpexpcld |
|- ( ph -> ( K ^ J ) e. RR+ ) |
152 |
151
|
rpcnd |
|- ( ph -> ( K ^ J ) e. CC ) |
153 |
150 152
|
mulcomd |
|- ( ph -> ( K x. ( K ^ J ) ) = ( ( K ^ J ) x. K ) ) |
154 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pntlemg |
|- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) ) |
155 |
154
|
simp1d |
|- ( ph -> M e. NN ) |
156 |
|
elfzouz |
|- ( J e. ( M ..^ N ) -> J e. ( ZZ>= ` M ) ) |
157 |
23 156
|
syl |
|- ( ph -> J e. ( ZZ>= ` M ) ) |
158 |
|
eluznn |
|- ( ( M e. NN /\ J e. ( ZZ>= ` M ) ) -> J e. NN ) |
159 |
155 157 158
|
syl2anc |
|- ( ph -> J e. NN ) |
160 |
159
|
nnnn0d |
|- ( ph -> J e. NN0 ) |
161 |
150 160
|
expp1d |
|- ( ph -> ( K ^ ( J + 1 ) ) = ( ( K ^ J ) x. K ) ) |
162 |
153 161
|
eqtr4d |
|- ( ph -> ( K x. ( K ^ J ) ) = ( K ^ ( J + 1 ) ) ) |
163 |
149 162
|
breqtrd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K ^ ( J + 1 ) ) ) |
164 |
146 147 163
|
ltled |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( K ^ ( J + 1 ) ) ) |
165 |
|
fzofzp1 |
|- ( J e. ( M ..^ N ) -> ( J + 1 ) e. ( M ... N ) ) |
166 |
23 165
|
syl |
|- ( ph -> ( J + 1 ) e. ( M ... N ) ) |
167 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pntlemh |
|- ( ( ph /\ ( J + 1 ) e. ( M ... N ) ) -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) ) |
168 |
166 167
|
mpdan |
|- ( ph -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) ) |
169 |
168
|
simprd |
|- ( ph -> ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) |
170 |
146 147 144 164 169
|
letrd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) ) |
171 |
146 144 143
|
lemul2d |
|- ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) <-> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) ) |
172 |
170 171
|
mpbid |
|- ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) |
173 |
38
|
rprege0d |
|- ( ph -> ( Z e. RR /\ 0 <_ Z ) ) |
174 |
|
remsqsqrt |
|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z ) |
175 |
173 174
|
syl |
|- ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z ) |
176 |
172 175
|
breqtrd |
|- ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z ) |
177 |
144 39 111
|
lemuldivd |
|- ( ph -> ( ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z <-> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
178 |
176 177
|
mpbid |
|- ( ph -> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) |
179 |
142 144 140 145 178
|
letrd |
|- ( ph -> _e <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) |
180 |
179
|
adantr |
|- ( ( ph /\ n e. I ) -> _e <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) |
181 |
|
reflcl |
|- ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR ) |
182 |
|
peano2re |
|- ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. RR ) |
183 |
140 181 182
|
3syl |
|- ( ph -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. RR ) |
184 |
183
|
adantr |
|- ( ( ph /\ n e. I ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. RR ) |
185 |
|
fllep1 |
|- ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) |
186 |
141 185
|
syl |
|- ( ( ph /\ n e. I ) -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) |
187 |
|
elfzle1 |
|- ( n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) <_ n ) |
188 |
128 187
|
syl |
|- ( ( ph /\ n e. I ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) <_ n ) |
189 |
141 184 137 186 188
|
letrd |
|- ( ( ph /\ n e. I ) -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ n ) |
190 |
139 141 137 180 189
|
letrd |
|- ( ( ph /\ n e. I ) -> _e <_ n ) |
191 |
139 137 132 190 136
|
letrd |
|- ( ( ph /\ n e. I ) -> _e <_ ( Z / V ) ) |
192 |
|
logdivle |
|- ( ( ( n e. RR /\ _e <_ n ) /\ ( ( Z / V ) e. RR /\ _e <_ ( Z / V ) ) ) -> ( n <_ ( Z / V ) <-> ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) ) ) |
193 |
137 190 132 191 192
|
syl22anc |
|- ( ( ph /\ n e. I ) -> ( n <_ ( Z / V ) <-> ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) ) ) |
194 |
136 193
|
mpbid |
|- ( ( ph /\ n e. I ) -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) ) |
195 |
54
|
adantr |
|- ( ( ph /\ n e. I ) -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR ) |
196 |
|
lemul2 |
|- ( ( ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR /\ ( ( log ` n ) / n ) e. RR /\ ( ( U - E ) e. RR /\ 0 < ( U - E ) ) ) -> ( ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) <-> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( U - E ) x. ( ( log ` n ) / n ) ) ) ) |
197 |
195 123 106 196
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) <-> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( U - E ) x. ( ( log ` n ) / n ) ) ) ) |
198 |
194 197
|
mpbid |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( U - E ) x. ( ( log ` n ) / n ) ) ) |
199 |
27
|
rpcnd |
|- ( ph -> ( U - E ) e. CC ) |
200 |
199
|
adantr |
|- ( ( ph /\ n e. I ) -> ( U - E ) e. CC ) |
201 |
122
|
recnd |
|- ( ( ph /\ n e. I ) -> ( log ` n ) e. CC ) |
202 |
121
|
rpcnne0d |
|- ( ( ph /\ n e. I ) -> ( n e. CC /\ n =/= 0 ) ) |
203 |
|
div23 |
|- ( ( ( U - E ) e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( ( U - E ) / n ) x. ( log ` n ) ) ) |
204 |
200 201 202 203
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( ( U - E ) / n ) x. ( log ` n ) ) ) |
205 |
|
divass |
|- ( ( ( U - E ) e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( U - E ) x. ( ( log ` n ) / n ) ) ) |
206 |
200 201 202 205
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( U - E ) x. ( ( log ` n ) / n ) ) ) |
207 |
204 206
|
eqtr3d |
|- ( ( ph /\ n e. I ) -> ( ( ( U - E ) / n ) x. ( log ` n ) ) = ( ( U - E ) x. ( ( log ` n ) / n ) ) ) |
208 |
51
|
adantr |
|- ( ( ph /\ n e. I ) -> ( U - E ) e. RR ) |
209 |
208 120
|
nndivred |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) / n ) e. RR ) |
210 |
125 85
|
syldan |
|- ( ( ph /\ n e. I ) -> ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) e. RR ) |
211 |
|
log1 |
|- ( log ` 1 ) = 0 |
212 |
120
|
nnge1d |
|- ( ( ph /\ n e. I ) -> 1 <_ n ) |
213 |
|
logleb |
|- ( ( 1 e. RR+ /\ n e. RR+ ) -> ( 1 <_ n <-> ( log ` 1 ) <_ ( log ` n ) ) ) |
214 |
108 121 213
|
sylancr |
|- ( ( ph /\ n e. I ) -> ( 1 <_ n <-> ( log ` 1 ) <_ ( log ` n ) ) ) |
215 |
212 214
|
mpbid |
|- ( ( ph /\ n e. I ) -> ( log ` 1 ) <_ ( log ` n ) ) |
216 |
211 215
|
eqbrtrrid |
|- ( ( ph /\ n e. I ) -> 0 <_ ( log ` n ) ) |
217 |
7
|
rpcnd |
|- ( ph -> U e. CC ) |
218 |
217
|
adantr |
|- ( ( ph /\ n e. I ) -> U e. CC ) |
219 |
30
|
rpred |
|- ( ph -> E e. RR ) |
220 |
219
|
adantr |
|- ( ( ph /\ n e. I ) -> E e. RR ) |
221 |
220
|
recnd |
|- ( ( ph /\ n e. I ) -> E e. CC ) |
222 |
|
divsubdir |
|- ( ( U e. CC /\ E e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U - E ) / n ) = ( ( U / n ) - ( E / n ) ) ) |
223 |
218 221 202 222
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) / n ) = ( ( U / n ) - ( E / n ) ) ) |
224 |
125 84
|
syldan |
|- ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. RR ) |
225 |
220 120
|
nndivred |
|- ( ( ph /\ n e. I ) -> ( E / n ) e. RR ) |
226 |
125 75
|
syldan |
|- ( ( ph /\ n e. I ) -> ( U / n ) e. RR ) |
227 |
125 81
|
syldan |
|- ( ( ph /\ n e. I ) -> ( R ` ( Z / n ) ) e. RR ) |
228 |
227
|
recnd |
|- ( ( ph /\ n e. I ) -> ( R ` ( Z / n ) ) e. CC ) |
229 |
38
|
adantr |
|- ( ( ph /\ n e. I ) -> Z e. RR+ ) |
230 |
229
|
rpcnne0d |
|- ( ( ph /\ n e. I ) -> ( Z e. CC /\ Z =/= 0 ) ) |
231 |
|
divdiv2 |
|- ( ( ( R ` ( Z / n ) ) e. CC /\ ( Z e. CC /\ Z =/= 0 ) /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( R ` ( Z / n ) ) / ( Z / n ) ) = ( ( ( R ` ( Z / n ) ) x. n ) / Z ) ) |
232 |
228 230 202 231
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( R ` ( Z / n ) ) / ( Z / n ) ) = ( ( ( R ` ( Z / n ) ) x. n ) / Z ) ) |
233 |
121
|
rpcnd |
|- ( ( ph /\ n e. I ) -> n e. CC ) |
234 |
|
div23 |
|- ( ( ( R ` ( Z / n ) ) e. CC /\ n e. CC /\ ( Z e. CC /\ Z =/= 0 ) ) -> ( ( ( R ` ( Z / n ) ) x. n ) / Z ) = ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) |
235 |
228 233 230 234
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( ( R ` ( Z / n ) ) x. n ) / Z ) = ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) |
236 |
232 235
|
eqtrd |
|- ( ( ph /\ n e. I ) -> ( ( R ` ( Z / n ) ) / ( Z / n ) ) = ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) |
237 |
236
|
fveq2d |
|- ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) = ( abs ` ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) ) |
238 |
125 83
|
syldan |
|- ( ( ph /\ n e. I ) -> ( ( R ` ( Z / n ) ) / Z ) e. CC ) |
239 |
238 233
|
absmuld |
|- ( ( ph /\ n e. I ) -> ( abs ` ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) = ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( abs ` n ) ) ) |
240 |
121
|
rprege0d |
|- ( ( ph /\ n e. I ) -> ( n e. RR /\ 0 <_ n ) ) |
241 |
|
absid |
|- ( ( n e. RR /\ 0 <_ n ) -> ( abs ` n ) = n ) |
242 |
240 241
|
syl |
|- ( ( ph /\ n e. I ) -> ( abs ` n ) = n ) |
243 |
242
|
oveq2d |
|- ( ( ph /\ n e. I ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( abs ` n ) ) = ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) ) |
244 |
237 239 243
|
3eqtrd |
|- ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) = ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) ) |
245 |
|
fveq2 |
|- ( u = ( Z / n ) -> ( R ` u ) = ( R ` ( Z / n ) ) ) |
246 |
|
id |
|- ( u = ( Z / n ) -> u = ( Z / n ) ) |
247 |
245 246
|
oveq12d |
|- ( u = ( Z / n ) -> ( ( R ` u ) / u ) = ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) |
248 |
247
|
fveq2d |
|- ( u = ( Z / n ) -> ( abs ` ( ( R ` u ) / u ) ) = ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) ) |
249 |
248
|
breq1d |
|- ( u = ( Z / n ) -> ( ( abs ` ( ( R ` u ) / u ) ) <_ E <-> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) <_ E ) ) |
250 |
22
|
simprd |
|- ( ph -> A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) |
251 |
250
|
adantr |
|- ( ( ph /\ n e. I ) -> A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) |
252 |
39
|
adantr |
|- ( ( ph /\ n e. I ) -> Z e. RR ) |
253 |
252 120
|
nndivred |
|- ( ( ph /\ n e. I ) -> ( Z / n ) e. RR ) |
254 |
21
|
rpregt0d |
|- ( ph -> ( V e. RR /\ 0 < V ) ) |
255 |
254
|
adantr |
|- ( ( ph /\ n e. I ) -> ( V e. RR /\ 0 < V ) ) |
256 |
|
lemuldiv2 |
|- ( ( n e. RR /\ Z e. RR /\ ( V e. RR /\ 0 < V ) ) -> ( ( V x. n ) <_ Z <-> n <_ ( Z / V ) ) ) |
257 |
137 252 255 256
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( V x. n ) <_ Z <-> n <_ ( Z / V ) ) ) |
258 |
136 257
|
mpbird |
|- ( ( ph /\ n e. I ) -> ( V x. n ) <_ Z ) |
259 |
255
|
simpld |
|- ( ( ph /\ n e. I ) -> V e. RR ) |
260 |
259 252 121
|
lemuldivd |
|- ( ( ph /\ n e. I ) -> ( ( V x. n ) <_ Z <-> V <_ ( Z / n ) ) ) |
261 |
258 260
|
mpbid |
|- ( ( ph /\ n e. I ) -> V <_ ( Z / n ) ) |
262 |
111
|
rpregt0d |
|- ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) e. RR /\ 0 < ( ( 1 + ( L x. E ) ) x. V ) ) ) |
263 |
262
|
adantr |
|- ( ( ph /\ n e. I ) -> ( ( ( 1 + ( L x. E ) ) x. V ) e. RR /\ 0 < ( ( 1 + ( L x. E ) ) x. V ) ) ) |
264 |
121
|
rpregt0d |
|- ( ( ph /\ n e. I ) -> ( n e. RR /\ 0 < n ) ) |
265 |
|
lediv23 |
|- ( ( Z e. RR /\ ( ( ( 1 + ( L x. E ) ) x. V ) e. RR /\ 0 < ( ( 1 + ( L x. E ) ) x. V ) ) /\ ( n e. RR /\ 0 < n ) ) -> ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ n <-> ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) ) |
266 |
252 263 264 265
|
syl3anc |
|- ( ( ph /\ n e. I ) -> ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ n <-> ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) ) |
267 |
189 266
|
mpbid |
|- ( ( ph /\ n e. I ) -> ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) |
268 |
21
|
rpred |
|- ( ph -> V e. RR ) |
269 |
268
|
adantr |
|- ( ( ph /\ n e. I ) -> V e. RR ) |
270 |
146
|
adantr |
|- ( ( ph /\ n e. I ) -> ( ( 1 + ( L x. E ) ) x. V ) e. RR ) |
271 |
|
elicc2 |
|- ( ( V e. RR /\ ( ( 1 + ( L x. E ) ) x. V ) e. RR ) -> ( ( Z / n ) e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) <-> ( ( Z / n ) e. RR /\ V <_ ( Z / n ) /\ ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
272 |
269 270 271
|
syl2anc |
|- ( ( ph /\ n e. I ) -> ( ( Z / n ) e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) <-> ( ( Z / n ) e. RR /\ V <_ ( Z / n ) /\ ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
273 |
253 261 267 272
|
mpbir3and |
|- ( ( ph /\ n e. I ) -> ( Z / n ) e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ) |
274 |
249 251 273
|
rspcdva |
|- ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) <_ E ) |
275 |
244 274
|
eqbrtrrd |
|- ( ( ph /\ n e. I ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) <_ E ) |
276 |
224 220 121
|
lemuldivd |
|- ( ( ph /\ n e. I ) -> ( ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) <_ E <-> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) <_ ( E / n ) ) ) |
277 |
275 276
|
mpbid |
|- ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) <_ ( E / n ) ) |
278 |
224 225 226 277
|
lesub2dd |
|- ( ( ph /\ n e. I ) -> ( ( U / n ) - ( E / n ) ) <_ ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) ) |
279 |
223 278
|
eqbrtrd |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) / n ) <_ ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) ) |
280 |
209 210 122 216 279
|
lemul1ad |
|- ( ( ph /\ n e. I ) -> ( ( ( U - E ) / n ) x. ( log ` n ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
281 |
207 280
|
eqbrtrrd |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` n ) / n ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
282 |
99 124 126 198 281
|
letrd |
|- ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
283 |
282
|
adantlr |
|- ( ( ( ph /\ n e. O ) /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
284 |
74
|
nnred |
|- ( ( ph /\ n e. O ) -> n e. RR ) |
285 |
38 151
|
rpdivcld |
|- ( ph -> ( Z / ( K ^ J ) ) e. RR+ ) |
286 |
285
|
rpred |
|- ( ph -> ( Z / ( K ^ J ) ) e. RR ) |
287 |
286
|
adantr |
|- ( ( ph /\ n e. O ) -> ( Z / ( K ^ J ) ) e. RR ) |
288 |
11
|
simpld |
|- ( ph -> Y e. RR+ ) |
289 |
38 288
|
rpdivcld |
|- ( ph -> ( Z / Y ) e. RR+ ) |
290 |
289
|
rpred |
|- ( ph -> ( Z / Y ) e. RR ) |
291 |
290
|
adantr |
|- ( ( ph /\ n e. O ) -> ( Z / Y ) e. RR ) |
292 |
|
simpr |
|- ( ( ph /\ n e. O ) -> n e. O ) |
293 |
292 20
|
eleqtrdi |
|- ( ( ph /\ n e. O ) -> n e. ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) ) |
294 |
|
elfzle2 |
|- ( n e. ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) -> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) |
295 |
293 294
|
syl |
|- ( ( ph /\ n e. O ) -> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) |
296 |
74
|
nnzd |
|- ( ( ph /\ n e. O ) -> n e. ZZ ) |
297 |
|
flge |
|- ( ( ( Z / ( K ^ J ) ) e. RR /\ n e. ZZ ) -> ( n <_ ( Z / ( K ^ J ) ) <-> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) ) |
298 |
287 296 297
|
syl2anc |
|- ( ( ph /\ n e. O ) -> ( n <_ ( Z / ( K ^ J ) ) <-> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) ) |
299 |
295 298
|
mpbird |
|- ( ( ph /\ n e. O ) -> n <_ ( Z / ( K ^ J ) ) ) |
300 |
288
|
rpred |
|- ( ph -> Y e. RR ) |
301 |
12
|
simpld |
|- ( ph -> X e. RR+ ) |
302 |
301
|
rpred |
|- ( ph -> X e. RR ) |
303 |
151
|
rpred |
|- ( ph -> ( K ^ J ) e. RR ) |
304 |
12
|
simprd |
|- ( ph -> Y < X ) |
305 |
300 302 304
|
ltled |
|- ( ph -> Y <_ X ) |
306 |
|
elfzofz |
|- ( J e. ( M ..^ N ) -> J e. ( M ... N ) ) |
307 |
23 306
|
syl |
|- ( ph -> J e. ( M ... N ) ) |
308 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pntlemh |
|- ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) ) |
309 |
307 308
|
mpdan |
|- ( ph -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) ) |
310 |
309
|
simpld |
|- ( ph -> X < ( K ^ J ) ) |
311 |
302 303 310
|
ltled |
|- ( ph -> X <_ ( K ^ J ) ) |
312 |
300 302 303 305 311
|
letrd |
|- ( ph -> Y <_ ( K ^ J ) ) |
313 |
288 151 38
|
lediv2d |
|- ( ph -> ( Y <_ ( K ^ J ) <-> ( Z / ( K ^ J ) ) <_ ( Z / Y ) ) ) |
314 |
312 313
|
mpbid |
|- ( ph -> ( Z / ( K ^ J ) ) <_ ( Z / Y ) ) |
315 |
314
|
adantr |
|- ( ( ph /\ n e. O ) -> ( Z / ( K ^ J ) ) <_ ( Z / Y ) ) |
316 |
284 287 291 299 315
|
letrd |
|- ( ( ph /\ n e. O ) -> n <_ ( Z / Y ) ) |
317 |
74 316
|
jca |
|- ( ( ph /\ n e. O ) -> ( n e. NN /\ n <_ ( Z / Y ) ) ) |
318 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
|
pntlemn |
|- ( ( ph /\ ( n e. NN /\ n <_ ( Z / Y ) ) ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
319 |
317 318
|
syldan |
|- ( ( ph /\ n e. O ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
320 |
319
|
adantr |
|- ( ( ( ph /\ n e. O ) /\ -. n e. I ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
321 |
103 104 283 320
|
ifbothda |
|- ( ( ph /\ n e. O ) -> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
322 |
58 102 87 321
|
fsumle |
|- ( ph -> sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
323 |
98 322
|
eqbrtrd |
|- ( ph -> ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |
324 |
45 56 88 89 323
|
letrd |
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) |