Step | Hyp | Ref
| Expression |
1 | | vex 2738 |
. . . . . . . . . 10
|
2 | | vex 2738 |
. . . . . . . . . 10
|
3 | | eleq1 2238 |
. . . . . . . . . . . 12
|
4 | 3 | anbi1d 465 |
. . . . . . . . . . 11
|
5 | | eqeq1 2182 |
. . . . . . . . . . . . . 14
|
6 | 5 | anbi1d 465 |
. . . . . . . . . . . . 13
|
7 | 6 | anbi1d 465 |
. . . . . . . . . . . 12
|
8 | 7 | 4exbidv 1868 |
. . . . . . . . . . 11
|
9 | 4, 8 | anbi12d 473 |
. . . . . . . . . 10
|
10 | | eleq1 2238 |
. . . . . . . . . . . 12
|
11 | 10 | anbi2d 464 |
. . . . . . . . . . 11
|
12 | | eqeq1 2182 |
. . . . . . . . . . . . . 14
|
13 | 12 | anbi2d 464 |
. . . . . . . . . . . . 13
|
14 | 13 | anbi1d 465 |
. . . . . . . . . . . 12
|
15 | 14 | 4exbidv 1868 |
. . . . . . . . . . 11
|
16 | 11, 15 | anbi12d 473 |
. . . . . . . . . 10
|
17 | | df-enq0 7398 |
. . . . . . . . . 10
~Q0
|
18 | 1, 2, 9, 16, 17 | brab 4266 |
. . . . . . . . 9
~Q0
|
19 | | vex 2738 |
. . . . . . . . . 10
|
20 | | eleq1 2238 |
. . . . . . . . . . . 12
|
21 | 20 | anbi1d 465 |
. . . . . . . . . . 11
|
22 | | eqeq1 2182 |
. . . . . . . . . . . . . 14
|
23 | 22 | anbi1d 465 |
. . . . . . . . . . . . 13
|
24 | 23 | anbi1d 465 |
. . . . . . . . . . . 12
|
25 | 24 | 4exbidv 1868 |
. . . . . . . . . . 11
|
26 | 21, 25 | anbi12d 473 |
. . . . . . . . . 10
|
27 | | eleq1 2238 |
. . . . . . . . . . . 12
|
28 | 27 | anbi2d 464 |
. . . . . . . . . . 11
|
29 | | eqeq1 2182 |
. . . . . . . . . . . . . 14
|
30 | 29 | anbi2d 464 |
. . . . . . . . . . . . 13
|
31 | 30 | anbi1d 465 |
. . . . . . . . . . . 12
|
32 | 31 | 4exbidv 1868 |
. . . . . . . . . . 11
|
33 | 28, 32 | anbi12d 473 |
. . . . . . . . . 10
|
34 | | df-enq0 7398 |
. . . . . . . . . 10
~Q0
|
35 | 2, 19, 26, 33, 34 | brab 4266 |
. . . . . . . . 9
~Q0
|
36 | 18, 35 | anbi12i 460 |
. . . . . . . 8
~Q0
~Q0
|
37 | 36 | biimpi 120 |
. . . . . . 7
~Q0
~Q0
|
38 | | an4 586 |
. . . . . . 7
|
39 | 37, 38 | sylib 122 |
. . . . . 6
~Q0
~Q0
|
40 | | 3anass 982 |
. . . . . . . 8
|
41 | | anass 401 |
. . . . . . . . 9
|
42 | | anass 401 |
. . . . . . . . . 10
|
43 | 42 | anbi2i 457 |
. . . . . . . . 9
|
44 | | anidm 396 |
. . . . . . . . . . 11
|
45 | 44 | anbi1i 458 |
. . . . . . . . . 10
|
46 | 45 | anbi2i 457 |
. . . . . . . . 9
|
47 | 41, 43, 46 | 3bitr2i 208 |
. . . . . . . 8
|
48 | 40, 47 | bitr4i 187 |
. . . . . . 7
|
49 | 48 | anbi1i 458 |
. . . . . 6
|
50 | 39, 49 | sylibr 134 |
. . . . 5
~Q0
~Q0
|
51 | | ee8anv 1933 |
. . . . . 6
|
52 | 51 | anbi2i 457 |
. . . . 5
|
53 | 50, 52 | sylibr 134 |
. . . 4
~Q0
~Q0
|
54 | | 19.42vvvv 1911 |
. . . . . . 7
|
55 | 54 | 2exbii 1604 |
. . . . . 6
|
56 | 55 | 2exbii 1604 |
. . . . 5
|
57 | | 19.42vvvv 1911 |
. . . . 5
|
58 | 56, 57 | bitri 184 |
. . . 4
|
59 | 53, 58 | sylibr 134 |
. . 3
~Q0
~Q0
|
60 | | 3simpb 995 |
. . . . . . . . 9
|
61 | 60 | adantr 276 |
. . . . . . . 8
|
62 | | simplll 533 |
. . . . . . . . . 10
|
63 | | simprlr 538 |
. . . . . . . . . 10
|
64 | 62, 63 | jca 306 |
. . . . . . . . 9
|
65 | 64 | adantl 277 |
. . . . . . . 8
|
66 | | oveq1 5872 |
. . . . . . . . . . . . . . . 16
|
67 | 63 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | | simpl3 1002 |
. . . . . . . . . . . . . . . . . . . . . 22
|
69 | 67, 68 | eqeltrrd 2253 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | | opelxp 4650 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 69, 70 | sylib 122 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | simprd 114 |
. . . . . . . . . . . . . . . . . . 19
|
73 | | pinn 7283 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
|
75 | | nnm0r 6470 |
. . . . . . . . . . . . . . . . . 18
|
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | eqeq2d 2187 |
. . . . . . . . . . . . . . . 16
|
78 | 66, 77 | syl5ib 154 |
. . . . . . . . . . . . . . 15
|
79 | | simprr 531 |
. . . . . . . . . . . . . . . . . 18
|
80 | | eqtr2 2194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | | vex 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
82 | | vex 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 81, 82 | opth 4231 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 80, 83 | sylib 122 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | | oveq1 5872 |
. . . . . . . . . . . . . . . . . . . . . 22
|
86 | | oveq1 5872 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 85, 86 | eqeqan12d 2191 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 84, 87 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | ad2ant2lr 510 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 89 | ad2ant2r 509 |
. . . . . . . . . . . . . . . . . 18
|
91 | 79, 90 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
|
92 | 91 | eqeq1d 2184 |
. . . . . . . . . . . . . . . 16
|
93 | 92 | adantl 277 |
. . . . . . . . . . . . . . 15
|
94 | 78, 93 | sylibd 149 |
. . . . . . . . . . . . . 14
|
95 | | simpllr 534 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 95 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
|
97 | | simpl2 1001 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 96, 97 | eqeltrrd 2253 |
. . . . . . . . . . . . . . . . . 18
|
99 | | opelxp 4650 |
. . . . . . . . . . . . . . . . . 18
|
100 | 98, 99 | sylib 122 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | simprd 114 |
. . . . . . . . . . . . . . . 16
|
102 | | pinn 7283 |
. . . . . . . . . . . . . . . 16
|
103 | 101, 102 | syl 14 |
. . . . . . . . . . . . . . 15
|
104 | 71 | simpld 112 |
. . . . . . . . . . . . . . 15
|
105 | | nnm00 6521 |
. . . . . . . . . . . . . . 15
|
106 | 103, 104,
105 | syl2anc 411 |
. . . . . . . . . . . . . 14
|
107 | 94, 106 | sylibd 149 |
. . . . . . . . . . . . 13
|
108 | | elni2 7288 |
. . . . . . . . . . . . . . . 16
|
109 | 108 | simprbi 275 |
. . . . . . . . . . . . . . 15
|
110 | 101, 109 | syl 14 |
. . . . . . . . . . . . . 14
|
111 | | n0i 3426 |
. . . . . . . . . . . . . 14
|
112 | | biorf 744 |
. . . . . . . . . . . . . 14
|
113 | 110, 111,
112 | 3syl 17 |
. . . . . . . . . . . . 13
|
114 | 107, 113 | sylibrd 169 |
. . . . . . . . . . . 12
|
115 | 62 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
|
116 | | simpl1 1000 |
. . . . . . . . . . . . . . . . . 18
|
117 | 115, 116 | eqeltrrd 2253 |
. . . . . . . . . . . . . . . . 17
|
118 | | opelxp 4650 |
. . . . . . . . . . . . . . . . 17
|
119 | 117, 118 | sylib 122 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | simprd 114 |
. . . . . . . . . . . . . . 15
|
121 | | pinn 7283 |
. . . . . . . . . . . . . . 15
|
122 | 120, 121 | syl 14 |
. . . . . . . . . . . . . 14
|
123 | | nnm0 6466 |
. . . . . . . . . . . . . 14
|
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . 13
|
125 | | oveq2 5873 |
. . . . . . . . . . . . . 14
|
126 | 125 | eqeq1d 2184 |
. . . . . . . . . . . . 13
|
127 | 124, 126 | syl5ibrcom 157 |
. . . . . . . . . . . 12
|
128 | 114, 127 | syld 45 |
. . . . . . . . . . 11
|
129 | | oveq2 5873 |
. . . . . . . . . . . . . . . 16
|
130 | 124 | eqeq2d 2187 |
. . . . . . . . . . . . . . . 16
|
131 | 129, 130 | syl5ib 154 |
. . . . . . . . . . . . . . 15
|
132 | | simprlr 538 |
. . . . . . . . . . . . . . . 16
|
133 | 132 | eqeq1d 2184 |
. . . . . . . . . . . . . . 15
|
134 | 131, 133 | sylibrd 169 |
. . . . . . . . . . . . . 14
|
135 | 119 | simpld 112 |
. . . . . . . . . . . . . . 15
|
136 | | nnm00 6521 |
. . . . . . . . . . . . . . 15
|
137 | 135, 103,
136 | syl2anc 411 |
. . . . . . . . . . . . . 14
|
138 | 134, 137 | sylibd 149 |
. . . . . . . . . . . . 13
|
139 | | biorf 744 |
. . . . . . . . . . . . . . 15
|
140 | | orcom 728 |
. . . . . . . . . . . . . . 15
|
141 | 139, 140 | bitrdi 196 |
. . . . . . . . . . . . . 14
|
142 | 110, 111,
141 | 3syl 17 |
. . . . . . . . . . . . 13
|
143 | 138, 142 | sylibrd 169 |
. . . . . . . . . . . 12
|
144 | | oveq1 5872 |
. . . . . . . . . . . . . 14
|
145 | 144 | eqeq1d 2184 |
. . . . . . . . . . . . 13
|
146 | 76, 145 | syl5ibrcom 157 |
. . . . . . . . . . . 12
|
147 | 143, 146 | syld 45 |
. . . . . . . . . . 11
|
148 | 128, 147 | jcad 307 |
. . . . . . . . . 10
|
149 | | eqtr3 2195 |
. . . . . . . . . . 11
|
150 | 149 | eqcomd 2181 |
. . . . . . . . . 10
|
151 | 148, 150 | syl6 33 |
. . . . . . . . 9
|
152 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
|
153 | 91, 152 | oveq12d 5883 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | adantl 277 |
. . . . . . . . . . . . . . 15
|
155 | 100 | simpld 112 |
. . . . . . . . . . . . . . . . 17
|
156 | | nnmcl 6472 |
. . . . . . . . . . . . . . . . 17
|
157 | 155, 74, 156 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
|
158 | | nnmcom 6480 |
. . . . . . . . . . . . . . . . 17
|
159 | 158 | adantl 277 |
. . . . . . . . . . . . . . . 16
|
160 | | nnmass 6478 |
. . . . . . . . . . . . . . . . 17
|
161 | 160 | adantl 277 |
. . . . . . . . . . . . . . . 16
|
162 | 157, 135,
103, 159, 161 | caov13d 6048 |
. . . . . . . . . . . . . . 15
|
163 | | nnmcl 6472 |
. . . . . . . . . . . . . . . . 17
|
164 | 122, 155,
163 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
|
165 | 161, 103,
104, 164 | caovassd 6024 |
. . . . . . . . . . . . . . 15
|
166 | 154, 162,
165 | 3eqtr3d 2216 |
. . . . . . . . . . . . . 14
|
167 | | nnmcl 6472 |
. . . . . . . . . . . . . . . 16
|
168 | 135, 157,
167 | syl2anc 411 |
. . . . . . . . . . . . . . 15
|
169 | | nnmcl 6472 |
. . . . . . . . . . . . . . . 16
|
170 | 104, 164,
169 | syl2anc 411 |
. . . . . . . . . . . . . . 15
|
171 | | nnmcan 6510 |
. . . . . . . . . . . . . . 15
|
172 | 103, 168,
170, 110, 171 | syl31anc 1241 |
. . . . . . . . . . . . . 14
|
173 | 166, 172 | mpbid 147 |
. . . . . . . . . . . . 13
|
174 | 135, 155,
74, 159, 161 | caov12d 6046 |
. . . . . . . . . . . . 13
|
175 | 104, 122,
155, 159, 161 | caov13d 6048 |
. . . . . . . . . . . . 13
|
176 | 173, 174,
175 | 3eqtr3d 2216 |
. . . . . . . . . . . 12
|
177 | 176 | adantr 276 |
. . . . . . . . . . 11
|
178 | | nnmcl 6472 |
. . . . . . . . . . . . . 14
|
179 | 135, 74, 178 | syl2anc 411 |
. . . . . . . . . . . . 13
|
180 | | nnmcl 6472 |
. . . . . . . . . . . . . 14
|
181 | 122, 104,
180 | syl2anc 411 |
. . . . . . . . . . . . 13
|
182 | 155, 179,
181 | 3jca 1177 |
. . . . . . . . . . . 12
|
183 | | nnmcan 6510 |
. . . . . . . . . . . 12
|
184 | 182, 183 | sylan 283 |
. . . . . . . . . . 11
|
185 | 177, 184 | mpbid 147 |
. . . . . . . . . 10
|
186 | 185 | ex 115 |
. . . . . . . . 9
|
187 | | 0elnn 4612 |
. . . . . . . . . 10
|
188 | 155, 187 | syl 14 |
. . . . . . . . 9
|
189 | 151, 186,
188 | mpjaod 718 |
. . . . . . . 8
|
190 | 61, 65, 189 | jca32 310 |
. . . . . . 7
|
191 | 190 | 2eximi 1599 |
. . . . . 6
|
192 | 191 | exlimivv 1894 |
. . . . 5
|
193 | 192 | exlimivv 1894 |
. . . 4
|
194 | 193 | 2eximi 1599 |
. . 3
|
195 | 59, 194 | syl 14 |
. 2
~Q0
~Q0
|
196 | | 19.42vvvv 1911 |
. . 3
|
197 | 5 | anbi1d 465 |
. . . . . . 7
|
198 | 197 | anbi1d 465 |
. . . . . 6
|
199 | 198 | 4exbidv 1868 |
. . . . 5
|
200 | 4, 199 | anbi12d 473 |
. . . 4
|
201 | 27 | anbi2d 464 |
. . . . 5
|
202 | 29 | anbi2d 464 |
. . . . . . 7
|