Step | Hyp | Ref
| Expression |
1 | | rpre 11839 |
. . . . . . . . 9
|
2 | | chpcl 24850 |
. . . . . . . . 9
ψ |
3 | 1, 2 | syl 17 |
. . . . . . . 8
ψ |
4 | 3 | recnd 10068 |
. . . . . . 7
ψ |
5 | | rprege0 11847 |
. . . . . . . . . . . . 13
|
6 | | flge0nn0 12621 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
|
8 | | nn0p1nn 11332 |
. . . . . . . . . . . 12
|
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
|
10 | 9 | nnrpd 11870 |
. . . . . . . . . 10
|
11 | 10 | relogcld 24369 |
. . . . . . . . 9
|
12 | 11 | recnd 10068 |
. . . . . . . 8
|
13 | | relogcl 24322 |
. . . . . . . . 9
|
14 | 13 | recnd 10068 |
. . . . . . . 8
|
15 | 12, 14 | subcld 10392 |
. . . . . . 7
|
16 | 4, 15 | mulcld 10060 |
. . . . . 6
ψ |
17 | | fzfid 12772 |
. . . . . . 7
|
18 | | elfznn 12370 |
. . . . . . . . . 10
|
19 | 18 | adantl 482 |
. . . . . . . . 9
|
20 | 19 | nnrpd 11870 |
. . . . . . . 8
|
21 | | 1rp 11836 |
. . . . . . . . . . . . 13
|
22 | | rpaddcl 11854 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | mpan2 707 |
. . . . . . . . . . . 12
|
24 | 23 | relogcld 24369 |
. . . . . . . . . . 11
|
25 | | relogcl 24322 |
. . . . . . . . . . 11
|
26 | 24, 25 | resubcld 10458 |
. . . . . . . . . 10
|
27 | | rpre 11839 |
. . . . . . . . . . 11
|
28 | | chpcl 24850 |
. . . . . . . . . . 11
ψ |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
ψ |
30 | 26, 29 | remulcld 10070 |
. . . . . . . . 9
ψ |
31 | 30 | recnd 10068 |
. . . . . . . 8
ψ |
32 | 20, 31 | syl 17 |
. . . . . . 7
ψ |
33 | 17, 32 | fsumcl 14464 |
. . . . . 6
ψ |
34 | | rpcnne0 11850 |
. . . . . 6
|
35 | | divsubdir 10721 |
. . . . . 6
ψ ψ
ψ ψ ψ ψ |
36 | 16, 33, 34, 35 | syl3anc 1326 |
. . . . 5
ψ ψ ψ ψ |
37 | 4, 12 | mulcld 10060 |
. . . . . . . 8
ψ |
38 | 4, 14 | mulcld 10060 |
. . . . . . . 8
ψ |
39 | 37, 38, 33 | sub32d 10424 |
. . . . . . 7
ψ ψ ψ ψ ψ ψ |
40 | 4, 12, 14 | subdid 10486 |
. . . . . . . 8
ψ ψ ψ |
41 | 40 | oveq1d 6665 |
. . . . . . 7
ψ ψ ψ ψ ψ |
42 | | fveq2 6191 |
. . . . . . . . . . 11
|
43 | | oveq1 6657 |
. . . . . . . . . . . 12
|
44 | 43 | fveq2d 6195 |
. . . . . . . . . . 11
ψ ψ |
45 | 42, 44 | jca 554 |
. . . . . . . . . 10
ψ ψ |
46 | | fveq2 6191 |
. . . . . . . . . . 11
|
47 | | oveq1 6657 |
. . . . . . . . . . . 12
|
48 | 47 | fveq2d 6195 |
. . . . . . . . . . 11
ψ ψ |
49 | 46, 48 | jca 554 |
. . . . . . . . . 10
ψ ψ |
50 | | fveq2 6191 |
. . . . . . . . . . . 12
|
51 | | log1 24332 |
. . . . . . . . . . . 12
|
52 | 50, 51 | syl6eq 2672 |
. . . . . . . . . . 11
|
53 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
54 | | 1m1e0 11089 |
. . . . . . . . . . . . . 14
|
55 | 53, 54 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
56 | 55 | fveq2d 6195 |
. . . . . . . . . . . 12
ψ ψ |
57 | | 2pos 11112 |
. . . . . . . . . . . . 13
|
58 | | 0re 10040 |
. . . . . . . . . . . . . 14
|
59 | | chpeq0 24933 |
. . . . . . . . . . . . . 14
ψ
|
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . 13
ψ |
61 | 57, 60 | mpbir 221 |
. . . . . . . . . . . 12
ψ |
62 | 56, 61 | syl6eq 2672 |
. . . . . . . . . . 11
ψ |
63 | 52, 62 | jca 554 |
. . . . . . . . . 10
ψ |
64 | | fveq2 6191 |
. . . . . . . . . . 11
|
65 | | oveq1 6657 |
. . . . . . . . . . . 12
|
66 | 65 | fveq2d 6195 |
. . . . . . . . . . 11
ψ ψ |
67 | 64, 66 | jca 554 |
. . . . . . . . . 10
ψ ψ |
68 | | nnuz 11723 |
. . . . . . . . . . 11
|
69 | 9, 68 | syl6eleq 2711 |
. . . . . . . . . 10
|
70 | | elfznn 12370 |
. . . . . . . . . . . . . 14
|
71 | 70 | adantl 482 |
. . . . . . . . . . . . 13
|
72 | 71 | nnrpd 11870 |
. . . . . . . . . . . 12
|
73 | 72 | relogcld 24369 |
. . . . . . . . . . 11
|
74 | 73 | recnd 10068 |
. . . . . . . . . 10
|
75 | 71 | nnred 11035 |
. . . . . . . . . . . . 13
|
76 | | peano2rem 10348 |
. . . . . . . . . . . . 13
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
|
78 | | chpcl 24850 |
. . . . . . . . . . . 12
ψ |
79 | 77, 78 | syl 17 |
. . . . . . . . . . 11
ψ |
80 | 79 | recnd 10068 |
. . . . . . . . . 10
ψ |
81 | 45, 49, 63, 67, 69, 74, 80 | fsumparts 14538 |
. . . . . . . . 9
..^ ψ ψ ψ ..^ ψ |
82 | 7 | nn0zd 11480 |
. . . . . . . . . . . 12
|
83 | | fzval3 12536 |
. . . . . . . . . . . 12
..^ |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
..^ |
85 | 84 | eqcomd 2628 |
. . . . . . . . . 10
..^ |
86 | 19 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
87 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . 18
|
88 | | pncan 10287 |
. . . . . . . . . . . . . . . . . 18
|
89 | 86, 87, 88 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
90 | | npcan 10290 |
. . . . . . . . . . . . . . . . . 18
|
91 | 86, 87, 90 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
92 | 89, 91 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
93 | 92 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
ψ ψ |
94 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . 17
|
95 | 19, 94 | syl 17 |
. . . . . . . . . . . . . . . 16
|
96 | | chpp1 24881 |
. . . . . . . . . . . . . . . 16
ψ ψ Λ |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . 15
ψ ψ Λ |
98 | 91 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
Λ Λ |
99 | 98 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
ψ Λ ψ Λ |
100 | 93, 97, 99 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
ψ ψ Λ |
101 | 100 | oveq1d 6665 |
. . . . . . . . . . . . 13
ψ ψ ψ
Λ ψ |
102 | 95 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
|
103 | | chpcl 24850 |
. . . . . . . . . . . . . . . 16
ψ |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
ψ |
105 | 104 | recnd 10068 |
. . . . . . . . . . . . . 14
ψ |
106 | | vmacl 24844 |
. . . . . . . . . . . . . . . 16
Λ |
107 | 19, 106 | syl 17 |
. . . . . . . . . . . . . . 15
Λ |
108 | 107 | recnd 10068 |
. . . . . . . . . . . . . 14
Λ |
109 | 105, 108 | pncan2d 10394 |
. . . . . . . . . . . . 13
ψ Λ ψ Λ |
110 | 101, 109 | eqtrd 2656 |
. . . . . . . . . . . 12
ψ ψ Λ |
111 | 110 | oveq2d 6666 |
. . . . . . . . . . 11
ψ ψ
Λ |
112 | 20 | relogcld 24369 |
. . . . . . . . . . . . 13
|
113 | 112 | recnd 10068 |
. . . . . . . . . . . 12
|
114 | 108, 113 | mulcomd 10061 |
. . . . . . . . . . 11
Λ Λ |
115 | 111, 114 | eqtr4d 2659 |
. . . . . . . . . 10
ψ ψ
Λ |
116 | 85, 115 | sumeq12rdv 14438 |
. . . . . . . . 9
..^ ψ ψ Λ |
117 | 7 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
|
118 | | pncan 10287 |
. . . . . . . . . . . . . . . . 17
|
119 | 117, 87, 118 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
ψ ψ |
121 | | chpfl 24876 |
. . . . . . . . . . . . . . . 16
ψ ψ |
122 | 1, 121 | syl 17 |
. . . . . . . . . . . . . . 15
ψ ψ |
123 | 120, 122 | eqtrd 2656 |
. . . . . . . . . . . . . 14
ψ ψ |
124 | 123 | oveq2d 6666 |
. . . . . . . . . . . . 13
ψ ψ |
125 | 12, 4 | mulcomd 10061 |
. . . . . . . . . . . . 13
ψ ψ |
126 | 124, 125 | eqtrd 2656 |
. . . . . . . . . . . 12
ψ ψ |
127 | | 0cn 10032 |
. . . . . . . . . . . . . 14
|
128 | 127 | mul01i 10226 |
. . . . . . . . . . . . 13
|
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
|
130 | 126, 129 | oveq12d 6668 |
. . . . . . . . . . 11
ψ ψ |
131 | 37 | subid1d 10381 |
. . . . . . . . . . 11
ψ ψ |
132 | 130, 131 | eqtrd 2656 |
. . . . . . . . . 10
ψ ψ |
133 | 89 | fveq2d 6195 |
. . . . . . . . . . . 12
ψ ψ |
134 | 133 | oveq2d 6666 |
. . . . . . . . . . 11
ψ ψ |
135 | 85, 134 | sumeq12rdv 14438 |
. . . . . . . . . 10
..^ ψ ψ |
136 | 132, 135 | oveq12d 6668 |
. . . . . . . . 9
ψ ..^ ψ ψ ψ |
137 | 81, 116, 136 | 3eqtr3d 2664 |
. . . . . . . 8
Λ ψ ψ |
138 | 137 | oveq1d 6665 |
. . . . . . 7
Λ ψ ψ ψ ψ |
139 | 39, 41, 138 | 3eqtr4d 2666 |
. . . . . 6
ψ ψ Λ ψ |
140 | 139 | oveq1d 6665 |
. . . . 5
ψ ψ
Λ ψ |
141 | | div23 10704 |
. . . . . . 7
ψ
ψ ψ |
142 | 4, 15, 34, 141 | syl3anc 1326 |
. . . . . 6
ψ ψ |
143 | 142 | oveq1d 6665 |
. . . . 5
ψ ψ ψ ψ |
144 | 36, 140, 143 | 3eqtr3rd 2665 |
. . . 4
ψ ψ
Λ ψ |
145 | 144 | mpteq2ia 4740 |
. . 3
ψ ψ
Λ ψ |
146 | | ovexd 6680 |
. . . 4
ψ |
147 | | ovexd 6680 |
. . . 4
ψ |
148 | | reex 10027 |
. . . . . . . 8
|
149 | | rpssre 11843 |
. . . . . . . 8
|
150 | 148, 149 | ssexi 4803 |
. . . . . . 7
|
151 | 150 | a1i 11 |
. . . . . 6
|
152 | | ovexd 6680 |
. . . . . 6
ψ |
153 | 15 | adantl 482 |
. . . . . 6
|
154 | | eqidd 2623 |
. . . . . 6
ψ ψ |
155 | | eqidd 2623 |
. . . . . 6
|
156 | 151, 152,
153, 154, 155 | offval2 6914 |
. . . . 5
ψ ψ |
157 | | chpo1ub 25169 |
. . . . . 6
ψ |
158 | | 0red 10041 |
. . . . . . . 8
|
159 | | 1red 10055 |
. . . . . . . 8
|
160 | | divrcnv 14584 |
. . . . . . . . 9
|
161 | 87, 160 | mp1i 13 |
. . . . . . . 8
|
162 | | rpreccl 11857 |
. . . . . . . . . 10
|
163 | 162 | rpred 11872 |
. . . . . . . . 9
|
164 | 163 | adantl 482 |
. . . . . . . 8
|
165 | 11, 13 | resubcld 10458 |
. . . . . . . . 9
|
166 | 165 | adantl 482 |
. . . . . . . 8
|
167 | | rpaddcl 11854 |
. . . . . . . . . . . . 13
|
168 | 21, 167 | mpan2 707 |
. . . . . . . . . . . 12
|
169 | 168 | relogcld 24369 |
. . . . . . . . . . 11
|
170 | 169, 13 | resubcld 10458 |
. . . . . . . . . 10
|
171 | 7 | nn0red 11352 |
. . . . . . . . . . . . 13
|
172 | | 1red 10055 |
. . . . . . . . . . . . 13
|
173 | | flle 12600 |
. . . . . . . . . . . . . 14
|
174 | 1, 173 | syl 17 |
. . . . . . . . . . . . 13
|
175 | 171, 1, 172, 174 | leadd1dd 10641 |
. . . . . . . . . . . 12
|
176 | 10, 168 | logled 24373 |
. . . . . . . . . . . 12
|
177 | 175, 176 | mpbid 222 |
. . . . . . . . . . 11
|
178 | 11, 169, 13, 177 | lesub1dd 10643 |
. . . . . . . . . 10
|
179 | | logdifbnd 24720 |
. . . . . . . . . 10
|
180 | 165, 170,
163, 178, 179 | letrd 10194 |
. . . . . . . . 9
|
181 | 180 | ad2antrl 764 |
. . . . . . . 8
|
182 | | fllep1 12602 |
. . . . . . . . . . . 12
|
183 | 1, 182 | syl 17 |
. . . . . . . . . . 11
|
184 | | logleb 24349 |
. . . . . . . . . . . 12
|
185 | 10, 184 | mpdan 702 |
. . . . . . . . . . 11
|
186 | 183, 185 | mpbid 222 |
. . . . . . . . . 10
|
187 | 11, 13 | subge0d 10617 |
. . . . . . . . . 10
|
188 | 186, 187 | mpbird 247 |
. . . . . . . . 9
|
189 | 188 | ad2antrl 764 |
. . . . . . . 8
|
190 | 158, 159,
161, 164, 166, 181, 189 | rlimsqz2 14381 |
. . . . . . 7
|
191 | | rlimo1 14347 |
. . . . . . 7
|
192 | 190, 191 | syl 17 |
. . . . . 6
|
193 | | o1mul 14345 |
. . . . . 6
ψ ψ |
194 | 157, 192,
193 | sylancr 695 |
. . . . 5
ψ |
195 | 156, 194 | eqeltrrd 2702 |
. . . 4
ψ |
196 | | nnrp 11842 |
. . . . . . . . 9
|
197 | 196 | ssriv 3607 |
. . . . . . . 8
|
198 | 197 | a1i 11 |
. . . . . . 7
|
199 | 198 | sselda 3603 |
. . . . . 6
|
200 | 199, 31 | syl 17 |
. . . . 5
ψ |
201 | | chpo1ub 25169 |
. . . . . . . 8
ψ |
202 | 201 | a1i 11 |
. . . . . . 7
ψ |
203 | | rerpdivcl 11861 |
. . . . . . . . 9
ψ
ψ |
204 | 29, 203 | mpancom 703 |
. . . . . . . 8
ψ |
205 | 204 | adantl 482 |
. . . . . . 7
ψ |
206 | 31 | adantl 482 |
. . . . . . 7
ψ |
207 | | rpreccl 11857 |
. . . . . . . . . . 11
|
208 | 207 | rpred 11872 |
. . . . . . . . . 10
|
209 | | chpge0 24852 |
. . . . . . . . . . 11
ψ |
210 | 27, 209 | syl 17 |
. . . . . . . . . 10
ψ |
211 | | logdifbnd 24720 |
. . . . . . . . . 10
|
212 | 26, 208, 29, 210, 211 | lemul1ad 10963 |
. . . . . . . . 9
ψ
ψ |
213 | 27 | lep1d 10955 |
. . . . . . . . . . . . 13
|
214 | | logleb 24349 |
. . . . . . . . . . . . . 14
|
215 | 23, 214 | mpdan 702 |
. . . . . . . . . . . . 13
|
216 | 213, 215 | mpbid 222 |
. . . . . . . . . . . 12
|
217 | 24, 25 | subge0d 10617 |
. . . . . . . . . . . 12
|
218 | 216, 217 | mpbird 247 |
. . . . . . . . . . 11
|
219 | 26, 29, 218, 210 | mulge0d 10604 |
. . . . . . . . . 10
ψ |
220 | 30, 219 | absidd 14161 |
. . . . . . . . 9
ψ ψ |
221 | | rpregt0 11846 |
. . . . . . . . . . . 12
|
222 | | divge0 10892 |
. . . . . . . . . . . 12
ψ ψ ψ |
223 | 29, 210, 221, 222 | syl21anc 1325 |
. . . . . . . . . . 11
ψ |
224 | 204, 223 | absidd 14161 |
. . . . . . . . . 10
ψ ψ |
225 | 29 | recnd 10068 |
. . . . . . . . . . 11
ψ |
226 | | rpcn 11841 |
. . . . . . . . . . 11
|
227 | | rpne0 11848 |
. . . . . . . . . . 11
|
228 | 225, 226,
227 | divrec2d 10805 |
. . . . . . . . . 10
ψ ψ |
229 | 224, 228 | eqtrd 2656 |
. . . . . . . . 9
ψ ψ |
230 | 212, 220,
229 | 3brtr4d 4685 |
. . . . . . . 8
ψ ψ |
231 | 230 | ad2antrl 764 |
. . . . . . 7
ψ ψ |
232 | 159, 202,
205, 206, 231 | o1le 14383 |
. . . . . 6
ψ |
233 | 198, 232 | o1res2 14294 |
. . . . 5
ψ |
234 | 200, 233 | o1fsum 14545 |
. . . 4
ψ |
235 | 146, 147,
195, 234 | o1sub2 14356 |
. . 3
ψ ψ |
236 | 145, 235 | syl5eqelr 2706 |
. 2
Λ ψ |
237 | 236 | trud 1493 |
1
Λ ψ |