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
