Step | Hyp | Ref
| Expression |
1 | | vex 2658 |
. . . . . . . . . 10
 |
2 | | vex 2658 |
. . . . . . . . . 10
 |
3 | | eleq1 2175 |
. . . . . . . . . . . 12
   
     |
4 | 3 | anbi1d 458 |
. . . . . . . . . . 11
    
     
      |
5 | | eqeq1 2119 |
. . . . . . . . . . . . . 14
    
      |
6 | 5 | anbi1d 458 |
. . . . . . . . . . . . 13
                     |
7 | 6 | anbi1d 458 |
. . . . . . . . . . . 12
               
    
            |
8 | 7 | 4exbidv 1822 |
. . . . . . . . . . 11
              
        
                         |
9 | 4, 8 | anbi12d 462 |
. . . . . . . . . 10
        
                          
                             |
10 | | eleq1 2175 |
. . . . . . . . . . . 12
   
     |
11 | 10 | anbi2d 457 |
. . . . . . . . . . 11
    
     
      |
12 | | eqeq1 2119 |
. . . . . . . . . . . . . 14
    
      |
13 | 12 | anbi2d 457 |
. . . . . . . . . . . . 13
                     |
14 | 13 | anbi1d 458 |
. . . . . . . . . . . 12
               
    
            |
15 | 14 | 4exbidv 1822 |
. . . . . . . . . . 11
              
        
                         |
16 | 11, 15 | anbi12d 462 |
. . . . . . . . . 10
        
                          
                             |
17 | | df-enq0 7174 |
. . . . . . . . . 10
~Q0        
                            |
18 | 1, 2, 9, 16, 17 | brab 4152 |
. . . . . . . . 9
 ~Q0    
                            |
19 | | vex 2658 |
. . . . . . . . . 10
 |
20 | | eleq1 2175 |
. . . . . . . . . . . 12
   
     |
21 | 20 | anbi1d 458 |
. . . . . . . . . . 11
    
     
      |
22 | | eqeq1 2119 |
. . . . . . . . . . . . . 14
    
      |
23 | 22 | anbi1d 458 |
. . . . . . . . . . . . 13
         
   
       |
24 | 23 | anbi1d 458 |
. . . . . . . . . . . 12
      
             
            |
25 | 24 | 4exbidv 1822 |
. . . . . . . . . . 11
                  
    
                         |
26 | 21, 25 | anbi12d 462 |
. . . . . . . . . 10
        
                          
                             |
27 | | eleq1 2175 |
. . . . . . . . . . . 12
   
     |
28 | 27 | anbi2d 457 |
. . . . . . . . . . 11
    
     
      |
29 | | eqeq1 2119 |
. . . . . . . . . . . . . 14
    
      |
30 | 29 | anbi2d 457 |
. . . . . . . . . . . . 13
         
   
       |
31 | 30 | anbi1d 458 |
. . . . . . . . . . . 12
      
             
            |
32 | 31 | 4exbidv 1822 |
. . . . . . . . . . 11
                  
    
                         |
33 | 28, 32 | anbi12d 462 |
. . . . . . . . . 10
        
                          
                             |
34 | | df-enq0 7174 |
. . . . . . . . . 10
~Q0        
                            |
35 | 2, 19, 26, 33, 34 | brab 4152 |
. . . . . . . . 9
 ~Q0    
                            |
36 | 18, 35 | anbi12i 453 |
. . . . . . . 8
  ~Q0
~Q0 
    
                                                           |
37 | 36 | biimpi 119 |
. . . . . . 7
  ~Q0
~Q0         
                                                        |
38 | | an4 558 |
. . . . . . 7
        
                                                     
    
                       
                                   |
39 | 37, 38 | sylib 121 |
. . . . . 6
  ~Q0
~Q0         
                    
                                   |
40 | | 3anass 947 |
. . . . . . . 8
                     |
41 | | anass 396 |
. . . . . . . . 9
    
         
                |
42 | | anass 396 |
. . . . . . . . . 10
    
                  |
43 | 42 | anbi2i 450 |
. . . . . . . . 9
       
      
                |
44 | | anidm 391 |
. . . . . . . . . . 11
      
    |
45 | 44 | anbi1i 451 |
. . . . . . . . . 10
    
              |
46 | 45 | anbi2i 450 |
. . . . . . . . 9
       
      
            |
47 | 41, 43, 46 | 3bitr2i 207 |
. . . . . . . 8
    
         
            |
48 | 40, 47 | bitr4i 186 |
. . . . . . 7
            
            |
49 | 48 | anbi1i 451 |
. . . . . 6
    
 
                                                 
    
                       
                                   |
50 | 39, 49 | sylibr 133 |
. . . . 5
  ~Q0
~Q0     
 
                                                    |
51 | | ee8anv 1883 |
. . . . . 6
                      
                 
                                                      |
52 | 51 | anbi2i 450 |
. . . . 5
    
 
                        
                 
          
    
                                                 |
53 | 50, 52 | sylibr 133 |
. . . 4
  ~Q0
~Q0     
 
                        
                 
         |
54 | | 19.42vvvv 1863 |
. . . . . . 7
            
 
                                 
        
             
                 
         |
55 | 54 | 2exbii 1566 |
. . . . . 6
                
    
                       
                
                
                 
         |
56 | 55 | 2exbii 1566 |
. . . . 5
                    
    
                       
                  
 
                              
             |
57 | | 19.42vvvv 1863 |
. . . . 5
                 
             
                 
          
    
                     
                 
         |
58 | 56, 57 | bitri 183 |
. . . 4
                    
    
                       
          
    
                     
                 
         |
59 | 53, 58 | sylibr 133 |
. . 3
  ~Q0
~Q0                     
    
                       
         |
60 | | 3simpb 960 |
. . . . . . . . 9
        
        |
61 | 60 | adantr 272 |
. . . . . . . 8
    
 
                                          |
62 | | simplll 505 |
. . . . . . . . . 10
                    
         
     |
63 | | simprlr 510 |
. . . . . . . . . 10
                    
         
     |
64 | 62, 63 | jca 302 |
. . . . . . . . 9
                    
         
          |
65 | 64 | adantl 273 |
. . . . . . . 8
    
 
                                     
      |
66 | | oveq1 5733 |
. . . . . . . . . . . . . . . 16

  
   |
67 | 63 | adantl 273 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                                       |
68 | | simpl3 967 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                                      |
69 | 67, 68 | eqeltrrd 2190 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
                                         |
70 | | opelxp 4527 |
. . . . . . . . . . . . . . . . . . . . 21
          |
71 | 69, 70 | sylib 121 |
. . . . . . . . . . . . . . . . . . . 20
    
 
                                  
   |
72 | 71 | simprd 113 |
. . . . . . . . . . . . . . . . . . 19
    
 
                                    |
73 | | pinn 7059 |
. . . . . . . . . . . . . . . . . . 19
   |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    
 
                                    |
75 | | nnm0r 6327 |
. . . . . . . . . . . . . . . . . 18
     |
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . . . . 17
    
 
                                      |
77 | 76 | eqeq2d 2124 |
. . . . . . . . . . . . . . . 16
    
 
                                      
     |
78 | 66, 77 | syl5ib 153 |
. . . . . . . . . . . . . . 15
    
 
                                        |
79 | | simprr 504 |
. . . . . . . . . . . . . . . . . 18
                    
         
      |
80 | | eqtr2 2131 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
  
     |
81 | | vex 2658 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
82 | | vex 2658 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
83 | 81, 82 | opth 4117 |
. . . . . . . . . . . . . . . . . . . . . 22
       
   |
84 | 80, 83 | sylib 121 |
. . . . . . . . . . . . . . . . . . . . 21
    
   
    |
85 | | oveq1 5733 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
86 | | oveq1 5733 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
87 | 85, 86 | eqeqan12d 2128 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
88 | 84, 87 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
    
   
    
       |
89 | 88 | ad2ant2lr 499 |
. . . . . . . . . . . . . . . . . . 19
                  
    
       |
90 | 89 | ad2ant2r 498 |
. . . . . . . . . . . . . . . . . 18
                    
         
    
       |
91 | 79, 90 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
                    
         
      |
92 | 91 | eqeq1d 2121 |
. . . . . . . . . . . . . . . 16
                    
         
  
     |
93 | 92 | adantl 273 |
. . . . . . . . . . . . . . 15
    
 
                                    
     |
94 | 78, 93 | sylibd 148 |
. . . . . . . . . . . . . 14
    
 
                                        |
95 | | simpllr 506 |
. . . . . . . . . . . . . . . . . . . 20
                    
         
     |
96 | 95 | adantl 273 |
. . . . . . . . . . . . . . . . . . 19
    
 
                                       |
97 | | simpl2 966 |
. . . . . . . . . . . . . . . . . . 19
    
 
                                      |
98 | 96, 97 | eqeltrrd 2190 |
. . . . . . . . . . . . . . . . . 18
    
 
                                    
    |
99 | | opelxp 4527 |
. . . . . . . . . . . . . . . . . 18
          |
100 | 98, 99 | sylib 121 |
. . . . . . . . . . . . . . . . 17
    
 
                                  
   |
101 | 100 | simprd 113 |
. . . . . . . . . . . . . . . 16
    
 
                                    |
102 | | pinn 7059 |
. . . . . . . . . . . . . . . 16
   |
103 | 101, 102 | syl 14 |
. . . . . . . . . . . . . . 15
    
 
                                    |
104 | 71 | simpld 111 |
. . . . . . . . . . . . . . 15
    
 
                                    |
105 | | nnm00 6377 |
. . . . . . . . . . . . . . 15
 
         |
106 | 103, 104,
105 | syl2anc 406 |
. . . . . . . . . . . . . 14
    
 
                                    
     |
107 | 94, 106 | sylibd 148 |
. . . . . . . . . . . . 13
    
 
                                        |
108 | | elni2 7064 |
. . . . . . . . . . . . . . . 16

    |
109 | 108 | simprbi 271 |
. . . . . . . . . . . . . . 15
   |
110 | 101, 109 | syl 14 |
. . . . . . . . . . . . . 14
    
 
                                    |
111 | | n0i 3332 |
. . . . . . . . . . . . . 14

  |
112 | | biorf 716 |
. . . . . . . . . . . . . 14
 
     |
113 | 110, 111,
112 | 3syl 17 |
. . . . . . . . . . . . 13
    
 
                                  
     |
114 | 107, 113 | sylibrd 168 |
. . . . . . . . . . . 12
    
 
                                      |
115 | 62 | adantl 273 |
. . . . . . . . . . . . . . . . . 18
    
 
                                       |
116 | | simpl1 965 |
. . . . . . . . . . . . . . . . . 18
    
 
                                      |
117 | 115, 116 | eqeltrrd 2190 |
. . . . . . . . . . . . . . . . 17
    
 
                                    
    |
118 | | opelxp 4527 |
. . . . . . . . . . . . . . . . 17
          |
119 | 117, 118 | sylib 121 |
. . . . . . . . . . . . . . . 16
    
 
                                  
   |
120 | 119 | simprd 113 |
. . . . . . . . . . . . . . 15
    
 
                                    |
121 | | pinn 7059 |
. . . . . . . . . . . . . . 15
   |
122 | 120, 121 | syl 14 |
. . . . . . . . . . . . . 14
    
 
                                    |
123 | | nnm0 6323 |
. . . . . . . . . . . . . 14
     |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . 13
    
 
                                      |
125 | | oveq2 5734 |
. . . . . . . . . . . . . 14

      |
126 | 125 | eqeq1d 2121 |
. . . . . . . . . . . . 13

  
     |
127 | 124, 126 | syl5ibrcom 156 |
. . . . . . . . . . . 12
    
 
                                        |
128 | 114, 127 | syld 45 |
. . . . . . . . . . 11
    
 
                                        |
129 | | oveq2 5734 |
. . . . . . . . . . . . . . . 16

      |
130 | 124 | eqeq2d 2124 |
. . . . . . . . . . . . . . . 16
    
 
                                      
     |
131 | 129, 130 | syl5ib 153 |
. . . . . . . . . . . . . . 15
    
 
                                        |
132 | | simprlr 510 |
. . . . . . . . . . . . . . . 16
    
 
                                        |
133 | 132 | eqeq1d 2121 |
. . . . . . . . . . . . . . 15
    
 
                                    
     |
134 | 131, 133 | sylibrd 168 |
. . . . . . . . . . . . . 14
    
 
                                        |
135 | 119 | simpld 111 |
. . . . . . . . . . . . . . 15
    
 
                                    |
136 | | nnm00 6377 |
. . . . . . . . . . . . . . 15
 
         |
137 | 135, 103,
136 | syl2anc 406 |
. . . . . . . . . . . . . 14
    
 
                                    
     |
138 | 134, 137 | sylibd 148 |
. . . . . . . . . . . . 13
    
 
                                        |
139 | | biorf 716 |
. . . . . . . . . . . . . . 15
 
     |
140 | | orcom 700 |
. . . . . . . . . . . . . . 15
  
    |
141 | 139, 140 | syl6bb 195 |
. . . . . . . . . . . . . 14
 
     |
142 | 110, 111,
141 | 3syl 17 |
. . . . . . . . . . . . 13
    
 
                                  
     |
143 | 138, 142 | sylibrd 168 |
. . . . . . . . . . . 12
    
 
                                      |
144 | | oveq1 5733 |
. . . . . . . . . . . . . 14

  
   |
145 | 144 | eqeq1d 2121 |
. . . . . . . . . . . . 13

  
     |
146 | 76, 145 | syl5ibrcom 156 |
. . . . . . . . . . . 12
    
 
                                        |
147 | 143, 146 | syld 45 |
. . . . . . . . . . 11
    
 
                                        |
148 | 128, 147 | jcad 303 |
. . . . . . . . . 10
    
 
                                            |
149 | | eqtr3 2132 |
. . . . . . . . . . 11
             |
150 | 149 | eqcomd 2118 |
. . . . . . . . . 10
             |
151 | 148, 150 | syl6 33 |
. . . . . . . . 9
    
 
                                          |
152 | | simplr 502 |
. . . . . . . . . . . . . . . . 17
                    
         
      |
153 | 91, 152 | oveq12d 5744 |
. . . . . . . . . . . . . . . 16
                    
         
              |
154 | 153 | adantl 273 |
. . . . . . . . . . . . . . 15
    
 
                                                |
155 | 100 | simpld 111 |
. . . . . . . . . . . . . . . . 17
    
 
                                    |
156 | | nnmcl 6329 |
. . . . . . . . . . . . . . . . 17
 
     |
157 | 155, 74, 156 | syl2anc 406 |
. . . . . . . . . . . . . . . 16
    
 
                                      |
158 | | nnmcom 6337 |
. . . . . . . . . . . . . . . . 17
 
       |
159 | 158 | adantl 273 |
. . . . . . . . . . . . . . . 16
       
        
                 
                |
160 | | nnmass 6335 |
. . . . . . . . . . . . . . . . 17
 
           |
161 | 160 | adantl 273 |
. . . . . . . . . . . . . . . 16
       
        
                 
                    |
162 | 157, 135,
103, 159, 161 | caov13d 5906 |
. . . . . . . . . . . . . . 15
    
 
                                                |
163 | | nnmcl 6329 |
. . . . . . . . . . . . . . . . 17
 
     |
164 | 122, 155,
163 | syl2anc 406 |
. . . . . . . . . . . . . . . 16
    
 
                                      |
165 | 161, 103,
104, 164 | caovassd 5882 |
. . . . . . . . . . . . . . 15
    
 
                                                |
166 | 154, 162,
165 | 3eqtr3d 2153 |
. . . . . . . . . . . . . 14
    
 
                                                |
167 | | nnmcl 6329 |
. . . . . . . . . . . . . . . 16
           |
168 | 135, 157,
167 | syl2anc 406 |
. . . . . . . . . . . . . . 15
    
 
                                        |
169 | | nnmcl 6329 |
. . . . . . . . . . . . . . . 16
  
        |
170 | 104, 164,
169 | syl2anc 406 |
. . . . . . . . . . . . . . 15
    
 
                                        |
171 | | nnmcan 6367 |
. . . . . . . . . . . . . . 15
                                     |
172 | 103, 168,
170, 110, 171 | syl31anc 1200 |
. . . . . . . . . . . . . 14
    
 
                                              
           |
173 | 166, 172 | mpbid 146 |
. . . . . . . . . . . . 13
    
 
                                            |
174 | 135, 155,
74, 159, 161 | caov12d 5904 |
. . . . . . . . . . . . 13
    
 
                                            |
175 | 104, 122,
155, 159, 161 | caov13d 5906 |
. . . . . . . . . . . . 13
    
 
                                            |
176 | 173, 174,
175 | 3eqtr3d 2153 |
. . . . . . . . . . . 12
    
 
                                            |
177 | 176 | adantr 272 |
. . . . . . . . . . 11
       
        
                 
       
          |
178 | | nnmcl 6329 |
. . . . . . . . . . . . . 14
 
     |
179 | 135, 74, 178 | syl2anc 406 |
. . . . . . . . . . . . 13
    
 
                                      |
180 | | nnmcl 6329 |
. . . . . . . . . . . . . 14
 
     |
181 | 122, 104,
180 | syl2anc 406 |
. . . . . . . . . . . . 13
    
 
                                      |
182 | 155, 179,
181 | 3jca 1142 |
. . . . . . . . . . . 12
    
 
                                     
    |
183 | | nnmcan 6367 |
. . . . . . . . . . . 12
     
                   |
184 | 182, 183 | sylan 279 |
. . . . . . . . . . 11
       
        
                 
       
        
       |
185 | 177, 184 | mpbid 146 |
. . . . . . . . . 10
       
        
                 
       
      |
186 | 185 | ex 114 |
. . . . . . . . 9
    
 
                                          |
187 | | 0elnn 4490 |
. . . . . . . . . 10
     |
188 | 155, 187 | syl 14 |
. . . . . . . . 9
    
 
                                      |
189 | 151, 186,
188 | mpjaod 690 |
. . . . . . . 8
    
 
                                        |
190 | 61, 65, 189 | jca32 306 |
. . . . . . 7
    
 
                                     
                    |
191 | 190 | 2eximi 1561 |
. . . . . 6
        
 
                                         
           
        |
192 | 191 | exlimivv 1848 |
. . . . 5
            
 
                                         
           
        |
193 | 192 | exlimivv 1848 |
. . . 4
                
    
                       
      
       
           
        |
194 | 193 | 2eximi 1561 |
. . 3
                    
    
                       
      
           
           
        |
195 | 59, 194 | syl 14 |
. 2
  ~Q0
~Q0             
           
        |
196 | | 19.42vvvv 1863 |
. . 3
                        
            
                         |
197 | 5 | anbi1d 458 |
. . . . . . 7
         
           |
198 | 197 | anbi1d 458 |
. . . . . 6
                                 |
199 | 198 | 4exbidv 1822 |
. . . . 5
              
   
    
                         |
200 | 4, 199 | anbi12d 462 |
. . . 4
        
                          
                             |
201 | 27 | anbi2d 457 |
. . . . 5
    
     
      |
202 | 29 | anbi2d 457 |
. . . . . . 7
         
    |