Step | Hyp | Ref
| Expression |
1 | | vex 2604 |
. . . . . . . . . 10
|
2 | | vex 2604 |
. . . . . . . . . 10
|
3 | | eleq1 2141 |
. . . . . . . . . . . 12
|
4 | 3 | anbi1d 452 |
. . . . . . . . . . 11
|
5 | | eqeq1 2087 |
. . . . . . . . . . . . . 14
|
6 | 5 | anbi1d 452 |
. . . . . . . . . . . . 13
|
7 | 6 | anbi1d 452 |
. . . . . . . . . . . 12
|
8 | 7 | 4exbidv 1791 |
. . . . . . . . . . 11
|
9 | 4, 8 | anbi12d 456 |
. . . . . . . . . 10
|
10 | | eleq1 2141 |
. . . . . . . . . . . 12
|
11 | 10 | anbi2d 451 |
. . . . . . . . . . 11
|
12 | | eqeq1 2087 |
. . . . . . . . . . . . . 14
|
13 | 12 | anbi2d 451 |
. . . . . . . . . . . . 13
|
14 | 13 | anbi1d 452 |
. . . . . . . . . . . 12
|
15 | 14 | 4exbidv 1791 |
. . . . . . . . . . 11
|
16 | 11, 15 | anbi12d 456 |
. . . . . . . . . 10
|
17 | | df-enq0 6614 |
. . . . . . . . . 10
~Q0
|
18 | 1, 2, 9, 16, 17 | brab 4027 |
. . . . . . . . 9
~Q0
|
19 | | vex 2604 |
. . . . . . . . . 10
|
20 | | eleq1 2141 |
. . . . . . . . . . . 12
|
21 | 20 | anbi1d 452 |
. . . . . . . . . . 11
|
22 | | eqeq1 2087 |
. . . . . . . . . . . . . 14
|
23 | 22 | anbi1d 452 |
. . . . . . . . . . . . 13
|
24 | 23 | anbi1d 452 |
. . . . . . . . . . . 12
|
25 | 24 | 4exbidv 1791 |
. . . . . . . . . . 11
|
26 | 21, 25 | anbi12d 456 |
. . . . . . . . . 10
|
27 | | eleq1 2141 |
. . . . . . . . . . . 12
|
28 | 27 | anbi2d 451 |
. . . . . . . . . . 11
|
29 | | eqeq1 2087 |
. . . . . . . . . . . . . 14
|
30 | 29 | anbi2d 451 |
. . . . . . . . . . . . 13
|
31 | 30 | anbi1d 452 |
. . . . . . . . . . . 12
|
32 | 31 | 4exbidv 1791 |
. . . . . . . . . . 11
|
33 | 28, 32 | anbi12d 456 |
. . . . . . . . . 10
|
34 | | df-enq0 6614 |
. . . . . . . . . 10
~Q0
|
35 | 2, 19, 26, 33, 34 | brab 4027 |
. . . . . . . . 9
~Q0
|
36 | 18, 35 | anbi12i 447 |
. . . . . . . 8
~Q0
~Q0
|
37 | 36 | biimpi 118 |
. . . . . . 7
~Q0
~Q0
|
38 | | an4 550 |
. . . . . . 7
|
39 | 37, 38 | sylib 120 |
. . . . . 6
~Q0
~Q0
|
40 | | 3anass 923 |
. . . . . . . 8
|
41 | | anass 393 |
. . . . . . . . 9
|
42 | | anass 393 |
. . . . . . . . . 10
|
43 | 42 | anbi2i 444 |
. . . . . . . . 9
|
44 | | anidm 388 |
. . . . . . . . . . 11
|
45 | 44 | anbi1i 445 |
. . . . . . . . . 10
|
46 | 45 | anbi2i 444 |
. . . . . . . . 9
|
47 | 41, 43, 46 | 3bitr2i 206 |
. . . . . . . 8
|
48 | 40, 47 | bitr4i 185 |
. . . . . . 7
|
49 | 48 | anbi1i 445 |
. . . . . 6
|
50 | 39, 49 | sylibr 132 |
. . . . 5
~Q0
~Q0
|
51 | | ee8anv 1851 |
. . . . . 6
|
52 | 51 | anbi2i 444 |
. . . . 5
|
53 | 50, 52 | sylibr 132 |
. . . 4
~Q0
~Q0
|
54 | | 19.42vvvv 1831 |
. . . . . . 7
|
55 | 54 | 2exbii 1537 |
. . . . . 6
|
56 | 55 | 2exbii 1537 |
. . . . 5
|
57 | | 19.42vvvv 1831 |
. . . . 5
|
58 | 56, 57 | bitri 182 |
. . . 4
|
59 | 53, 58 | sylibr 132 |
. . 3
~Q0
~Q0
|
60 | | 3simpb 936 |
. . . . . . . . 9
|
61 | 60 | adantr 270 |
. . . . . . . 8
|
62 | | simplll 499 |
. . . . . . . . . 10
|
63 | | simprlr 504 |
. . . . . . . . . 10
|
64 | 62, 63 | jca 300 |
. . . . . . . . 9
|
65 | 64 | adantl 271 |
. . . . . . . 8
|
66 | | oveq1 5539 |
. . . . . . . . . . . . . . . 16
|
67 | 63 | adantl 271 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | | simpl3 943 |
. . . . . . . . . . . . . . . . . . . . . 22
|
69 | 67, 68 | eqeltrrd 2156 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | | opelxp 4392 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 69, 70 | sylib 120 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | simprd 112 |
. . . . . . . . . . . . . . . . . . 19
|
73 | | pinn 6499 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
|
75 | | nnm0r 6081 |
. . . . . . . . . . . . . . . . . 18
|
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | eqeq2d 2092 |
. . . . . . . . . . . . . . . 16
|
78 | 66, 77 | syl5ib 152 |
. . . . . . . . . . . . . . 15
|
79 | | simprr 498 |
. . . . . . . . . . . . . . . . . 18
|
80 | | eqtr2 2099 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | | vex 2604 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
82 | | vex 2604 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 81, 82 | opth 3992 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 80, 83 | sylib 120 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | | oveq1 5539 |
. . . . . . . . . . . . . . . . . . . . . 22
|
86 | | oveq1 5539 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 85, 86 | eqeqan12d 2096 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 84, 87 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | ad2ant2lr 493 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 89 | ad2ant2r 492 |
. . . . . . . . . . . . . . . . . 18
|
91 | 79, 90 | mpbird 165 |
. . . . . . . . . . . . . . . . 17
|
92 | 91 | eqeq1d 2089 |
. . . . . . . . . . . . . . . 16
|
93 | 92 | adantl 271 |
. . . . . . . . . . . . . . 15
|
94 | 78, 93 | sylibd 147 |
. . . . . . . . . . . . . 14
|
95 | | simpllr 500 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 95 | adantl 271 |
. . . . . . . . . . . . . . . . . . 19
|
97 | | simpl2 942 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 96, 97 | eqeltrrd 2156 |
. . . . . . . . . . . . . . . . . 18
|
99 | | opelxp 4392 |
. . . . . . . . . . . . . . . . . 18
|
100 | 98, 99 | sylib 120 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | simprd 112 |
. . . . . . . . . . . . . . . 16
|
102 | | pinn 6499 |
. . . . . . . . . . . . . . . 16
|
103 | 101, 102 | syl 14 |
. . . . . . . . . . . . . . 15
|
104 | 71 | simpld 110 |
. . . . . . . . . . . . . . 15
|
105 | | nnm00 6125 |
. . . . . . . . . . . . . . 15
|
106 | 103, 104,
105 | syl2anc 403 |
. . . . . . . . . . . . . 14
|
107 | 94, 106 | sylibd 147 |
. . . . . . . . . . . . 13
|
108 | | elni2 6504 |
. . . . . . . . . . . . . . . 16
|
109 | 108 | simprbi 269 |
. . . . . . . . . . . . . . 15
|
110 | 101, 109 | syl 14 |
. . . . . . . . . . . . . 14
|
111 | | n0i 3256 |
. . . . . . . . . . . . . 14
|
112 | | biorf 695 |
. . . . . . . . . . . . . 14
|
113 | 110, 111,
112 | 3syl 17 |
. . . . . . . . . . . . 13
|
114 | 107, 113 | sylibrd 167 |
. . . . . . . . . . . 12
|
115 | 62 | adantl 271 |
. . . . . . . . . . . . . . . . . 18
|
116 | | simpl1 941 |
. . . . . . . . . . . . . . . . . 18
|
117 | 115, 116 | eqeltrrd 2156 |
. . . . . . . . . . . . . . . . 17
|
118 | | opelxp 4392 |
. . . . . . . . . . . . . . . . 17
|
119 | 117, 118 | sylib 120 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | simprd 112 |
. . . . . . . . . . . . . . 15
|
121 | | pinn 6499 |
. . . . . . . . . . . . . . 15
|
122 | 120, 121 | syl 14 |
. . . . . . . . . . . . . 14
|
123 | | nnm0 6077 |
. . . . . . . . . . . . . 14
|
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . 13
|
125 | | oveq2 5540 |
. . . . . . . . . . . . . 14
|
126 | 125 | eqeq1d 2089 |
. . . . . . . . . . . . 13
|
127 | 124, 126 | syl5ibrcom 155 |
. . . . . . . . . . . 12
|
128 | 114, 127 | syld 44 |
. . . . . . . . . . 11
|
129 | | oveq2 5540 |
. . . . . . . . . . . . . . . 16
|
130 | 124 | eqeq2d 2092 |
. . . . . . . . . . . . . . . 16
|
131 | 129, 130 | syl5ib 152 |
. . . . . . . . . . . . . . 15
|
132 | | simprlr 504 |
. . . . . . . . . . . . . . . 16
|
133 | 132 | eqeq1d 2089 |
. . . . . . . . . . . . . . 15
|
134 | 131, 133 | sylibrd 167 |
. . . . . . . . . . . . . 14
|
135 | 119 | simpld 110 |
. . . . . . . . . . . . . . 15
|
136 | | nnm00 6125 |
. . . . . . . . . . . . . . 15
|
137 | 135, 103,
136 | syl2anc 403 |
. . . . . . . . . . . . . 14
|
138 | 134, 137 | sylibd 147 |
. . . . . . . . . . . . 13
|
139 | | biorf 695 |
. . . . . . . . . . . . . . 15
|
140 | | orcom 679 |
. . . . . . . . . . . . . . 15
|
141 | 139, 140 | syl6bb 194 |
. . . . . . . . . . . . . 14
|
142 | 110, 111,
141 | 3syl 17 |
. . . . . . . . . . . . 13
|
143 | 138, 142 | sylibrd 167 |
. . . . . . . . . . . 12
|
144 | | oveq1 5539 |
. . . . . . . . . . . . . 14
|
145 | 144 | eqeq1d 2089 |
. . . . . . . . . . . . 13
|
146 | 76, 145 | syl5ibrcom 155 |
. . . . . . . . . . . 12
|
147 | 143, 146 | syld 44 |
. . . . . . . . . . 11
|
148 | 128, 147 | jcad 301 |
. . . . . . . . . 10
|
149 | | eqtr3 2100 |
. . . . . . . . . . 11
|
150 | 149 | eqcomd 2086 |
. . . . . . . . . 10
|
151 | 148, 150 | syl6 33 |
. . . . . . . . 9
|
152 | | simplr 496 |
. . . . . . . . . . . . . . . . 17
|
153 | 91, 152 | oveq12d 5550 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | adantl 271 |
. . . . . . . . . . . . . . 15
|
155 | 100 | simpld 110 |
. . . . . . . . . . . . . . . . 17
|
156 | | nnmcl 6083 |
. . . . . . . . . . . . . . . . 17
|
157 | 155, 74, 156 | syl2anc 403 |
. . . . . . . . . . . . . . . 16
|
158 | | nnmcom 6091 |
. . . . . . . . . . . . . . . . 17
|
159 | 158 | adantl 271 |
. . . . . . . . . . . . . . . 16
|
160 | | nnmass 6089 |
. . . . . . . . . . . . . . . . 17
|
161 | 160 | adantl 271 |
. . . . . . . . . . . . . . . 16
|
162 | 157, 135,
103, 159, 161 | caov13d 5704 |
. . . . . . . . . . . . . . 15
|
163 | | nnmcl 6083 |
. . . . . . . . . . . . . . . . 17
|
164 | 122, 155,
163 | syl2anc 403 |
. . . . . . . . . . . . . . . 16
|
165 | 161, 103,
104, 164 | caovassd 5680 |
. . . . . . . . . . . . . . 15
|
166 | 154, 162,
165 | 3eqtr3d 2121 |
. . . . . . . . . . . . . 14
|
167 | | nnmcl 6083 |
. . . . . . . . . . . . . . . 16
|
168 | 135, 157,
167 | syl2anc 403 |
. . . . . . . . . . . . . . 15
|
169 | | nnmcl 6083 |
. . . . . . . . . . . . . . . 16
|
170 | 104, 164,
169 | syl2anc 403 |
. . . . . . . . . . . . . . 15
|
171 | | nnmcan 6115 |
. . . . . . . . . . . . . . 15
|
172 | 103, 168,
170, 110, 171 | syl31anc 1172 |
. . . . . . . . . . . . . 14
|
173 | 166, 172 | mpbid 145 |
. . . . . . . . . . . . 13
|
174 | 135, 155,
74, 159, 161 | caov12d 5702 |
. . . . . . . . . . . . 13
|
175 | 104, 122,
155, 159, 161 | caov13d 5704 |
. . . . . . . . . . . . 13
|
176 | 173, 174,
175 | 3eqtr3d 2121 |
. . . . . . . . . . . 12
|
177 | 176 | adantr 270 |
. . . . . . . . . . 11
|
178 | | nnmcl 6083 |
. . . . . . . . . . . . . 14
|
179 | 135, 74, 178 | syl2anc 403 |
. . . . . . . . . . . . 13
|
180 | | nnmcl 6083 |
. . . . . . . . . . . . . 14
|
181 | 122, 104,
180 | syl2anc 403 |
. . . . . . . . . . . . 13
|
182 | 155, 179,
181 | 3jca 1118 |
. . . . . . . . . . . 12
|
183 | | nnmcan 6115 |
. . . . . . . . . . . 12
|
184 | 182, 183 | sylan 277 |
. . . . . . . . . . 11
|
185 | 177, 184 | mpbid 145 |
. . . . . . . . . 10
|
186 | 185 | ex 113 |
. . . . . . . . 9
|
187 | | 0elnn 4358 |
. . . . . . . . . 10
|
188 | 155, 187 | syl 14 |
. . . . . . . . 9
|
189 | 151, 186,
188 | mpjaod 670 |
. . . . . . . 8
|
190 | 61, 65, 189 | jca32 303 |
. . . . . . 7
|
191 | 190 | 2eximi 1532 |
. . . . . 6
|
192 | 191 | exlimivv 1817 |
. . . . 5
|
193 | 192 | exlimivv 1817 |
. . . 4
|
194 | 193 | 2eximi 1532 |
. . 3
|
195 | 59, 194 | syl 14 |
. 2
~Q0
~Q0
|
196 | | 19.42vvvv 1831 |
. . 3
|
197 | 5 | anbi1d 452 |
. . . . . . 7
|
198 | 197 | anbi1d 452 |
. . . . . 6
|
199 | 198 | 4exbidv 1791 |
. . . . 5
|
200 | 4, 199 | anbi12d 456 |
. . . 4
|
201 | 27 | anbi2d 451 |
. . . . 5
|
202 | 29 | anbi2d 451 |
. . . . . . 7
|
203 | 202 | anbi1d 452 |
. . . . . 6
|
204 | 203 | 4exbidv 1791 |
. . . . 5
|
205 | 201, 204 | anbi12d 456 |
. . . 4
|
206 | | df-enq0 6614 |
. . . 4
~Q0
|
207 | 1, 19, 200, 205, 206 | brab 4027 |
. . 3
~Q0
|
208 | 196, 207 | bitr4i 185 |
. 2
~Q0 |
209 | 195, 208 | sylib 120 |
1
~Q0
~Q0 ~Q0 |