Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
|
2 | | 2re 11090 |
. . . . . . . . . . 11
|
3 | | 1lt2 11194 |
. . . . . . . . . . 11
|
4 | | rplogcl 24350 |
. . . . . . . . . . 11
|
5 | 2, 3, 4 | mp2an 708 |
. . . . . . . . . 10
|
6 | | elrp 11834 |
. . . . . . . . . 10
|
7 | 5, 6 | mpbi 220 |
. . . . . . . . 9
|
8 | 7 | simpli 474 |
. . . . . . . 8
|
9 | 8 | recni 10052 |
. . . . . . 7
|
10 | 9 | mulid1i 10042 |
. . . . . 6
|
11 | | cht2 24898 |
. . . . . 6
|
12 | 10, 11 | eqtr4i 2647 |
. . . . 5
|
13 | 1, 12 | syl6reqr 2675 |
. . . 4
|
14 | | chtfl 24875 |
. . . . 5
|
15 | 14 | adantr 481 |
. . . 4
|
16 | 13, 15 | sylan9eqr 2678 |
. . 3
|
17 | | 2t2e4 11177 |
. . . . . . 7
|
18 | | df-4 11081 |
. . . . . . 7
|
19 | 17, 18 | eqtri 2644 |
. . . . . 6
|
20 | | simplr 792 |
. . . . . . 7
|
21 | 2 | a1i 11 |
. . . . . . . 8
|
22 | | simpl 473 |
. . . . . . . . 9
|
23 | 22 | adantr 481 |
. . . . . . . 8
|
24 | | 2pos 11112 |
. . . . . . . . . 10
|
25 | 2, 24 | pm3.2i 471 |
. . . . . . . . 9
|
26 | 25 | a1i 11 |
. . . . . . . 8
|
27 | | ltmul2 10874 |
. . . . . . . 8
|
28 | 21, 23, 26, 27 | syl3anc 1326 |
. . . . . . 7
|
29 | 20, 28 | mpbid 222 |
. . . . . 6
|
30 | 19, 29 | syl5eqbrr 4689 |
. . . . 5
|
31 | | 3re 11094 |
. . . . . . 7
|
32 | 31 | a1i 11 |
. . . . . 6
|
33 | | 1red 10055 |
. . . . . 6
|
34 | | remulcl 10021 |
. . . . . . . 8
|
35 | 2, 22, 34 | sylancr 695 |
. . . . . . 7
|
36 | 35 | adantr 481 |
. . . . . 6
|
37 | 32, 33, 36 | ltaddsub2d 10628 |
. . . . 5
|
38 | 30, 37 | mpbid 222 |
. . . 4
|
39 | | resubcl 10345 |
. . . . . . 7
|
40 | 35, 31, 39 | sylancl 694 |
. . . . . 6
|
41 | 40 | adantr 481 |
. . . . 5
|
42 | 7 | a1i 11 |
. . . . 5
|
43 | | ltmul2 10874 |
. . . . 5
|
44 | 33, 41, 42, 43 | syl3anc 1326 |
. . . 4
|
45 | 38, 44 | mpbid 222 |
. . 3
|
46 | 16, 45 | eqbrtrrd 4677 |
. 2
|
47 | | chtcl 24835 |
. . . 4
|
48 | 47 | ad2antrr 762 |
. . 3
|
49 | | reflcl 12597 |
. . . . . . 7
|
50 | 49 | ad2antrr 762 |
. . . . . 6
|
51 | | remulcl 10021 |
. . . . . 6
|
52 | 2, 50, 51 | sylancr 695 |
. . . . 5
|
53 | | resubcl 10345 |
. . . . 5
|
54 | 52, 31, 53 | sylancl 694 |
. . . 4
|
55 | | remulcl 10021 |
. . . 4
|
56 | 8, 54, 55 | sylancr 695 |
. . 3
|
57 | 40 | adantr 481 |
. . . 4
|
58 | | remulcl 10021 |
. . . 4
|
59 | 8, 57, 58 | sylancr 695 |
. . 3
|
60 | 15 | adantr 481 |
. . . 4
|
61 | | simpr 477 |
. . . . . 6
|
62 | | df-3 11080 |
. . . . . . 7
|
63 | 62 | fveq2i 6194 |
. . . . . 6
|
64 | 61, 63 | syl6eleqr 2712 |
. . . . 5
|
65 | | eluzfz2 12349 |
. . . . . 6
|
66 | | 3z 11410 |
. . . . . . 7
|
67 | | oveq2 6658 |
. . . . . . . 8
|
68 | 67 | raleqdv 3144 |
. . . . . . 7
|
69 | | oveq2 6658 |
. . . . . . . 8
|
70 | 69 | raleqdv 3144 |
. . . . . . 7
|
71 | | oveq2 6658 |
. . . . . . . 8
|
72 | 71 | raleqdv 3144 |
. . . . . . 7
|
73 | | oveq2 6658 |
. . . . . . . 8
|
74 | 73 | raleqdv 3144 |
. . . . . . 7
|
75 | | 6lt8 11216 |
. . . . . . . . . . 11
|
76 | | 6re 11101 |
. . . . . . . . . . . . 13
|
77 | | 6pos 11119 |
. . . . . . . . . . . . 13
|
78 | 76, 77 | elrpii 11835 |
. . . . . . . . . . . 12
|
79 | | 8re 11105 |
. . . . . . . . . . . . 13
|
80 | | 8pos 11121 |
. . . . . . . . . . . . 13
|
81 | 79, 80 | elrpii 11835 |
. . . . . . . . . . . 12
|
82 | | logltb 24346 |
. . . . . . . . . . . 12
|
83 | 78, 81, 82 | mp2an 708 |
. . . . . . . . . . 11
|
84 | 75, 83 | mpbi 220 |
. . . . . . . . . 10
|
85 | 84 | a1i 11 |
. . . . . . . . 9
|
86 | | elfz1eq 12352 |
. . . . . . . . . . 11
|
87 | 86 | fveq2d 6195 |
. . . . . . . . . 10
|
88 | | cht3 24899 |
. . . . . . . . . 10
|
89 | 87, 88 | syl6eq 2672 |
. . . . . . . . 9
|
90 | 86 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
91 | 90 | oveq1d 6665 |
. . . . . . . . . . . 12
|
92 | | 3cn 11095 |
. . . . . . . . . . . . . . 15
|
93 | 92 | 2timesi 11147 |
. . . . . . . . . . . . . 14
|
94 | 93 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
95 | 92, 92 | pncan3oi 10297 |
. . . . . . . . . . . . 13
|
96 | 94, 95 | eqtri 2644 |
. . . . . . . . . . . 12
|
97 | 91, 96 | syl6eq 2672 |
. . . . . . . . . . 11
|
98 | 97 | oveq2d 6666 |
. . . . . . . . . 10
|
99 | | 2rp 11837 |
. . . . . . . . . . . . . . 15
|
100 | | relogcl 24322 |
. . . . . . . . . . . . . . 15
|
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
102 | 101 | recni 10052 |
. . . . . . . . . . . . 13
|
103 | 102, 92 | mulcomi 10046 |
. . . . . . . . . . . 12
|
104 | | relogexp 24342 |
. . . . . . . . . . . . 13
|
105 | 99, 66, 104 | mp2an 708 |
. . . . . . . . . . . 12
|
106 | 103, 105 | eqtr4i 2647 |
. . . . . . . . . . 11
|
107 | | cu2 12963 |
. . . . . . . . . . . 12
|
108 | 107 | fveq2i 6194 |
. . . . . . . . . . 11
|
109 | 106, 108 | eqtri 2644 |
. . . . . . . . . 10
|
110 | 98, 109 | syl6eq 2672 |
. . . . . . . . 9
|
111 | 85, 89, 110 | 3brtr4d 4685 |
. . . . . . . 8
|
112 | 111 | rgen 2922 |
. . . . . . 7
|
113 | | df-2 11079 |
. . . . . . . . . . . . . . . . . 18
|
114 | | 2div2e1 11150 |
. . . . . . . . . . . . . . . . . . . 20
|
115 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
116 | 62, 115 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . . . . 22
|
117 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
118 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
120 | 117, 118,
119 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
|
121 | 116, 120 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
|
122 | | eluzelre 11698 |
. . . . . . . . . . . . . . . . . . . . . 22
|
123 | | ltdiv1 10887 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
124 | 2, 25, 123 | mp3an13 1415 |
. . . . . . . . . . . . . . . . . . . . . 22
|
125 | 122, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
126 | 121, 125 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 114, 126 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 122 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . 21
|
130 | | ltadd1 10495 |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | 129, 129,
130 | mp3an13 1415 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | 128, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 127, 132 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
134 | 113, 133 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . 17
|
135 | 134 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
136 | | peano2z 11418 |
. . . . . . . . . . . . . . . . . 18
|
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
138 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . 17
|
139 | 117, 137,
138 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
140 | 135, 139 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
141 | 62, 140 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
|
142 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
143 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . 19
|
144 | 129, 128,
143 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
145 | 127, 144 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
146 | 142, 128,
128, 145 | leadd2dd 10642 |
. . . . . . . . . . . . . . . 16
|
147 | 122 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
148 | 147 | 2halvesd 11278 |
. . . . . . . . . . . . . . . 16
|
149 | 146, 148 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
|
150 | 149 | adantr 481 |
. . . . . . . . . . . . . 14
|
151 | | elfz 12332 |
. . . . . . . . . . . . . . . 16
|
152 | 66, 151 | mp3an2 1412 |
. . . . . . . . . . . . . . 15
|
153 | 136, 118,
152 | syl2anr 495 |
. . . . . . . . . . . . . 14
|
154 | 141, 150,
153 | mpbir2and 957 |
. . . . . . . . . . . . 13
|
155 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
156 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
157 | 156 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
158 | 157 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
159 | 155, 158 | breq12d 4666 |
. . . . . . . . . . . . . 14
|
160 | 159 | rspcv 3305 |
. . . . . . . . . . . . 13
|
161 | 154, 160 | syl 17 |
. . . . . . . . . . . 12
|
162 | 128 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
163 | 162 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . 21
|
165 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . 21
|
166 | | adddi 10025 |
. . . . . . . . . . . . . . . . . . . . 21
|
167 | 164, 165,
166 | mp3an13 1415 |
. . . . . . . . . . . . . . . . . . . 20
|
168 | 163, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
169 | 147 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
170 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . 22
|
171 | | divcan2 10693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
172 | 164, 170,
171 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . . . 21
|
173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
174 | 164 | mulid1i 10042 |
. . . . . . . . . . . . . . . . . . . . 21
|
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
176 | 173, 175 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
177 | 168, 176 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
178 | 177 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
179 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . . . . . 20
|
180 | 92, 164, 165, 179 | subaddrii 10370 |
. . . . . . . . . . . . . . . . . . 19
|
181 | 180 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . 18
|
182 | | subsub3 10313 |
. . . . . . . . . . . . . . . . . . . 20
|
183 | 92, 164, 182 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . 19
|
184 | 169, 183 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
185 | 181, 184 | syl5reqr 2671 |
. . . . . . . . . . . . . . . . 17
|
186 | 178, 185 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
187 | 186 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
188 | 187 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
189 | 137 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
190 | | chtcl 24835 |
. . . . . . . . . . . . . . . 16
|
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . 15
|
192 | 122 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
193 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . 17
|
194 | 192, 193 | syl 17 |
. . . . . . . . . . . . . . . 16
|
195 | | remulcl 10021 |
. . . . . . . . . . . . . . . 16
|
196 | 101, 194,
195 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
197 | | remulcl 10021 |
. . . . . . . . . . . . . . . 16
|
198 | 101, 192,
197 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
199 | 191, 196,
198 | ltadd1d 10620 |
. . . . . . . . . . . . . 14
|
200 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
201 | 194 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
202 | 200, 201,
169 | adddid 10064 |
. . . . . . . . . . . . . . . 16
|
203 | | adddi 10025 |
. . . . . . . . . . . . . . . . . . . . . 22
|
204 | 164, 165,
203 | mp3an13 1415 |
. . . . . . . . . . . . . . . . . . . . 21
|
205 | 169, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
206 | 174 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . 20
|
207 | 205, 206 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 207 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
209 | | zmulcl 11426 |
. . . . . . . . . . . . . . . . . . . . . 22
|
210 | 117, 118,
209 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
|
211 | 210 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
212 | 211 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
213 | | subsub3 10313 |
. . . . . . . . . . . . . . . . . . . 20
|
214 | 92, 164, 213 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . 19
|
215 | 212, 214 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
216 | 180 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . 19
|
217 | 169 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . . . . 21
|
218 | 217 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | 165 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
220 | 169, 169,
219 | addsubd 10413 |
. . . . . . . . . . . . . . . . . . . 20
|
221 | 218, 220 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
222 | 216, 221 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
|
223 | 208, 215,
222 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . . . 17
|
224 | 223 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
225 | 202, 224 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
226 | 225 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
227 | 188, 199,
226 | 3bitrd 294 |
. . . . . . . . . . . . 13
|
228 | | 3nn 11186 |
. . . . . . . . . . . . . . . . 17
|
229 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . 18
|
230 | 154, 229 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
231 | | eluznn 11758 |
. . . . . . . . . . . . . . . . 17
|
232 | 228, 230,
231 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
233 | | chtublem 24936 |
. . . . . . . . . . . . . . . 16
|
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . 15
|
235 | 177 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
236 | | addsubass 10291 |
. . . . . . . . . . . . . . . . . . . 20
|
237 | 164, 165,
236 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . 19
|
238 | 169, 237 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
239 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . 19
|
240 | 239 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . 18
|
241 | 238, 240 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
242 | 235, 241 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
243 | 242 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
244 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . 19
|
245 | 163, 165,
244 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
246 | 245 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
247 | | relogexp 24342 |
. . . . . . . . . . . . . . . . . . . . 21
|
248 | 99, 117, 247 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . 20
|
249 | | sq2 12960 |
. . . . . . . . . . . . . . . . . . . . 21
|
250 | 249 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . 20
|
251 | 164, 102 | mulcomi 10046 |
. . . . . . . . . . . . . . . . . . . 20
|
252 | 248, 250,
251 | 3eqtr3i 2652 |
. . . . . . . . . . . . . . . . . . 19
|
253 | 252 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . 18
|
254 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
255 | 200, 254,
163 | mulassd 10063 |
. . . . . . . . . . . . . . . . . 18
|
256 | 253, 255 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
|
257 | 173 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
258 | 246, 256,
257 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
259 | 258 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
260 | 234, 243,
259 | 3brtr3d 4684 |
. . . . . . . . . . . . . 14
|
261 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . 19
|
262 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . 19
|
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
264 | 263 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
265 | 264 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
266 | | chtcl 24835 |
. . . . . . . . . . . . . . . 16
|
267 | 265, 266 | syl 17 |
. . . . . . . . . . . . . . 15
|
268 | 191, 198 | readdcld 10069 |
. . . . . . . . . . . . . . 15
|
269 | | zmulcl 11426 |
. . . . . . . . . . . . . . . . . . . 20
|
270 | 117, 263,
269 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
271 | 270 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
272 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . 18
|
273 | 271, 31, 272 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
274 | 273 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
275 | | remulcl 10021 |
. . . . . . . . . . . . . . . 16
|
276 | 101, 274,
275 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
277 | | lelttr 10128 |
. . . . . . . . . . . . . . 15
|
278 | 267, 268,
276, 277 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
279 | 260, 278 | mpand 711 |
. . . . . . . . . . . . 13
|
280 | 227, 279 | sylbid 230 |
. . . . . . . . . . . 12
|
281 | 161, 280 | syld 47 |
. . . . . . . . . . 11
|
282 | | eluzfz2 12349 |
. . . . . . . . . . . . . 14
|
283 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
284 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
285 | 284 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
286 | 285 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
287 | 283, 286 | breq12d 4666 |
. . . . . . . . . . . . . . 15
|
288 | 287 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
289 | 282, 288 | syl 17 |
. . . . . . . . . . . . 13
|
290 | 289 | adantr 481 |
. . . . . . . . . . . 12
|
291 | 210 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
292 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
293 | 122 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . 18
|
294 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
295 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . . . 19
|
296 | 122, 264,
294, 295 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
297 | 293, 296 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
298 | 291, 271,
292, 297 | ltsub1dd 10639 |
. . . . . . . . . . . . . . . 16
|
299 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . 18
|
300 | 291, 31, 299 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
301 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
302 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . 17
|
303 | 300, 273,
301, 302 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
304 | 298, 303 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
305 | | chtcl 24835 |
. . . . . . . . . . . . . . . . 17
|
306 | 122, 305 | syl 17 |
. . . . . . . . . . . . . . . 16
|
307 | | remulcl 10021 |
. . . . . . . . . . . . . . . . 17
|
308 | 101, 300,
307 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
309 | 101, 273,
275 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
310 | | lttr 10114 |
. . . . . . . . . . . . . . . 16
|
311 | 306, 308,
309, 310 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
312 | 304, 311 | mpan2d 710 |
. . . . . . . . . . . . . 14
|
313 | 312 | adantr 481 |
. . . . . . . . . . . . 13
|
314 | 118 | adantr 481 |
. . . . . . . . . . . . . . 15
|
315 | | dvdsval2 14986 |
. . . . . . . . . . . . . . . . . . 19
|
316 | 117, 170,
315 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . 18
|
317 | 263, 316 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
318 | | 2lt3 11195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
319 | 2, 31 | ltnlei 10158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
320 | 318, 319 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
321 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
322 | 320, 321 | mtbii 316 |
. . . . . . . . . . . . . . . . . . . . . 22
|
323 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
324 | 261, 323 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
325 | 322, 324 | nsyl3 133 |
. . . . . . . . . . . . . . . . . . . . 21
|
326 | 325 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
327 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . . 22
|
328 | 117, 327 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
329 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
330 | | dvdsprm 15415 |
. . . . . . . . . . . . . . . . . . . . 21
|
331 | 328, 329,
330 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
332 | 326, 331 | mtbird 315 |
. . . . . . . . . . . . . . . . . . 19
|
333 | 332 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
334 | 333 | con2d 129 |
. . . . . . . . . . . . . . . . 17
|
335 | 317, 334 | sylbird 250 |
. . . . . . . . . . . . . . . 16
|
336 | 335 | imp 445 |
. . . . . . . . . . . . . . 15
|
337 | | chtnprm 24880 |
. . . . . . . . . . . . . . 15
|
338 | 314, 336,
337 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
339 | 338 | breq1d 4663 |
. . . . . . . . . . . . 13
|
340 | 313, 339 | sylibrd 249 |
. . . . . . . . . . . 12
|
341 | 290, 340 | syld 47 |
. . . . . . . . . . 11
|
342 | | zeo 11463 |
. . . . . . . . . . . 12
|
343 | 118, 342 | syl 17 |
. . . . . . . . . . 11
|
344 | 281, 341,
343 | mpjaodan 827 |
. . . . . . . . . 10
|
345 | | ovex 6678 |
. . . . . . . . . . 11
|
346 | | fveq2 6191 |
. . . . . . . . . . . 12
|
347 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
348 | 347 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
349 | 348 | oveq2d 6666 |
. . . . . . . . . . . 12
|
350 | 346, 349 | breq12d 4666 |
. . . . . . . . . . 11
|
351 | 345, 350 | ralsn 4222 |
. . . . . . . . . 10
|
352 | 344, 351 | syl6ibr 242 |
. . . . . . . . 9
|
353 | 352 | ancld 576 |
. . . . . . . 8
|
354 | | ralun 3795 |
. . . . . . . . 9
|
355 | | fzsuc 12388 |
. . . . . . . . . 10
|
356 | 355 | raleqdv 3144 |
. . . . . . . . 9
|
357 | 354, 356 | syl5ibr 236 |
. . . . . . . 8
|
358 | 353, 357 | syld 47 |
. . . . . . 7
|
359 | 66, 68, 70, 72, 74, 112, 358 | uzind4i 11750 |
. . . . . 6
|
360 | | fveq2 6191 |
. . . . . . . 8
|
361 | | oveq2 6658 |
. . . . . . . . . 10
|
362 | 361 | oveq1d 6665 |
. . . . . . . . 9
|
363 | 362 | oveq2d 6666 |
. . . . . . . 8
|
364 | 360, 363 | breq12d 4666 |
. . . . . . 7
|
365 | 364 | rspcv 3305 |
. . . . . 6
|
366 | 65, 359, 365 | sylc 65 |
. . . . 5
|
367 | 64, 366 | syl 17 |
. . . 4
|
368 | 60, 367 | eqbrtrrd 4677 |
. . 3
|
369 | 35 | adantr 481 |
. . . . 5
|
370 | 31 | a1i 11 |
. . . . 5
|
371 | | flle 12600 |
. . . . . . 7
|
372 | 371 | ad2antrr 762 |
. . . . . 6
|
373 | 22 | adantr 481 |
. . . . . . 7
|
374 | 25 | a1i 11 |
. . . . . . 7
|
375 | | lemul2 10876 |
. . . . . . 7
|
376 | 50, 373, 374, 375 | syl3anc 1326 |
. . . . . 6
|
377 | 372, 376 | mpbid 222 |
. . . . 5
|
378 | 52, 369, 370, 377 | lesub1dd 10643 |
. . . 4
|
379 | 7 | a1i 11 |
. . . . 5
|
380 | | lemul2 10876 |
. . . . 5
|
381 | 54, 57, 379, 380 | syl3anc 1326 |
. . . 4
|
382 | 378, 381 | mpbid 222 |
. . 3
|
383 | 48, 56, 59, 368, 382 | ltletrd 10197 |
. 2
|
384 | 117 | a1i 11 |
. . . 4
|
385 | | flcl 12596 |
. . . . 5
|
386 | 385 | adantr 481 |
. . . 4
|
387 | | ltle 10126 |
. . . . . . 7
|
388 | 2, 387 | mpan 706 |
. . . . . 6
|
389 | | flge 12606 |
. . . . . . 7
|
390 | 117, 389 | mpan2 707 |
. . . . . 6
|
391 | 388, 390 | sylibd 229 |
. . . . 5
|
392 | 391 | imp 445 |
. . . 4
|
393 | | eluz2 11693 |
. . . 4
|
394 | 384, 386,
392, 393 | syl3anbrc 1246 |
. . 3
|
395 | | uzp1 11721 |
. . 3
|
396 | 394, 395 | syl 17 |
. 2
|
397 | 46, 383, 396 | mpjaodan 827 |
1
|