Step | Hyp | Ref
| Expression |
1 | | nnsucelrlem1 4424 |
. . . 4
1c
|
2 | | addceq1 4383 |
. . . . . . . . . 10
0c
1c
0c 1c |
3 | | addcid2 4407 |
. . . . . . . . . 10
0c
1c
1c |
4 | 2, 3 | syl6eq 2401 |
. . . . . . . . 9
0c
1c
1c |
5 | 4 | eleq2d 2420 |
. . . . . . . 8
0c
1c
1c |
6 | | el1c 4139 |
. . . . . . . 8
1c
|
7 | 5, 6 | syl6bb 252 |
. . . . . . 7
0c
1c
|
8 | 7 | anbi2d 684 |
. . . . . 6
0c
1c
|
9 | | eleq2 2414 |
. . . . . . 7
0c
0c |
10 | | df-0c 4377 |
. . . . . . . . 9
0c
|
11 | 10 | eleq2i 2417 |
. . . . . . . 8
0c
|
12 | | vex 2862 |
. . . . . . . . 9
|
13 | 12 | elsnc 3756 |
. . . . . . . 8
|
14 | 11, 13 | bitri 240 |
. . . . . . 7
0c
|
15 | 9, 14 | syl6bb 252 |
. . . . . 6
0c
|
16 | 8, 15 | imbi12d 311 |
. . . . 5
0c
1c
|
17 | 16 | 2albidv 1627 |
. . . 4
0c
1c
|
18 | | addceq1 4383 |
. . . . . . . . 9
1c 1c |
19 | 18 | eleq2d 2420 |
. . . . . . . 8
1c
1c |
20 | 19 | anbi2d 684 |
. . . . . . 7
1c
1c |
21 | | eleq2 2414 |
. . . . . . 7
|
22 | 20, 21 | imbi12d 311 |
. . . . . 6
1c
1c |
23 | 22 | 2albidv 1627 |
. . . . 5
1c
1c |
24 | | eleq12 2415 |
. . . . . . . . . 10
|
25 | 24 | ancoms 439 |
. . . . . . . . 9
|
26 | 25 | notbid 285 |
. . . . . . . 8
|
27 | | sneq 3744 |
. . . . . . . . . 10
|
28 | | uneq12 3413 |
. . . . . . . . . 10
|
29 | 27, 28 | sylan2 460 |
. . . . . . . . 9
|
30 | 29 | eleq1d 2419 |
. . . . . . . 8
1c
1c |
31 | 26, 30 | anbi12d 691 |
. . . . . . 7
1c
1c |
32 | | eleq1 2413 |
. . . . . . . 8
|
33 | 32 | adantr 451 |
. . . . . . 7
|
34 | 31, 33 | imbi12d 311 |
. . . . . 6
1c
1c |
35 | 34 | cbval2v 2006 |
. . . . 5
1c
1c |
36 | 23, 35 | syl6bb 252 |
. . . 4
1c
1c |
37 | | addceq1 4383 |
. . . . . . . 8
1c
1c
1c
1c |
38 | 37 | eleq2d 2420 |
. . . . . . 7
1c
1c
1c 1c |
39 | 38 | anbi2d 684 |
. . . . . 6
1c
1c
1c
1c |
40 | | eleq2 2414 |
. . . . . 6
1c
1c |
41 | 39, 40 | imbi12d 311 |
. . . . 5
1c
1c
1c
1c
1c |
42 | 41 | 2albidv 1627 |
. . . 4
1c
1c
1c
1c
1c |
43 | | addceq1 4383 |
. . . . . . . 8
1c 1c |
44 | 43 | eleq2d 2420 |
. . . . . . 7
1c
1c |
45 | 44 | anbi2d 684 |
. . . . . 6
1c
1c |
46 | | eleq2 2414 |
. . . . . 6
|
47 | 45, 46 | imbi12d 311 |
. . . . 5
1c
1c |
48 | 47 | 2albidv 1627 |
. . . 4
1c
1c |
49 | | vex 2862 |
. . . . . . . . . . 11
|
50 | 49 | unsneqsn 3887 |
. . . . . . . . . 10
|
51 | 50 | ord 366 |
. . . . . . . . 9
|
52 | 49 | snid 3760 |
. . . . . . . . . 10
|
53 | | eleq2 2414 |
. . . . . . . . . 10
|
54 | 52, 53 | mpbiri 224 |
. . . . . . . . 9
|
55 | 51, 54 | syl6 29 |
. . . . . . . 8
|
56 | 55 | con1d 116 |
. . . . . . 7
|
57 | 56 | exlimiv 1634 |
. . . . . 6
|
58 | 57 | impcom 419 |
. . . . 5
|
59 | 58 | gen2 1547 |
. . . 4
|
60 | | elsuc 4413 |
. . . . . . . . 9
1c
1c
1c ∼ |
61 | | vex 2862 |
. . . . . . . . . . . . 13
|
62 | 61 | elcompl 3225 |
. . . . . . . . . . . 12
∼ |
63 | 62 | anbi2i 675 |
. . . . . . . . . . 11
1c ∼
1c
|
64 | | simprrl 740 |
. . . . . . . . . . . . . . . . . . 19
1c
|
65 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 65 | adantr 451 |
. . . . . . . . . . . . . . . . . . 19
1c
|
67 | 64, 66 | difeq12d 3386 |
. . . . . . . . . . . . . . . . . 18
1c
|
68 | | simprrr 741 |
. . . . . . . . . . . . . . . . . . 19
1c
|
69 | | nnsucelrlem2 4425 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 68, 69 | syl 15 |
. . . . . . . . . . . . . . . . . 18
1c
|
71 | | simprlr 739 |
. . . . . . . . . . . . . . . . . . 19
1c
|
72 | | nnsucelrlem2 4425 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 71, 72 | syl 15 |
. . . . . . . . . . . . . . . . . 18
1c
|
74 | 67, 70, 73 | 3eqtr3d 2393 |
. . . . . . . . . . . . . . . . 17
1c
|
75 | | simprll 738 |
. . . . . . . . . . . . . . . . 17
1c
1c |
76 | 74, 75 | eqeltrd 2427 |
. . . . . . . . . . . . . . . 16
1c
1c |
77 | 76 | 3adantr1 1114 |
. . . . . . . . . . . . . . 15
1c
1c
1c |
78 | 77 | ex 423 |
. . . . . . . . . . . . . 14
1c
1c
1c |
79 | | simpl 443 |
. . . . . . . . . . . . . . . . 17
1c
1c
|
80 | | simpr3l 1016 |
. . . . . . . . . . . . . . . . 17
1c
1c
|
81 | | simpr2r 1015 |
. . . . . . . . . . . . . . . . 17
1c
1c
|
82 | 49 | nnsucelrlem3 4426 |
. . . . . . . . . . . . . . . . 17
|
83 | 79, 80, 81, 82 | syl3anc 1182 |
. . . . . . . . . . . . . . . 16
1c
1c
|
84 | | simp22r 1075 |
. . . . . . . . . . . . . . . . . . 19
1c
1c
|
85 | | difsn 3845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
86 | 85 | uneq1d 3417 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 86 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 88 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . 20
1c
1c
|
90 | | simp23l 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
1c
|
91 | 90 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c
|
92 | 61 | snss 3838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
93 | | ssequn2 3436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 92, 93 | bitr2i 241 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 94 | biimpi 186 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | 95 | eqcoms 2356 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 91, 96 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . . 20
1c
1c
|
98 | 89, 97 | syld 40 |
. . . . . . . . . . . . . . . . . . 19
1c
1c
|
99 | 84, 98 | mt3d 117 |
. . . . . . . . . . . . . . . . . 18
1c
1c
|
100 | | nnsucelrlem4 4427 |
. . . . . . . . . . . . . . . . . 18
|
101 | 99, 100 | syl 15 |
. . . . . . . . . . . . . . . . 17
1c
1c
|
102 | | simpl3r 1011 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c
|
103 | | difss 3393 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 103 | sseli 3269 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 102, 104 | nsyl 113 |
. . . . . . . . . . . . . . . . . . . 20
1c
1c
|
106 | | simp2l 981 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c
1c |
107 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
1c |
108 | 107 | biimpd 198 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c |
109 | 106, 108 | mpan9 455 |
. . . . . . . . . . . . . . . . . . . 20
1c
1c
1c |
110 | | simpl1 958 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c
1c |
111 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
112 | 12, 111 | difex 4107 |
. . . . . . . . . . . . . . . . . . . . . 22
|
113 | | eleq12 2415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
114 | 113 | ancoms 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
115 | 114 | notbid 285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
116 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
117 | | uneq12 3413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
118 | 116, 117 | sylan2 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
119 | 118 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
1c
1c |
120 | 115, 119 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1c
1c |
121 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
122 | 121 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
123 | 120, 122 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . 23
1c
1c
|
124 | 123 | spc2gv 2942 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
1c
|
125 | 112, 49, 124 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c
|
126 | 110, 125 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
1c
1c
1c
|
127 | 105, 109,
126 | mp2and 660 |
. . . . . . . . . . . . . . . . . . 19
1c
1c
|
128 | 127 | 3adant1 973 |
. . . . . . . . . . . . . . . . . 18
1c
1c
|
129 | 61 | snid 3760 |
. . . . . . . . . . . . . . . . . . . . 21
|
130 | | eldif 3221 |
. . . . . . . . . . . . . . . . . . . . . 22
|
131 | 130 | simprbi 450 |
. . . . . . . . . . . . . . . . . . . . 21
|
132 | 129, 131 | mt2 170 |
. . . . . . . . . . . . . . . . . . . 20
|
133 | 61 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . 20
∼ |
134 | 132, 133 | mpbir 200 |
. . . . . . . . . . . . . . . . . . 19
∼
|
135 | | eqid 2353 |
. . . . . . . . . . . . . . . . . . 19
|
136 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . . . 22
|
137 | 136 | uneq2d 3418 |
. . . . . . . . . . . . . . . . . . . . 21
|
138 | 137 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . 20
|
139 | 138 | rspcev 2955 |
. . . . . . . . . . . . . . . . . . 19
∼
∼ |
140 | 134, 135,
139 | mp2an 653 |
. . . . . . . . . . . . . . . . . 18
∼
|
141 | | compleq 3243 |
. . . . . . . . . . . . . . . . . . . . 21
∼
∼ |
142 | | uneq1 3411 |
. . . . . . . . . . . . . . . . . . . . . 22
|
143 | 142 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
|
144 | 141, 143 | rexeqbidv 2820 |
. . . . . . . . . . . . . . . . . . . 20
∼
∼
|
145 | 144 | rspcev 2955 |
. . . . . . . . . . . . . . . . . . 19
∼
∼ |
146 | | elsuc 4413 |
. . . . . . . . . . . . . . . . . . 19
1c
∼ |
147 | 145, 146 | sylibr 203 |
. . . . . . . . . . . . . . . . . 18
∼
1c |
148 | 128, 140,
147 | sylancl 643 |
. . . . . . . . . . . . . . . . 17
1c
1c
1c |
149 | 101, 148 | eqeltrrd 2428 |
. . . . . . . . . . . . . . . 16
1c
1c
1c |
150 | 83, 149 | mpd3an3 1278 |
. . . . . . . . . . . . . . 15
1c
1c
1c |
151 | 150 | ex 423 |
. . . . . . . . . . . . . 14
1c
1c
1c |
152 | 78, 151 | pm2.61ine 2592 |
. . . . . . . . . . . . 13
1c
1c
1c |
153 | 152 | 3expa 1151 |
. . . . . . . . . . . 12
1c
1c
1c |
154 | 153 | exp32 588 |
. . . . . . . . . . 11
1c
1c
1c |
155 | 63, 154 | sylan2b 461 |
. . . . . . . . . 10
1c
1c ∼
1c |
156 | 155 | rexlimdvva 2745 |
. . . . . . . . 9
1c
1c ∼
1c |
157 | 60, 156 | syl5bi 208 |
. . . . . . . 8
1c
1c
1c
1c |
158 | 157 | com23 72 |
. . . . . . 7
1c
1c 1c
1c |
159 | 158 | imp3a 420 |
. . . . . 6
1c
1c
1c
1c |
160 | 159 | alrimivv 1632 |
. . . . 5
1c
1c
1c
1c |
161 | 160 | a1i 10 |
. . . 4
Nn
1c
1c
1c
1c |
162 | 1, 17, 36, 42, 48, 59, 161 | finds 4411 |
. . 3
Nn
1c
|
163 | | nnsucelr.2 |
. . . . 5
|
164 | | eleq1 2413 |
. . . . . . . 8
|
165 | 164 | notbid 285 |
. . . . . . 7
|
166 | | sneq 3744 |
. . . . . . . . 9
|
167 | 166 | uneq2d 3418 |
. . . . . . . 8
|
168 | 167 | eleq1d 2419 |
. . . . . . 7
1c
1c |
169 | 165, 168 | anbi12d 691 |
. . . . . 6
1c
1c |
170 | 169 | imbi1d 308 |
. . . . 5
1c
1c |
171 | 163, 170 | spcv 2945 |
. . . 4
1c
1c |
172 | 171 | alimi 1559 |
. . 3
1c
1c
|
173 | | nnsucelr.1 |
. . . 4
|
174 | | eleq2 2414 |
. . . . . . 7
|
175 | 174 | notbid 285 |
. . . . . 6
|
176 | | uneq1 3411 |
. . . . . . 7
|
177 | 176 | eleq1d 2419 |
. . . . . 6
1c
1c |
178 | 175, 177 | anbi12d 691 |
. . . . 5
1c
1c |
179 | | eleq1 2413 |
. . . . 5
|
180 | 178, 179 | imbi12d 311 |
. . . 4
1c
1c |
181 | 173, 180 | spcv 2945 |
. . 3
1c
1c |
182 | 162, 172,
181 | 3syl 18 |
. 2
Nn
1c
|
183 | 182 | imp 418 |
1
Nn
1c |