Step | Hyp | Ref
| Expression |
1 | | eliun 4274 |
. . . . . . . . 9
          
            |
2 | 1 | biimpi 199 |
. . . . . . . 8
                       |
3 | 2 | adantl 473 |
. . . . . . 7
 
          
            |
4 | | iundjiun.nph |
. . . . . . . . 9
   |
5 | | nfcv 2612 |
. . . . . . . . . 10
   |
6 | | nfiu1 4299 |
. . . . . . . . . 10
  
          |
7 | 5, 6 | nfel 2624 |
. . . . . . . . 9

           |
8 | | simp2 1031 |
. . . . . . . . . . . 12
 
        
      |
9 | | simpl 464 |
. . . . . . . . . . . . . . 15
 
    
  |
10 | | elfzuz 11822 |
. . . . . . . . . . . . . . . . 17
           |
11 | | iundjiun.z |
. . . . . . . . . . . . . . . . . 18
     |
12 | 11 | eqcomi 2480 |
. . . . . . . . . . . . . . . . 17
     |
13 | 10, 12 | syl6eleq 2559 |
. . . . . . . . . . . . . . . 16
       |
14 | 13 | adantl 473 |
. . . . . . . . . . . . . . 15
 
    
  |
15 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
 
   |
16 | | iundjiun.e |
. . . . . . . . . . . . . . . . . . 19
       |
17 | 16 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . 18
 
       |
18 | | difexg 4545 |
. . . . . . . . . . . . . . . . . 18
         
  ..^         |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
     
  ..^         |
20 | | iundjiun.f |
. . . . . . . . . . . . . . . . . 18
      
 ..^         |
21 | 20 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . 17
       
 ..^                   ..^         |
22 | 15, 19, 21 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
 
          
 ..^         |
23 | | difssd 3550 |
. . . . . . . . . . . . . . . 16
 
     
  ..^             |
24 | 22, 23 | eqsstrd 3452 |
. . . . . . . . . . . . . . 15
 
           |
25 | 9, 14, 24 | syl2anc 673 |
. . . . . . . . . . . . . 14
 
    
          |
26 | 25 | 3adant3 1050 |
. . . . . . . . . . . . 13
 
        
          |
27 | | simp3 1032 |
. . . . . . . . . . . . 13
 
        
      |
28 | 26, 27 | sseldd 3419 |
. . . . . . . . . . . 12
 
        
      |
29 | | rspe 2844 |
. . . . . . . . . . . 12
     
     
           |
30 | 8, 28, 29 | syl2anc 673 |
. . . . . . . . . . 11
 
        
            |
31 | | eliun 4274 |
. . . . . . . . . . 11
          
            |
32 | 30, 31 | sylibr 217 |
. . . . . . . . . 10
 
        
            |
33 | 32 | 3exp 1230 |
. . . . . . . . 9
          
              |
34 | 4, 7, 33 | rexlimd 2866 |
. . . . . . . 8
            
            |
35 | 34 | adantr 472 |
. . . . . . 7
 
          
 
        
             |
36 | 3, 35 | mpd 15 |
. . . . . 6
 
          
            |
37 | 36 | ralrimiva 2809 |
. . . . 5
 
                      |
38 | | dfss3 3408 |
. . . . 5
 
                   
                      |
39 | 37, 38 | sylibr 217 |
. . . 4
          
            |
40 | | fzssuz 11865 |
. . . . . . . . . . 11
         |
41 | 40 | a1i 11 |
. . . . . . . . . 10
                     |
42 | 31 | biimpi 199 |
. . . . . . . . . 10
                       |
43 | | nfv 1769 |
. . . . . . . . . . 11

     |
44 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
45 | 44 | eleq2d 2534 |
. . . . . . . . . . 11
     
       |
46 | 43, 45 | uzwo4 37451 |
. . . . . . . . . 10
     
    
                    
      
        |
47 | 41, 42, 46 | syl2anc 673 |
. . . . . . . . 9
                     
      
        |
48 | 47 | adantl 473 |
. . . . . . . 8
 
          
          
      
        |
49 | | simprl 772 |
. . . . . . . . . . . . . 14
                   
      
      |
50 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
         |
51 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . . 19
               |
52 | 50, 51 | nfan 2031 |
. . . . . . . . . . . . . . . . . 18
   
           
       |
53 | | elfzoelz 11947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
  |
54 | 53 | zred 11063 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
  |
55 | 54 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 ..^    |
56 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
57 | 56 | zred 11063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
58 | 57 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 ..^ 
  |
59 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 ..^    |
60 | 58, 59 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 ..^      |
61 | | elfzolem1 37631 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
    |
62 | 61 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 ..^ 
    |
63 | 58 | ltm1d 10561 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 ..^      |
64 | 55, 60, 58, 62, 63 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . . . 21
     
 ..^ 
  |
65 | 64 | ad4ant24 1264 |
. . . . . . . . . . . . . . . . . . . 20
   
           
       ..^ 
  |
66 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . 22
             
     
 ..^  
     
       |
67 | | elfzel1 11825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
68 | 67 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 ..^ 
  |
69 | | elfzel2 11824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
70 | 69 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 ..^ 
  |
71 | 53 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 ..^    |
72 | 68, 70, 71 | 3jca 1210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 ..^  
   |
73 | | elfzole1 11955 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^
  |
74 | 73 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 ..^    |
75 | 70 | zred 11063 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 ..^ 
  |
76 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
77 | 57, 76 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
78 | 69 | zred 11063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
79 | 57 | ltm1d 10561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
80 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
81 | 77, 57, 78, 79, 80 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
82 | 81 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
 ..^      |
83 | 55, 60, 75, 62, 82 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 ..^ 
  |
84 | 55, 75, 83 | ltled 9800 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 ..^ 
  |
85 | 72, 74, 84 | jca32 544 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
 ..^          |
86 | | elfz2 11817 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
 
      |
87 | 85, 86 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 ..^        |
88 | 87 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
             
     
 ..^        |
89 | | rspa 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
       |
90 | 66, 88, 89 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
             
     
 ..^          |
91 | 90 | adantlll 732 |
. . . . . . . . . . . . . . . . . . . 20
   
           
       ..^ 

       |
92 | 65, 91 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
   
           
       ..^ 
      |
93 | 92 | ex 441 |
. . . . . . . . . . . . . . . . . 18
        
     
        ..^
       |
94 | 52, 93 | ralrimi 2800 |
. . . . . . . . . . . . . . . . 17
        
     
        ..^       |
95 | | ralnex 2834 |
. . . . . . . . . . . . . . . . 17
 
 ..^    
  ..^        |
96 | 94, 95 | sylib 201 |
. . . . . . . . . . . . . . . 16
        
     
     
  ..^        |
97 | | eliun 4274 |
. . . . . . . . . . . . . . . 16
   ..^        ..^        |
98 | 96, 97 | sylnibr 312 |
. . . . . . . . . . . . . . 15
        
     
     
  ..^        |
99 | 98 | adantrl 730 |
. . . . . . . . . . . . . 14
                   
      
  ..^        |
100 | 49, 99 | eldifd 3401 |
. . . . . . . . . . . . 13
                   
      
       ..^         |
101 | 14, 22 | syldan 478 |
. . . . . . . . . . . . . . 15
 
    
        
  ..^         |
102 | 101 | eqcomd 2477 |
. . . . . . . . . . . . . 14
 
    
       ..^             |
103 | 102 | adantr 472 |
. . . . . . . . . . . . 13
                   
            
 ..^             |
104 | 100, 103 | eleqtrd 2551 |
. . . . . . . . . . . 12
                   
      
      |
105 | 104 | ex 441 |
. . . . . . . . . . 11
 
    
            
             |
106 | 105 | ex 441 |
. . . . . . . . . 10
            
     
              |
107 | 4, 106 | reximdai 2853 |
. . . . . . . . 9
            
      
      
            |
108 | 107 | adantr 472 |
. . . . . . . 8
 
          
 
          
     
                   |
109 | 48, 108 | mpd 15 |
. . . . . . 7
 
          
            |
110 | 109, 1 | sylibr 217 |
. . . . . 6
 
          
            |
111 | 110 | ralrimiva 2809 |
. . . . 5
 
                      |
112 | | dfss3 3408 |
. . . . 5
 
                   
                      |
113 | 111, 112 | sylibr 217 |
. . . 4
          
            |
114 | 39, 113 | eqssd 3435 |
. . 3
                       |
115 | 114 | ralrimivw 2810 |
. 2
                        |
116 | 11 | iuneqfzuz 37645 |
. . 3
 
          
         
           |
117 | 115, 116 | syl 17 |
. 2
             |
118 | | fveq2 5879 |
. . . . . . . . . . . . . 14
           |
119 | | oveq2 6316 |
. . . . . . . . . . . . . . 15
  ..^  ..^   |
120 | 119 | iuneq1d 4294 |
. . . . . . . . . . . . . 14
   ..^        ..^        |
121 | 118, 120 | difeq12d 3541 |
. . . . . . . . . . . . 13
     
  ..^           
  ..^         |
122 | 121 | cbvmptv 4488 |
. . . . . . . . . . . 12
        ..^             
  ..^         |
123 | 20, 122 | eqtri 2493 |
. . . . . . . . . . 11
      
 ..^         |
124 | | simpllr 777 |
. . . . . . . . . . 11
   



  |
125 | | simplr 770 |
. . . . . . . . . . 11
   



  |
126 | | simpr 468 |
. . . . . . . . . . 11
   



  |
127 | 11, 123, 124, 125, 126 | iundjiunlem 38413 |
. . . . . . . . . 10
   



            |
128 | 127 | adantlr 729 |
. . . . . . . . 9
      
              |
129 | | simpll 768 |
. . . . . . . . . 10
      

       |
130 | | neqne 2651 |
. . . . . . . . . . . 12
   |
131 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
132 | 131, 11 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . 17
       |
133 | | eluzelz 11192 |
. . . . . . . . . . . . . . . . 17
    
  |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
135 | 134 | zred 11063 |
. . . . . . . . . . . . . . 15
   |
136 | 135 | adantl 473 |
. . . . . . . . . . . . . 14
 
   |
137 | 136 | ad2antrr 740 |
. . . . . . . . . . . . 13
         |
138 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
139 | 138, 11 | syl6eleq 2559 |
. . . . . . . . . . . . . . . 16
       |
140 | | eluzelz 11192 |
. . . . . . . . . . . . . . . 16
    
  |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . 15
   |
142 | 141 | zred 11063 |
. . . . . . . . . . . . . 14
   |
143 | 142 | ad3antrrr 744 |
. . . . . . . . . . . . 13
      
  |
144 | | simpr 468 |
. . . . . . . . . . . . . . 15
  

   |
145 | 136 | adantr 472 |
. . . . . . . . . . . . . . . 16
  

   |
146 | 142 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
  

   |
147 | 145, 146 | lenltd 9798 |
. . . . . . . . . . . . . . 15
  

 
   |
148 | 144, 147 | mpbird 240 |
. . . . . . . . . . . . . 14
  

   |
149 | 148 | adantlr 729 |
. . . . . . . . . . . . 13
      
  |
150 | | simplr 770 |
. . . . . . . . . . . . 13
         |
151 | 137, 143,
149, 150 | leneltd 9806 |
. . . . . . . . . . . 12
      
  |
152 | 130, 151 | sylanl2 663 |
. . . . . . . . . . 11
    
 
  |
153 | 152 | ad5ant2345 1283 |
. . . . . . . . . 10
      

   |
154 | | anass 661 |
. . . . . . . . . . 11
    
 
    |
155 | | incom 3616 |
. . . . . . . . . . . . 13
                     |
156 | 155 | a1i 11 |
. . . . . . . . . . . 12
   
 

              
       |
157 | | simplrr 779 |
. . . . . . . . . . . . 13
   
 

  |
158 | | simplrl 778 |
. . . . . . . . . . . . 13
   
 

  |
159 | | simpr 468 |
. . . . . . . . . . . . 13
   
 

  |
160 | 11, 123, 157, 158, 159 | iundjiunlem 38413 |
. . . . . . . . . . . 12
   
 

            |
161 | 156, 160 | eqtrd 2505 |
. . . . . . . . . . 11
   
 

            |
162 | 154, 161 | sylanb 480 |
. . . . . . . . . 10
   



            |
163 | 129, 153,
162 | syl2anc 673 |
. . . . . . . . 9
      

             |
164 | 128, 163 | pm2.61dan 808 |
. . . . . . . 8
   


             |
165 | 164 | ex 441 |
. . . . . . 7
     
             |
166 | | df-or 377 |
. . . . . . 7
            

    
        |
167 | 165, 166 | sylibr 217 |
. . . . . 6
                   |
168 | 167 | ralrimiva 2809 |
. . . . 5
 
 

    
        |
169 | 168 | ex 441 |
. . . 4
   
              |
170 | 4, 169 | ralrimi 2800 |
. . 3
  

             |
171 | | nfcv 2612 |
. . . . 5
       |
172 | | nfmpt1 4485 |
. . . . . . 7
        
 ..^         |
173 | 20, 172 | nfcxfr 2610 |
. . . . . 6
   |
174 | | nfcv 2612 |
. . . . . 6
   |
175 | 173, 174 | nffv 5886 |
. . . . 5
       |
176 | | fveq2 5879 |
. . . . 5
           |
177 | 171, 175,
176 | cbvdisj 4376 |
. . . 4
Disj
   
Disj       |
178 | | fveq2 5879 |
. . . . 5
           |
179 | 178 | disjor 4380 |
. . . 4
Disj
   



    
        |
180 | | nfcv 2612 |
. . . . . 6
   |
181 | | nfv 1769 |
. . . . . . 7

 |
182 | | nfcv 2612 |
. . . . . . . . . 10
   |
183 | 173, 182 | nffv 5886 |
. . . . . . . . 9
       |
184 | 175, 183 | nfin 3630 |
. . . . . . . 8
             |
185 | | nfcv 2612 |
. . . . . . . 8
   |
186 | 184, 185 | nfeq 2623 |
. . . . . . 7
             |
187 | 181, 186 | nfor 2038 |
. . . . . 6
               |
188 | 180, 187 | nfral 2789 |
. . . . 5
  

            |
189 | | nfv 1769 |
. . . . 5
  

            |
190 | | equequ1 1875 |
. . . . . . 7
 
   |
191 | | fveq2 5879 |
. . . . . . . . 9
           |
192 | 191 | ineq1d 3624 |
. . . . . . . 8
     
                 |
193 | 192 | eqeq1d 2473 |
. . . . . . 7
           
             |
194 | 190, 193 | orbi12d 724 |
. . . . . 6
                             |
195 | 194 | ralbidv 2829 |
. . . . 5
  

          


    
         |
196 | 188, 189,
195 | cbvral 3001 |
. . . 4
 

           



    
        |
197 | 177, 179,
196 | 3bitri 279 |
. . 3
Disj
   



    
        |
198 | 170, 197 | sylibr 217 |
. 2
 Disj
      |
199 | 115, 117,
198 | jca31 543 |
1
   
          
                    Disj        |