Step | Hyp | Ref
| Expression |
1 | | blocni.u |
. . . . . 6
 |
2 | | blocnilem.1 |
. . . . . . 7
     |
3 | | blocni.8 |
. . . . . . 7
     |
4 | 2, 3 | imsxmet 26336 |
. . . . . 6
        |
5 | 1, 4 | ax-mp 5 |
. . . . 5
      |
6 | | blocni.w |
. . . . . 6
 |
7 | | eqid 2453 |
. . . . . . 7
         |
8 | | blocni.d |
. . . . . . 7
     |
9 | 7, 8 | imsxmet 26336 |
. . . . . 6
            |
10 | 6, 9 | ax-mp 5 |
. . . . 5
          |
11 | | 1rp 11313 |
. . . . . 6
 |
12 | | blocni.j |
. . . . . . 7
     |
13 | | blocni.k |
. . . . . . 7
     |
14 | 12, 13 | metcnpi3 21573 |
. . . . . 6
       
                   

                    |
15 | 11, 14 | mpanr2 691 |
. . . . 5
       
                
      
               |
16 | 5, 10, 15 | mpanl12 689 |
. . . 4
             
               |
17 | | rpreccl 11333 |
. . . . . . . . 9

    |
18 | 17 | rpred 11348 |
. . . . . . . 8

    |
19 | 18 | ad2antlr 734 |
. . . . . . 7
  
                  
 
    |
20 | | eqid 2453 |
. . . . . . . . . . . . . . . 16
         |
21 | | eqid 2453 |
. . . . . . . . . . . . . . . 16
 CV   CV   |
22 | 2, 20, 21, 3 | imsdval 26330 |
. . . . . . . . . . . . . . 15
 
       CV               |
23 | 1, 22 | mp3an1 1353 |
. . . . . . . . . . . . . 14
 
       CV               |
24 | 23 | breq1d 4415 |
. . . . . . . . . . . . 13
 
        CV                |
25 | | blocni.l |
. . . . . . . . . . . . . . . . . 18
 |
26 | | blocni.4 |
. . . . . . . . . . . . . . . . . . 19
   |
27 | 2, 7, 26 | lnof 26408 |
. . . . . . . . . . . . . . . . . 18
 
           |
28 | 1, 6, 25, 27 | mp3an 1366 |
. . . . . . . . . . . . . . . . 17
         |
29 | 28 | ffvelrni 6026 |
. . . . . . . . . . . . . . . 16
           |
30 | 28 | ffvelrni 6026 |
. . . . . . . . . . . . . . . 16
           |
31 | | eqid 2453 |
. . . . . . . . . . . . . . . . . 18
         |
32 | | eqid 2453 |
. . . . . . . . . . . . . . . . . 18
 CV   CV   |
33 | 7, 31, 32, 8 | imsdval 26330 |
. . . . . . . . . . . . . . . . 17
                                 CV                       |
34 | 6, 33 | mp3an1 1353 |
. . . . . . . . . . . . . . . 16
                  
              CV                       |
35 | 29, 30, 34 | syl2an 480 |
. . . . . . . . . . . . . . 15
 
               CV                       |
36 | 1, 6, 25 | 3pm3.2i 1187 |
. . . . . . . . . . . . . . . . 17

  |
37 | 2, 20, 31, 26 | lnosub 26412 |
. . . . . . . . . . . . . . . . 17
  
 
 
                              |
38 | 36, 37 | mpan 677 |
. . . . . . . . . . . . . . . 16
 
                               |
39 | 38 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
 
   CV                   CV                       |
40 | 35, 39 | eqtr4d 2490 |
. . . . . . . . . . . . . 14
 
               CV                   |
41 | 40 | breq1d 4415 |
. . . . . . . . . . . . 13
 
                CV                
   |
42 | 24, 41 | imbi12d 322 |
. . . . . . . . . . . 12
 
      
            
   CV               CV                     |
43 | 42 | ancoms 455 |
. . . . . . . . . . 11
 
      
            
   CV               CV                     |
44 | 43 | adantlr 722 |
. . . . . . . . . 10
  


     
            
   CV               CV                     |
45 | 44 | ralbidva 2826 |
. . . . . . . . 9
 
       
            

   CV               CV                     |
46 | | fveq2 5870 |
. . . . . . . . . . . . . 14
    
              |
47 | 46 | fveq2d 5874 |
. . . . . . . . . . . . 13
    
  CV           CV               |
48 | | fveq2 5870 |
. . . . . . . . . . . . . 14
    
  CV       CV           |
49 | 48 | oveq2d 6311 |
. . . . . . . . . . . . 13
    
     CV           CV            |
50 | 47, 49 | breq12d 4418 |
. . . . . . . . . . . 12
    
   CV        
     CV     
  CV                  CV             |
51 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
     
  |
52 | | simpll 761 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
     
  |
53 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
54 | 2, 21 | nvcl 26300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     CV       |
55 | 1, 54 | mpan 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   CV       |
56 | 55 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         CV       |
57 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
58 | 2, 57, 21 | nvgt0 26316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
  CV        |
59 | 1, 58 | mpan 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
  CV        |
60 | 59 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         CV       |
61 | 56, 60 | elrpd 11345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         CV       |
62 | | rpdivcl 11332 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    CV         CV        |
63 | 53, 61, 62 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 
     
   CV        |
64 | 63 | rpcnd 11350 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 
     
   CV        |
65 | | simprl 765 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 
     
  |
66 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
67 | 2, 66 | nvscl 26259 |
. . . . . . . . . . . . . . . . . . . . . 22
     CV           CV                |
68 | 51, 64, 65, 67 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
     
    CV                |
69 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
70 | 2, 69, 20 | nvpncan2 26289 |
. . . . . . . . . . . . . . . . . . . . 21
 
    CV                           CV                          CV                |
71 | 51, 52, 68, 70 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
            CV                          CV                |
72 | 71 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
  CV                CV                         CV        CV                 |
73 | 63 | rprege0d 11355 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
    CV         CV         |
74 | 2, 66, 21 | nvsge0 26304 |
. . . . . . . . . . . . . . . . . . . 20
      CV         CV       
  CV        CV                   CV        CV        |
75 | 51, 73, 65, 74 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
  CV        CV                   CV        CV        |
76 | | rpcn 11317 |
. . . . . . . . . . . . . . . . . . . . 21

  |
77 | 76 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
  |
78 | 55 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
     
  CV       |
79 | 78 | recnd 9674 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
  CV       |
80 | 2, 57, 21 | nvz 26310 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      CV    
       |
81 | 1, 80 | mpan 677 |
. . . . . . . . . . . . . . . . . . . . . . 23
    CV    
       |
82 | 81 | necon3bid 2670 |
. . . . . . . . . . . . . . . . . . . . . 22
    CV    
       |
83 | 82 | biimpar 488 |
. . . . . . . . . . . . . . . . . . . . 21
         CV       |
84 | 83 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
  CV       |
85 | 77, 79, 84 | divcan1d 10391 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
    CV        CV        |
86 | 72, 75, 85 | 3eqtrd 2491 |
. . . . . . . . . . . . . . . . . 18
  
 
     
  CV                CV                         |
87 | | rpre 11315 |
. . . . . . . . . . . . . . . . . . . 20

  |
88 | 87 | leidd 10187 |
. . . . . . . . . . . . . . . . . . 19

  |
89 | 88 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . 18
  
 
     
  |
90 | 86, 89 | eqbrtrd 4426 |
. . . . . . . . . . . . . . . . 17
  
 
     
  CV                CV                         |
91 | 2, 69 | nvgcl 26251 |
. . . . . . . . . . . . . . . . . . 19
 
    CV                          CV                 |
92 | 51, 52, 68, 91 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . 18
  
 
     
           CV                 |
93 | | oveq1 6302 |
. . . . . . . . . . . . . . . . . . . . . 22
            CV              
                    CV                        |
94 | 93 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . 21
            CV              
  CV               CV                CV                         |
95 | 94 | breq1d 4415 |
. . . . . . . . . . . . . . . . . . . 20
            CV              
   CV               CV                CV                      
   |
96 | 93 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . 22
            CV              
                           CV                         |
97 | 96 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . 21
            CV              
  CV                   CV                   CV                          |
98 | 97 | breq1d 4415 |
. . . . . . . . . . . . . . . . . . . 20
            CV              
   CV                
  CV                   CV                       
   |
99 | 95, 98 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . 19
            CV              
    CV               CV                
    CV                CV                         CV                   CV                       
    |
100 | 99 | rspcv 3148 |
. . . . . . . . . . . . . . . . . 18
            CV                
   CV            
  CV                
    CV                CV                      
  CV                   CV                       
    |
101 | 92, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
  
 
     
 
   CV               CV                
    CV                CV                      
  CV                   CV                       
    |
102 | 90, 101 | mpid 42 |
. . . . . . . . . . . . . . . 16
  
 
     
 
   CV               CV                
   CV                   CV                       
   |
103 | 28 | ffvelrni 6026 |
. . . . . . . . . . . . . . . . . . . 20
           |
104 | 7, 32 | nvcl 26300 |
. . . . . . . . . . . . . . . . . . . 20
          
  CV           |
105 | 6, 103, 104 | sylancr 670 |
. . . . . . . . . . . . . . . . . . 19
   CV           |
106 | 105 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . 18
  
 
     
  CV           |
107 | | 1red 9663 |
. . . . . . . . . . . . . . . . . 18
  
 
     
  |
108 | 106, 107,
63 | lemuldiv2d 11395 |
. . . . . . . . . . . . . . . . 17
  
 
     
     CV        CV         
  CV        
    CV          |
109 | 71 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
     
               CV                              CV                 |
110 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
111 | 2, 66, 110, 26 | lnomul 26413 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
     CV               CV                   CV                    |
112 | 36, 111 | mpan 677 |
. . . . . . . . . . . . . . . . . . . . . 22
     CV              CV                   CV                    |
113 | 64, 65, 112 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
     
       CV                   CV                    |
114 | 109, 113 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
               CV                           CV                    |
115 | 114 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
  CV                   CV                          CV        CV                     |
116 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
  |
117 | 103 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
          |
118 | 7, 110, 32 | nvsge0 26304 |
. . . . . . . . . . . . . . . . . . . 20
      CV         CV                  CV        CV                       CV        CV            |
119 | 116, 73, 117, 118 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
  CV        CV                       CV        CV            |
120 | 115, 119 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . 18
  
 
     
  CV                   CV                            CV        CV            |
121 | 120 | breq1d 4415 |
. . . . . . . . . . . . . . . . 17
  
 
     
   CV                   CV                       
    CV        CV             |
122 | | rpcnne0 11326 |
. . . . . . . . . . . . . . . . . . . . 21

    |
123 | | rpcnne0 11326 |
. . . . . . . . . . . . . . . . . . . . 21
   CV        CV       CV        |
124 | | recdiv 10320 |
. . . . . . . . . . . . . . . . . . . . 21
       CV       CV           CV          CV        |
125 | 122, 123,
124 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
    CV          CV          CV        |
126 | 53, 61, 125 | syl2an 480 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
    CV          CV        |
127 | | rpne0 11324 |
. . . . . . . . . . . . . . . . . . . . 21

  |
128 | 127 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . . . 20
  
 
     
  |
129 | 79, 77, 128 | divrec2d 10394 |
. . . . . . . . . . . . . . . . . . 19
  
 
     
   CV           CV        |
130 | 126, 129 | eqtr2d 2488 |
. . . . . . . . . . . . . . . . . 18
  
 
     
     CV          CV         |
131 | 130 | breq2d 4417 |
. . . . . . . . . . . . . . . . 17
  
 
     
   CV        
     CV     
  CV        
    CV          |
132 | 108, 121,
131 | 3bitr4d 289 |
. . . . . . . . . . . . . . . 16
  
 
     
   CV                   CV                       
  CV        
     CV         |
133 | 102, 132 | sylibd 218 |
. . . . . . . . . . . . . . 15
  
 
     
 
   CV               CV                
   CV        
     CV         |
134 | 133 | anassrs 654 |
. . . . . . . . . . . . . 14
    
       
   CV            
  CV                
   CV        
     CV         |
135 | 134 | imp 431 |
. . . . . . . . . . . . 13
            
   CV               CV                
 
  CV        
     CV        |
136 | 135 | an32s 814 |
. . . . . . . . . . . 12
       
   CV               CV                
         CV        
     CV        |
137 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . 19
         |
138 | 2, 7, 57, 137, 26 | lno0 26409 |
. . . . . . . . . . . . . . . . . 18
 
               |
139 | 1, 6, 25, 138 | mp3an 1366 |
. . . . . . . . . . . . . . . . 17
             |
140 | 139 | fveq2i 5873 |
. . . . . . . . . . . . . . . 16
  CV               CV          |
141 | 137, 32 | nvz0 26309 |
. . . . . . . . . . . . . . . . 17
   CV           |
142 | 6, 141 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
  CV          |
143 | 140, 142 | eqtri 2475 |
. . . . . . . . . . . . . . 15
  CV              |
144 | | 0le0 10706 |
. . . . . . . . . . . . . . 15
 |
145 | 143, 144 | eqbrtri 4425 |
. . . . . . . . . . . . . 14
  CV              |
146 | 17 | rpcnd 11350 |
. . . . . . . . . . . . . . 15

    |
147 | 57, 21 | nvz0 26309 |
. . . . . . . . . . . . . . . . . 18
   CV           |
148 | 1, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
  CV          |
149 | 148 | oveq2i 6306 |
. . . . . . . . . . . . . . . 16
     CV               |
150 | | mul01 9817 |
. . . . . . . . . . . . . . . 16
         |
151 | 149, 150 | syl5eq 2499 |
. . . . . . . . . . . . . . 15
        CV            |
152 | 146, 151 | syl 17 |
. . . . . . . . . . . . . 14

     CV            |
153 | 145, 152 | syl5breqr 4442 |
. . . . . . . . . . . . 13

  CV                  CV            |
154 | 153 | ad3antlr 738 |
. . . . . . . . . . . 12
    
 
   CV               CV                
 
  CV                  CV            |
155 | 50, 136, 154 | pm2.61ne 2711 |
. . . . . . . . . . 11
    
 
   CV               CV                
 
  CV        
     CV        |
156 | 155 | ex 436 |
. . . . . . . . . 10
  


 
   CV               CV                
   CV        
     CV         |
157 | 156 | ralrimdva 2808 |
. . . . . . . . 9
 
      CV               CV                  
  CV        
     CV         |
158 | 45, 157 | sylbid 219 |
. . . . . . . 8
 
       
             
  CV        
     CV         |
159 | 158 | imp 431 |
. . . . . . 7
  
                  
 

  CV        
     CV        |
160 | | oveq1 6302 |
. . . . . . . . . 10
      CV           CV        |
161 | 160 | breq2d 4417 |
. . . . . . . . 9
      CV            CV     
  CV        
     CV         |
162 | 161 | ralbidv 2829 |
. . . . . . . 8
    
  CV            CV     

  CV        
     CV         |
163 | 162 | rspcev 3152 |
. . . . . . 7
       CV        
     CV       
   CV        
   CV        |
164 | 19, 159, 163 | syl2anc 667 |
. . . . . 6
  
                  
 
    CV        
   CV        |
165 | 164 | ex 436 |
. . . . 5
 
       
                 CV        
   CV         |
166 | 165 | rexlimdva 2881 |
. . . 4
  

                  
   CV        
   CV         |
167 | 16, 166 | syl5 33 |
. . 3
 
          CV        
   CV         |
168 | 167 | imp 431 |
. 2
 
       
   CV        
   CV        |
169 | | blocni.5 |
. . . 4
   |
170 | 2, 21, 32, 26, 169, 1, 6 | isblo3i 26454 |
. . 3


    CV        
   CV         |
171 | 25, 170 | mpbiran 930 |
. 2

    CV        
   CV        |
172 | 168, 171 | sylibr 216 |
1
 
      
  |