Step | Hyp | Ref
| Expression |
1 | | heibor.1 |
. . 3
     |
2 | 1 | heibor1 32142 |
. 2
       
           |
3 | | cmetmet 22256 |
. . . 4
    
      |
4 | 3 | adantr 467 |
. . 3
          
      |
5 | | metxmet 21349 |
. . . . . 6
    
       |
6 | 1 | mopntop 21455 |
. . . . . 6
        |
7 | 3, 5, 6 | 3syl 18 |
. . . . 5
    
  |
8 | 7 | adantr 467 |
. . . 4
          
  |
9 | | istotbnd 32101 |
. . . . . . . . . . . . 13
         
   


            |
10 | 9 | simprbi 466 |
. . . . . . . . . . . 12
    
   


           |
11 | | 2nn 10767 |
. . . . . . . . . . . . . . 15
 |
12 | | nnexpcl 12285 |
. . . . . . . . . . . . . . 15
 
       |
13 | 11, 12 | mpan 676 |
. . . . . . . . . . . . . 14

      |
14 | 13 | nnrpd 11339 |
. . . . . . . . . . . . 13

      |
15 | 14 | rpreccld 11351 |
. . . . . . . . . . . 12

        |
16 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
                               |
17 | 16 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . 17
               
                 |
18 | 17 | rexbidv 2901 |
. . . . . . . . . . . . . . . 16
        
       

                 |
19 | 18 | ralbidv 2827 |
. . . . . . . . . . . . . . 15
        

       


                 |
20 | 19 | anbi2d 710 |
. . . . . . . . . . . . . 14
          

          


                  |
21 | 20 | rexbidv 2901 |
. . . . . . . . . . . . 13
        
             
                      |
22 | 21 | rspccva 3149 |
. . . . . . . . . . . 12
     
 
                                      |
23 | 10, 15, 22 | syl2an 480 |
. . . . . . . . . . 11
         


                 |
24 | 23 | expcom 437 |
. . . . . . . . . 10

    
  


                  |
25 | 24 | adantl 468 |
. . . . . . . . 9
       
      


                  |
26 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
                                       |
27 | 26 | eqeq2d 2461 |
. . . . . . . . . . . . . 14
                   
                     |
28 | 27 | ac6sfi 7815 |
. . . . . . . . . . . . 13
   
                      
                     |
29 | 28 | adantrl 722 |
. . . . . . . . . . . 12
                     
       
                     |
30 | 29 | adantl 468 |
. . . . . . . . . . 11
      
 
 
 
                
       
                     |
31 | | simp3l 1036 |
. . . . . . . . . . . . . . . . . . 19
      
 
                                  |
32 | | frn 5735 |
. . . . . . . . . . . . . . . . . . 19
    
  |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      
 
                           
  |
34 | 1 | mopnuni 21456 |
. . . . . . . . . . . . . . . . . . . . 21
         |
35 | 3, 5, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
    
   |
36 | 35 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
          |
37 | 36 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . 18
      
 
                               |
38 | 33, 37 | sseqtrd 3468 |
. . . . . . . . . . . . . . . . 17
      
 
                           
   |
39 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . 20
     |
40 | 1, 39 | eqeltri 2525 |
. . . . . . . . . . . . . . . . . . 19
 |
41 | 40 | uniex 6587 |
. . . . . . . . . . . . . . . . . 18
  |
42 | 41 | elpw2 4567 |
. . . . . . . . . . . . . . . . 17
      |
43 | 38, 42 | sylibr 216 |
. . . . . . . . . . . . . . . 16
      
 
                           
    |
44 | | simp2l 1034 |
. . . . . . . . . . . . . . . . 17
      
 
                              |
45 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . 19
    
  |
46 | | dffn4 5799 |
. . . . . . . . . . . . . . . . . . 19

      |
47 | 45, 46 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
           |
48 | | fofi 7860 |
. . . . . . . . . . . . . . . . . 18
      
  |
49 | 47, 48 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
      
  |
50 | 44, 31, 49 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
      
 
                           
  |
51 | 43, 50 | elind 3618 |
. . . . . . . . . . . . . . 15
      
 
                           
      |
52 | 26 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . 20
                   
                     |
53 | 52 | rexrn 6024 |
. . . . . . . . . . . . . . . . . . 19
  
             

                     |
54 | | eliun 4283 |
. . . . . . . . . . . . . . . . . . 19
                
                 |
55 | | eliun 4283 |
. . . . . . . . . . . . . . . . . . 19
                   

                    |
56 | 53, 54, 55 | 3bitr4g 292 |
. . . . . . . . . . . . . . . . . 18
                 
                      |
57 | 56 | eqrdv 2449 |
. . . . . . . . . . . . . . . . 17
                                      |
58 | 31, 45, 57 | 3syl 18 |
. . . . . . . . . . . . . . . 16
      
 
                                            
                    |
59 | | simp3r 1037 |
. . . . . . . . . . . . . . . . 17
      
 
                            
                    |
60 | | uniiun 4331 |
. . . . . . . . . . . . . . . . . 18
   |
61 | | iuneq2 4295 |
. . . . . . . . . . . . . . . . . 18
 
                  
                     |
62 | 60, 61 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
 
                                        |
63 | 59, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
      
 
                             
                    |
64 | | simp2r 1035 |
. . . . . . . . . . . . . . . 16
      
 
                               |
65 | 58, 63, 64 | 3eqtr2rd 2492 |
. . . . . . . . . . . . . . 15
      
 
                            
                 |
66 | | iuneq1 4292 |
. . . . . . . . . . . . . . . . 17
 
                                |
67 | 66 | eqeq2d 2461 |
. . . . . . . . . . . . . . . 16
  
             
                   |
68 | 67 | rspcev 3150 |
. . . . . . . . . . . . . . 15
                       
    

                |
69 | 51, 65, 68 | syl2anc 667 |
. . . . . . . . . . . . . 14
      
 
                                  
                |
70 | 69 | 3expia 1210 |
. . . . . . . . . . . . 13
      
 
         
                   
    

                 |
71 | 70 | adantrrr 731 |
. . . . . . . . . . . 12
      
 
 
 
                
                          
    

                 |
72 | 71 | exlimdv 1779 |
. . . . . . . . . . 11
      
 
 
 
                
        
                   
    

                 |
73 | 30, 72 | mpd 15 |
. . . . . . . . . 10
      
 
 
 
                
                       |
74 | 73 | rexlimdvaa 2880 |
. . . . . . . . 9
        
                         
                 |
75 | 25, 74 | syld 45 |
. . . . . . . 8
       
                            |
76 | 75 | ralrimdva 2806 |
. . . . . . 7
    
           

                 |
77 | 41 | pwex 4586 |
. . . . . . . . 9
 
 |
78 | 77 | inex1 4544 |
. . . . . . . 8
   
 |
79 | | nn0ennn 12192 |
. . . . . . . . 9
 |
80 | | nnenom 12193 |
. . . . . . . . 9
 |
81 | 79, 80 | entri 7623 |
. . . . . . . 8
 |
82 | | iuneq1 4292 |
. . . . . . . . 9
     
              
                     |
83 | 82 | eqeq2d 2461 |
. . . . . . . 8
     
              
                       |
84 | 78, 81, 83 | axcc4 8869 |
. . . . . . 7
 
                                

                      |
85 | 76, 84 | syl6 34 |
. . . . . 6
    
                

                       |
86 | | elpwi 3960 |
. . . . . . . . . 10
 
  |
87 | | eqid 2451 |
. . . . . . . . . . . 12
         
       |
88 | | eqid 2451 |
. . . . . . . . . . . 12
    
                                       
                                    |
89 | | eqid 2451 |
. . . . . . . . . . . 12
                  
                |
90 | | simpl 459 |
. . . . . . . . . . . 12
               

                    
      |
91 | 35 | pweqd 3956 |
. . . . . . . . . . . . . . . 16
    
     |
92 | 91 | ineq1d 3633 |
. . . . . . . . . . . . . . 15
    
         |
93 | 92 | feq3d 5716 |
. . . . . . . . . . . . . 14
    
       
           |
94 | 93 | biimpar 488 |
. . . . . . . . . . . . 13
                        |
95 | 94 | adantrr 723 |
. . . . . . . . . . . 12
               

                    
         |
96 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . 19
                         
                   |
97 | 96 | cbviunv 4317 |
. . . . . . . . . . . . . . . . . 18
         
                 
        
                  |
98 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
99 | | inss1 3652 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
100 | 99, 91 | syl5sseqr 3481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       |
101 | | fss 5737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
102 | 98, 100, 101 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
                      |
103 | 102 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
104 | 103 | elpwid 3961 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
105 | 104 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . 20
       
        

       |
106 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . 20
       
        

    
  |
107 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . 21
                               |
108 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
109 | 108 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
110 | 109 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
                               |
111 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . 21
               |
112 | 107, 110,
89, 111 | ovmpt2 6432 |
. . . . . . . . . . . . . . . . . . . 20
 
                                      |
113 | 105, 106,
112 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
       
        

                                          |
114 | 113 | iuneq2dv 4300 |
. . . . . . . . . . . . . . . . . 18
                          
                 
                     |
115 | 97, 114 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
                          
                 
                     |
116 | 115 | eqeq2d 2461 |
. . . . . . . . . . . . . . . 16
                 
         
                
                       |
117 | 116 | biimprd 227 |
. . . . . . . . . . . . . . 15
                 
                                                  |
118 | 117 | ralimdva 2796 |
. . . . . . . . . . . . . 14
                 
                   
         
                    |
119 | 118 | impr 625 |
. . . . . . . . . . . . 13
               

                    
 
        
                   |
120 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
121 | 120 | iuneq1d 4303 |
. . . . . . . . . . . . . . . 16
          
                 
        
                   |
122 | | simpl 459 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
123 | 122 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
 
                             
                   |
124 | 123 | iuneq2dv 4300 |
. . . . . . . . . . . . . . . 16
          
                 
        
                   |
125 | 121, 124 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
          
                 
        
                   |
126 | 125 | eqeq2d 2461 |
. . . . . . . . . . . . . 14
 
         
                
                              |
127 | 126 | cbvralv 3019 |
. . . . . . . . . . . . 13
 
                                     
                   |
128 | 119, 127 | sylib 200 |
. . . . . . . . . . . 12
               

                    
 
        
                   |
129 | 1, 87, 88, 89, 90, 95, 128 | heiborlem10 32152 |
. . . . . . . . . . 11
                 
                      
            |
130 | 129 | exp32 610 |
. . . . . . . . . 10
               

                    

 
            |
131 | 86, 130 | syl5 33 |
. . . . . . . . 9
               

                    
   
            |
132 | 131 | ralrimiv 2800 |
. . . . . . . 8
               

                    
   
           |
133 | 132 | ex 436 |
. . . . . . 7
    
          

                                    |
134 | 133 | exlimdv 1779 |
. . . . . 6
    
                                 
   
            |
135 | 85, 134 | syld 45 |
. . . . 5
    
                     |
136 | 135 | imp 431 |
. . . 4
          
   
           |
137 | | eqid 2451 |
. . . . 5
   |
138 | 137 | iscmp 20403 |
. . . 4


   
            |
139 | 8, 136, 138 | sylanbrc 670 |
. . 3
          
  |
140 | 4, 139 | jca 535 |
. 2
          
    
   |
141 | 2, 140 | impbii 191 |
1
      
    
       |