Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uzindOLD Unicode version

Theorem uzindOLD 10982
 Description: Induction on the upper integers that start at an integer . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Warning: The HTML proof page is 3/4 megabyte in size. An attempt to shorten it is on my to-do list. Anyone is welcome to try. (Contributed by NM, 11-May-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
uzindOLD.1
uzindOLD.2
uzindOLD.3
uzindOLD.4
uzindOLD.5
uzindOLD.6
Assertion
Ref Expression
uzindOLD
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,,

Proof of Theorem uzindOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef 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
85, 6, 7mp3an13 1315 . . . . . . 7
94, 8syl 16 . . . . . 6
10 ax-1cn 9571 . . . . . . . 8
1110addid2i 9789 . . . . . . 7
1211breq1i 4459 . . . . . 6
139, 12syl6bb 261 . . . . 5
143, 13bitr3d 255 . . . 4
151, 2, 14syl2an 477 . . 3
16 zsubcl 10931 . . . . 5
17 peano2z 10930 . . . . 5
1816, 17syl 16 . . . 4
19 elnnz1 10915 . . . . . . . 8
20 eleq1 2529 . . . . . . . . . 10
21 ovex 6324 . . . . . . . . . . . . . . 15
2221isseti 3115 . . . . . . . . . . . . . 14
23 nfv 1707 . . . . . . . . . . . . . . . 16
24 nfsbc1v 3347 . . . . . . . . . . . . . . . . 17
25 uzindOLD.5 . . . . . . . . . . . . . . . . . 18
2625nfth 1625 . . . . . . . . . . . . . . . . 17
2724, 26nfbi 1934 . . . . . . . . . . . . . . . 16
2823, 27nfim 1920 . . . . . . . . . . . . . . 15
29 sbceq1a 3338 . . . . . . . . . . . . . . . . . 18
3029adantr 465 . . . . . . . . . . . . . . . . 17
31 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
3231oveq1d 6311 . . . . . . . . . . . . . . . . . . . 20
3310subidi 9913 . . . . . . . . . . . . . . . . . . . . . 22
3433oveq1i 6306 . . . . . . . . . . . . . . . . . . . . 21
35 zcn 10894 . . . . . . . . . . . . . . . . . . . . . 22
36 addid2 9784 . . . . . . . . . . . . . . . . . . . . . 22
3735, 36syl 16 . . . . . . . . . . . . . . . . . . . . 21
3834, 37syl5eq 2510 . . . . . . . . . . . . . . . . . . . 20
3932, 38sylan9eq 2518 . . . . . . . . . . . . . . . . . . 19
40 eqtr 2483 . . . . . . . . . . . . . . . . . . 19
4139, 40sylan2 474 . . . . . . . . . . . . . . . . . 18
42 uzindOLD.1 . . . . . . . . . . . . . . . . . 18
4341, 42syl 16 . . . . . . . . . . . . . . . . 17
4430, 43bitr3d 255 . . . . . . . . . . . . . . . 16
4544ex 434 . . . . . . . . . . . . . . 15
4628, 45exlimi 1912 . . . . . . . . . . . . . 14
4722, 46ax-mp 5 . . . . . . . . . . . . 13
4847ex 434 . . . . . . . . . . . 12
4948adantld 467 . . . . . . . . . . 11
5049pm5.74d 247 . . . . . . . . . 10
5120, 50imbi12d 320 . . . . . . . . 9
52 eleq1 2529 . . . . . . . . . 10
53 ovex 6324 . . . . . . . . . . . . 13
5453isseti 3115 . . . . . . . . . . . 12
55 eeanv 1988 . . . . . . . . . . . . 13
56 nfv 1707 . . . . . . . . . . . . . . 15
57 nfv 1707 . . . . . . . . . . . . . . . 16
5824, 57nfbi 1934 . . . . . . . . . . . . . . 15
5956, 58nfim 1920 . . . . . . . . . . . . . 14
60 nfv 1707 . . . . . . . . . . . . . . . 16
61 nfv 1707 . . . . . . . . . . . . . . . . 17
62 nfsbc1v 3347 . . . . . . . . . . . . . . . . 17
6361, 62nfbi 1934 . . . . . . . . . . . . . . . 16
6460, 63nfim 1920 . . . . . . . . . . . . . . 15
65 oveq1 6303 . . . . . . . . . . . . . . . . . . 19
6665oveq1d 6311 . . . . . . . . . . . . . . . . . 18
67 eqeq12 2476 . . . . . . . . . . . . . . . . . 18
6866, 67syl5ibr 221 . . . . . . . . . . . . . . . . 17
69 uzindOLD.2 . . . . . . . . . . . . . . . . 17
7068, 69syl6 33 . . . . . . . . . . . . . . . 16
71 sbceq1a 3338 . . . . . . . . . . . . . . . . 17
7229, 71bi2bian9 875 . . . . . . . . . . . . . . . 16
7370, 72sylibd 214 . . . . . . . . . . . . . . 15
7464, 73exlimi 1912 . . . . . . . . . . . . . 14
7559, 74exlimi 1912 . . . . . . . . . . . . 13
7655, 75sylbir 213 . . . . . . . . . . . 12
7722, 54, 76mp2an 672 . . . . . . . . . . 11
7877imbi2d 316 . . . . . . . . . 10
7952, 78imbi12d 320 . . . . . . . . 9
80 zcn 10894 . . . . . . . . . . . . . . . 16
81 subcl 9842 . . . . . . . . . . . . . . . . . . 19
8210, 81mpan2 671 . . . . . . . . . . . . . . . . . 18
83 addcl 9595 . . . . . . . . . . . . . . . . . 18
8482, 83sylan 471 . . . . . . . . . . . . . . . . 17
85 npcan 9852 . . . . . . . . . . . . . . . . 17
8684, 10, 85sylancl 662 . . . . . . . . . . . . . . . 16
8780, 35, 86syl2an 477 . . . . . . . . . . . . . . 15
8887ex 434 . . . . . . . . . . . . . 14
8988adantld 467 . . . . . . . . . . . . 13
90 dfsbcq 3329 . . . . . . . . . . . . 13
9189, 90syl6 33 . . . . . . . . . . . 12
9291pm5.74d 247 . . . . . . . . . . 11
9392pm5.74i 245 . . . . . . . . . 10
94 eleq1 2529 . . . . . . . . . . 11
95 ovex 6324 . . . . . . . . . . . . . 14
9695isseti 3115 . . . . . . . . . . . . 13
97 ovex 6324 . . . . . . . . . . . . . 14
9897isseti 3115 . . . . . . . . . . . . 13
99 eeanv 1988 . . . . . . . . . . . . . 14
100 nfv 1707 . . . . . . . . . . . . . . . 16
101 nfsbc1v 3347 . . . . . . . . . . . . . . . . 17
102 nfv 1707 . . . . . . . . . . . . . . . . 17
103101, 102nfbi 1934 . . . . . . . . . . . . . . . 16
104100, 103nfim 1920 . . . . . . . . . . . . . . 15
105 nfv 1707 . . . . . . . . . . . . . . . . 17
106 nfv 1707 . . . . . . . . . . . . . . . . . 18
107 nfsbc1v 3347 . . . . . . . . . . . . . . . . . 18
108106, 107nfbi 1934 . . . . . . . . . . . . . . . . 17
109105, 108nfim 1920 . . . . . . . . . . . . . . . 16
110 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . 22
111110oveq1d 6311 . . . . . . . . . . . . . . . . . . . . 21
112111oveq1d 6311 . . . . . . . . . . . . . . . . . . . 20
113112oveq1d 6311 . . . . . . . . . . . . . . . . . . 19
114 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
115 eqeq12 2476 . . . . . . . . . . . . . . . . . . . 20
116114, 115sylan2 474 . . . . . . . . . . . . . . . . . . 19
117113, 116syl5ibr 221 . . . . . . . . . . . . . . . . . 18
118 uzindOLD.3 . . . . . . . . . . . . . . . . . 18
119117, 118syl6 33 . . . . . . . . . . . . . . . . 17
120 sbceq1a 3338 . . . . . . . . . . . . . . . . . 18
121 sbceq1a 3338 . . . . . . . . . . . . . . . . . 18
122120, 121bi2bian9 875 . . . . . . . . . . . . . . . . 17
123119, 122sylibd 214 . . . . . . . . . . . . . . . 16
124109, 123exlimi 1912 . . . . . . . . . . . . . . 15
125104, 124exlimi 1912 . . . . . . . . . . . . . 14
12699, 125sylbir 213 . . . . . . . . . . . . 13
12796, 98, 126mp2an 672 . . . . . . . . . . . 12
128127imbi2d 316 . . . . . . . . . . 11
12994, 128imbi12d 320 . . . . . . . . . 10
13093, 129syl5bbr 259 . . . . . . . . 9
131 eleq1 2529 . . . . . . . . . 10
132 nfv 1707 . . . . . . . . . . . . . 14
133 nfv 1707 . . . . . . . . . . . . . . 15
13424, 133nfbi 1934 . . . . . . . . . . . . . 14
135132, 134nfim 1920 . . . . . . . . . . . . 13
13629adantr 465 . . . . . . . . . . . . . . 15
137 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
138137oveq1d 6311 . . . . . . . . . . . . . . . . . . 19
139 eqtr 2483 . . . . . . . . . . . . . . . . . . 19
140138, 139sylan2 474 . . . . . . . . . . . . . . . . . 18
141 zcn 10894 . . . . . . . . . . . . . . . . . . 19
142 subcl 9842 . . . . . . . . . . . . . . . . . . . . . . 23
14310a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
144 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23
145 add32 9815 . . . . . . . . . . . . . . . . . . . . . . 23
146142, 143, 144, 145syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22
147 npcan 9852 . . . . . . . . . . . . . . . . . . . . . . 23
148147oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . 22
149146, 148eqtrd 2498 . . . . . . . . . . . . . . . . . . . . 21
150149oveq1d 6311 . . . . . . . . . . . . . . . . . . . 20
151 peano2cn 9773 . . . . . . . . . . . . . . . . . . . . . 22
152142, 151syl 16 . . . . . . . . . . . . . . . . . . . . 21
153 addsub 9854 . . . . . . . . . . . . . . . . . . . . 21
154152, 144, 143, 153syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20
155 pncan 9849 . . . . . . . . . . . . . . . . . . . . . 22
15610, 155mpan2 671 . . . . . . . . . . . . . . . . . . . . 21
157156adantr 465 . . . . . . . . . . . . . . . . . . . 20
158150, 154, 1573eqtr3d 2506 . . . . . . . . . . . . . . . . . . 19
159141, 35, 158syl2an 477 . . . . . . . . . . . . . . . . . 18
160140, 159sylan9eq 2518 . . . . . . . . . . . . . . . . 17
161160anasss 647 . . . . . . . . . . . . . . . 16
162 uzindOLD.4 . . . . . . . . . . . . . . . 16
163161, 162syl 16 . . . . . . . . . . . . . . 15
164136, 163bitr3d 255 . . . . . . . . . . . . . 14
165164ex 434 . . . . . . . . . . . . 13
166135, 165exlimi 1912 . . . . . . . . . . . 12
16722, 166ax-mp 5 . . . . . . . . . . 11
168167pm5.74da 687 . . . . . . . . . 10
169131, 168imbi12d 320 . . . . . . . . 9
17025a1ii 27 . . . . . . . . 9
171 nnz 10911 . . . . . . . . . . 11
172171a1d 25 . . . . . . . . . 10
173 nfv 1707 . . . . . . . . . . . . . . . . 17
174 nfsbc1v 3347 . . . . . . . . . . . . . . . . . 18
17562, 174nfim 1920 . . . . . . . . . . . . . . . . 17
176173, 175nfim 1920 . . . . . . . . . . . . . . . 16
177 uzindOLD.6 . . . . . . . . . . . . . . . . 17
178 peano2zm 10932 . . . . . . . . . . . . . . . . . . . . . 22
179 zaddcl 10929 . . . . . . . . . . . . . . . . . . . . . 22
180178, 179sylan 471 . . . . . . . . . . . . . . . . . . . . 21
181171, 180sylan 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
188186, 187sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189 peano2rem 9909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
190189adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
191 lesub1 10071 . . . . . . . . . . . . . . . . . . . . . . . . . 26
192185, 188, 190, 191syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
193 recn 9603 . . . . . . . . . . . . . . . . . . . . . . . . . 26
194 recn 9603 . . . . . . . . . . . . . . . . . . . . . . . . . 26
195 subsub 9872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
19610, 195mp3an3 1313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
197196anidms 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
198 subid 9861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
199198oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
200199, 11syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
201197, 200eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202201adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
203 subcl 9842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
20410, 203mpan2 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
205 addcl 9595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
206204, 205sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
207 subsub 9872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
20810, 207mp3an3 1313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
209206, 208sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
210 pncan 9849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
211204, 210sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
212211oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
213 npcan 9852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
21410, 213mpan2 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
215214adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
216209, 212, 2153eqtrd 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
217202, 216breq12d 4465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
218193, 194, 217syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . 25
219192, 218bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . 24
220184, 2, 219syl2an 477 . . . . . . . . . . . . . . . . . . . . . . 23
221220biimpar 485 . . . . . . . . . . . . . . . . . . . . . 22
222221an32s 804 . . . . . . . . . . . . . . . . . . . . 21
223183, 222sylanb 472 . . . . . . . . . . . . . . . . . . . 20
224181, 182, 223jca31 534 . . . . . . . . . . . . . . . . . . 19
225 eleq1 2529 . . . . . . . . . . . . . . . . . . . . 21
226225anbi1d 704 . . . . . . . . . . . . . . . . . . . 20
227 breq2 4456 . . . . . . . . . . . . . . . . . . . 20
228226, 227anbi12d 710 . . . . . . . . . . . . . . . . . . 19
229224, 228syl5ibr 221 . . . . . . . . . . . . . . . . . 18
230 sbceq1a 3338 . . . . . . . . . . . . . . . . . . . 20
23171, 230imbi12d 320 . . . . . . . . . . . . . . . . . . 19
232231biimpd 207 . . . . . . . . . . . . . . . . . 18
233229, 232imim12d 74 . . . . . . . . . . . . . . . . 17
234177, 233mpi 17 . . . . . . . . . . . . . . . 16
235176, 234exlimi 1912 . . . . . . . . . . . . . . 15