Step Hyp Ref
Expression
1 zre 10893
. . . 4
2 zre 10893
. . . 4
3 subge0 10090
. . . . 5
4 resubcl 9906
. . . . . . 7
5 0re 9617
. . . . . . . 8
6 1re 9616
. . . . . . . 8
7 leadd1 10045
. . . . . . . 8
8 5 , 6 , 7 mp3an13 1315
. . . . . . 7
9 4 , 8 syl 16
. . . . . 6
10 ax-1cn 9571
. . . . . . . 8
11 10 addid2i 9789
. . . . . . 7
12 11 breq1i 4459
. . . . . 6
13 9 , 12 syl6bb 261
. . . . 5
14 3 , 13 bitr3d 255
. . . 4
15 1 , 2 , 14 syl2an 477
. . 3
16 zsubcl 10931
. . . . 5
17 peano2z 10930
. . . . 5
18 16 , 17 syl 16
. . . 4
19 elnnz1 10915
. . . . . . . 8
20 eleq1 2529
. . . . . . . . . 10
21 ovex 6324
. . . . . . . . . . . . . . 15
22 21 isseti 3115
. . . . . . . . . . . . . 14
23 nfv 1707
. . . . . . . . . . . . . . . 16
24 nfsbc1v 3347
. . . . . . . . . . . . . . . . 17
25 uzindOLD.5
. . . . . . . . . . . . . . . . . 18
26 25 nfth 1625
. . . . . . . . . . . . . . . . 17
27 24 , 26 nfbi 1934
. . . . . . . . . . . . . . . 16
28 23 , 27 nfim 1920
. . . . . . . . . . . . . . 15
29 sbceq1a 3338
. . . . . . . . . . . . . . . . . 18
30 29 adantr 465
. . . . . . . . . . . . . . . . 17
31 oveq1 6303
. . . . . . . . . . . . . . . . . . . . 21
32 31 oveq1d 6311
. . . . . . . . . . . . . . . . . . . 20
33 10 subidi 9913
. . . . . . . . . . . . . . . . . . . . . 22
34 33 oveq1i 6306
. . . . . . . . . . . . . . . . . . . . 21
35 zcn 10894
. . . . . . . . . . . . . . . . . . . . . 22
36 addid2 9784
. . . . . . . . . . . . . . . . . . . . . 22
37 35 , 36 syl 16
. . . . . . . . . . . . . . . . . . . . 21
38 34 , 37 syl5eq 2510
. . . . . . . . . . . . . . . . . . . 20
39 32 , 38 sylan9eq 2518
. . . . . . . . . . . . . . . . . . 19
40 eqtr 2483
. . . . . . . . . . . . . . . . . . 19
41 39 , 40 sylan2 474
. . . . . . . . . . . . . . . . . 18
42 uzindOLD.1
. . . . . . . . . . . . . . . . . 18
43 41 , 42 syl 16
. . . . . . . . . . . . . . . . 17
44 30 , 43 bitr3d 255
. . . . . . . . . . . . . . . 16
45 44 ex 434
. . . . . . . . . . . . . . 15
46 28 , 45 exlimi 1912
. . . . . . . . . . . . . 14
47 22 , 46 ax-mp 5
. . . . . . . . . . . . 13
48 47 ex 434
. . . . . . . . . . . 12
49 48 adantld 467
. . . . . . . . . . 11
50 49 pm5.74d 247
. . . . . . . . . 10
51 20 , 50 imbi12d 320
. . . . . . . . 9
52 eleq1 2529
. . . . . . . . . 10
53 ovex 6324
. . . . . . . . . . . . 13
54 53 isseti 3115
. . . . . . . . . . . 12
55 eeanv 1988
. . . . . . . . . . . . 13
56 nfv 1707
. . . . . . . . . . . . . . 15
57 nfv 1707
. . . . . . . . . . . . . . . 16
58 24 , 57 nfbi 1934
. . . . . . . . . . . . . . 15
59 56 , 58 nfim 1920
. . . . . . . . . . . . . 14
60 nfv 1707
. . . . . . . . . . . . . . . 16
61 nfv 1707
. . . . . . . . . . . . . . . . 17
62 nfsbc1v 3347
. . . . . . . . . . . . . . . . 17
63 61 , 62 nfbi 1934
. . . . . . . . . . . . . . . 16
64 60 , 63 nfim 1920
. . . . . . . . . . . . . . 15
65 oveq1 6303
. . . . . . . . . . . . . . . . . . 19
66 65 oveq1d 6311
. . . . . . . . . . . . . . . . . 18
67 eqeq12 2476
. . . . . . . . . . . . . . . . . 18
68 66 , 67 syl5ibr 221
. . . . . . . . . . . . . . . . 17
69 uzindOLD.2
. . . . . . . . . . . . . . . . 17
70 68 , 69 syl6 33
. . . . . . . . . . . . . . . 16
71 sbceq1a 3338
. . . . . . . . . . . . . . . . 17
72 29 , 71 bi2bian9 875
. . . . . . . . . . . . . . . 16
73 70 , 72 sylibd 214
. . . . . . . . . . . . . . 15
74 64 , 73 exlimi 1912
. . . . . . . . . . . . . 14
75 59 , 74 exlimi 1912
. . . . . . . . . . . . 13
76 55 , 75 sylbir 213
. . . . . . . . . . . 12
77 22 , 54 , 76 mp2an 672
. . . . . . . . . . 11
78 77 imbi2d 316
. . . . . . . . . 10
79 52 , 78 imbi12d 320
. . . . . . . . 9
80 zcn 10894
. . . . . . . . . . . . . . . 16
81 subcl 9842
. . . . . . . . . . . . . . . . . . 19
82 10 , 81 mpan2 671
. . . . . . . . . . . . . . . . . 18
83 addcl 9595
. . . . . . . . . . . . . . . . . 18
84 82 , 83 sylan 471
. . . . . . . . . . . . . . . . 17
85 npcan 9852
. . . . . . . . . . . . . . . . 17
86 84 , 10 , 85 sylancl 662
. . . . . . . . . . . . . . . 16
87 80 , 35 , 86 syl2an 477
. . . . . . . . . . . . . . 15
88 87 ex 434
. . . . . . . . . . . . . 14
89 88 adantld 467
. . . . . . . . . . . . 13
90 dfsbcq 3329
. . . . . . . . . . . . 13
91 89 , 90 syl6 33
. . . . . . . . . . . 12
92 91 pm5.74d 247
. . . . . . . . . . 11
93 92 pm5.74i 245
. . . . . . . . . 10
94 eleq1 2529
. . . . . . . . . . 11
95 ovex 6324
. . . . . . . . . . . . . 14
96 95 isseti 3115
. . . . . . . . . . . . 13
97 ovex 6324
. . . . . . . . . . . . . 14
98 97 isseti 3115
. . . . . . . . . . . . 13
99 eeanv 1988
. . . . . . . . . . . . . 14
100 nfv 1707
. . . . . . . . . . . . . . . 16
101 nfsbc1v 3347
. . . . . . . . . . . . . . . . 17
102 nfv 1707
. . . . . . . . . . . . . . . . 17
103 101 , 102 nfbi 1934
. . . . . . . . . . . . . . . 16
104 100 , 103 nfim 1920
. . . . . . . . . . . . . . 15
105 nfv 1707
. . . . . . . . . . . . . . . . 17
106 nfv 1707
. . . . . . . . . . . . . . . . . 18
107 nfsbc1v 3347
. . . . . . . . . . . . . . . . . 18
108 106 , 107 nfbi 1934
. . . . . . . . . . . . . . . . 17
109 105 , 108 nfim 1920
. . . . . . . . . . . . . . . 16
110 oveq1 6303
. . . . . . . . . . . . . . . . . . . . . 22
111 110 oveq1d 6311
. . . . . . . . . . . . . . . . . . . . 21
112 111 oveq1d 6311
. . . . . . . . . . . . . . . . . . . 20
113 112 oveq1d 6311
. . . . . . . . . . . . . . . . . . 19
114 oveq1 6303
. . . . . . . . . . . . . . . . . . . 20
115 eqeq12 2476
. . . . . . . . . . . . . . . . . . . 20
116 114 , 115 sylan2 474
. . . . . . . . . . . . . . . . . . 19
117 113 , 116 syl5ibr 221
. . . . . . . . . . . . . . . . . 18
118 uzindOLD.3
. . . . . . . . . . . . . . . . . 18
119 117 , 118 syl6 33
. . . . . . . . . . . . . . . . 17
120 sbceq1a 3338
. . . . . . . . . . . . . . . . . 18
121 sbceq1a 3338
. . . . . . . . . . . . . . . . . 18
122 120 , 121 bi2bian9 875
. . . . . . . . . . . . . . . . 17
123 119 , 122 sylibd 214
. . . . . . . . . . . . . . . 16
124 109 , 123 exlimi 1912
. . . . . . . . . . . . . . 15
125 104 , 124 exlimi 1912
. . . . . . . . . . . . . 14
126 99 , 125 sylbir 213
. . . . . . . . . . . . 13
127 96 , 98 , 126 mp2an 672
. . . . . . . . . . . 12
128 127 imbi2d 316
. . . . . . . . . . 11
129 94 , 128 imbi12d 320
. . . . . . . . . 10
130 93 , 129 syl5bbr 259
. . . . . . . . 9
131 eleq1 2529
. . . . . . . . . 10
132 nfv 1707
. . . . . . . . . . . . . 14
133 nfv 1707
. . . . . . . . . . . . . . 15
134 24 , 133 nfbi 1934
. . . . . . . . . . . . . 14
135 132 , 134 nfim 1920
. . . . . . . . . . . . 13
136 29 adantr 465
. . . . . . . . . . . . . . 15
137 oveq1 6303
. . . . . . . . . . . . . . . . . . . 20
138 137 oveq1d 6311
. . . . . . . . . . . . . . . . . . 19
139 eqtr 2483
. . . . . . . . . . . . . . . . . . 19
140 138 , 139 sylan2 474
. . . . . . . . . . . . . . . . . 18
141 zcn 10894
. . . . . . . . . . . . . . . . . . 19
142 subcl 9842
. . . . . . . . . . . . . . . . . . . . . . 23
143 10 a1i 11
. . . . . . . . . . . . . . . . . . . . . . 23
144 simpr 461
. . . . . . . . . . . . . . . . . . . . . . 23
145 add32 9815
. . . . . . . . . . . . . . . . . . . . . . 23
146 142 , 143 ,
144 , 145 syl3anc 1228
. . . . . . . . . . . . . . . . . . . . . 22
147 npcan 9852
. . . . . . . . . . . . . . . . . . . . . . 23
148 147 oveq1d 6311
. . . . . . . . . . . . . . . . . . . . . 22
149 146 , 148 eqtrd 2498
. . . . . . . . . . . . . . . . . . . . 21
150 149 oveq1d 6311
. . . . . . . . . . . . . . . . . . . 20
151 peano2cn 9773
. . . . . . . . . . . . . . . . . . . . . 22
152 142 , 151 syl 16
. . . . . . . . . . . . . . . . . . . . 21
153 addsub 9854
. . . . . . . . . . . . . . . . . . . . 21
154 152 , 144 ,
143 , 153 syl3anc 1228
. . . . . . . . . . . . . . . . . . . 20
155 pncan 9849
. . . . . . . . . . . . . . . . . . . . . 22
156 10 , 155 mpan2 671
. . . . . . . . . . . . . . . . . . . . 21
157 156 adantr 465
. . . . . . . . . . . . . . . . . . . 20
158 150 , 154 ,
157 3eqtr3d 2506
. . . . . . . . . . . . . . . . . . 19
159 141 , 35 , 158 syl2an 477
. . . . . . . . . . . . . . . . . 18
160 140 , 159 sylan9eq 2518
. . . . . . . . . . . . . . . . 17
161 160 anasss 647
. . . . . . . . . . . . . . . 16
162 uzindOLD.4
. . . . . . . . . . . . . . . 16
163 161 , 162 syl 16
. . . . . . . . . . . . . . 15
164 136 , 163 bitr3d 255
. . . . . . . . . . . . . 14
165 164 ex 434
. . . . . . . . . . . . 13
166 135 , 165 exlimi 1912
. . . . . . . . . . . 12
167 22 , 166 ax-mp 5
. . . . . . . . . . 11
168 167 pm5.74da 687
. . . . . . . . . 10
169 131 , 168 imbi12d 320
. . . . . . . . 9
170 25 a1ii 27
. . . . . . . . 9
171 nnz 10911
. . . . . . . . . . 11
172 171 a1d 25
. . . . . . . . . 10
173 nfv 1707
. . . . . . . . . . . . . . . . 17
174 nfsbc1v 3347
. . . . . . . . . . . . . . . . . 18
175 62 , 174 nfim 1920
. . . . . . . . . . . . . . . . 17
176 173 , 175 nfim 1920
. . . . . . . . . . . . . . . 16
177 uzindOLD.6
. . . . . . . . . . . . . . . . 17
178 peano2zm 10932
. . . . . . . . . . . . . . . . . . . . . 22
179 zaddcl 10929
. . . . . . . . . . . . . . . . . . . . . 22
180 178 , 179 sylan 471
. . . . . . . . . . . . . . . . . . . . 21
181 171 , 180 sylan 471
. . . . . . . . . . . . . . . . . . . 20
182 simpr 461
. . . . . . . . . . . . . . . . . . . 20
183 elnnz1 10915
. . . . . . . . . . . . . . . . . . . . 21
184 zre 10893
. . . . . . . . . . . . . . . . . . . . . . . 24
185 simpr 461
. . . . . . . . . . . . . . . . . . . . . . . . . 26
186 peano2rem 9909
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
187 readdcl 9596
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
188 186 , 187 sylan 471
. . . . . . . . . . . . . . . . . . . . . . . . . 26
189 peano2rem 9909
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
190 189 adantl 466
. . . . . . . . . . . . . . . . . . . . . . . . . 26
191 lesub1 10071
. . . . . . . . . . . . . . . . . . . . . . . . . 26
192 185 , 188 ,
190 , 191 syl3anc 1228
. . . . . . . . . . . . . . . . . . . . . . . . 25
193 recn 9603
. . . . . . . . . . . . . . . . . . . . . . . . . 26
194 recn 9603
. . . . . . . . . . . . . . . . . . . . . . . . . 26
195 subsub 9872
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
196 10 , 195 mp3an3 1313
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
197 196 anidms 645
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
198 subid 9861
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
199 198 oveq1d 6311
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
200 199 , 11 syl6eq 2514
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
201 197 , 200 eqtrd 2498
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202 201 adantl 466
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
203 subcl 9842
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
204 10 , 203 mpan2 671
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
205 addcl 9595
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
206 204 , 205 sylan 471
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
207 subsub 9872
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
208 10 , 207 mp3an3 1313
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
209 206 , 208 sylancom 667
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
210 pncan 9849
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
211 204 , 210 sylan 471
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
212 211 oveq1d 6311
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
213 npcan 9852
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
214 10 , 213 mpan2 671
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
215 214 adantr 465
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
216 209 , 212 ,
215 3eqtrd 2502
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
217 202 , 216 breq12d 4465
. . . . . . . . . . . . . . . . . . . . . . . . . 26
218 193 , 194 ,
217 syl2an 477
. . . . . . . . . . . . . . . . . . . . . . . . 25
219 192 , 218 bitrd 253
. . . . . . . . . . . . . . . . . . . . . . . 24
220 184 , 2 , 219 syl2an 477
. . . . . . . . . . . . . . . . . . . . . . 23
221 220 biimpar 485
. . . . . . . . . . . . . . . . . . . . . 22
222 221 an32s 804
. . . . . . . . . . . . . . . . . . . . 21
223 183 , 222 sylanb 472
. . . . . . . . . . . . . . . . . . . 20
224 181 , 182 ,
223 jca31 534
. . . . . . . . . . . . . . . . . . 19
225 eleq1 2529
. . . . . . . . . . . . . . . . . . . . 21
226 225 anbi1d 704
. . . . . . . . . . . . . . . . . . . 20
227 breq2 4456
. . . . . . . . . . . . . . . . . . . 20
228 226 , 227 anbi12d 710
. . . . . . . . . . . . . . . . . . 19
229 224 , 228 syl5ibr 221
. . . . . . . . . . . . . . . . . 18
230 sbceq1a 3338
. . . . . . . . . . . . . . . . . . . 20
231 71 , 230 imbi12d 320
. . . . . . . . . . . . . . . . . . 19
232 231 biimpd 207
. . . . . . . . . . . . . . . . . 18
233 229 , 232 imim12d 74
. . . . . . . . . . . . . . . . 17
234 177 , 233 mpi 17
. . . . . . . . . . . . . . . 16
235 176 , 234 exlimi 1912
. . . . . . . . . . . . . . 15