Step | Hyp | Ref
| Expression |
1 | | heibor.1 |
. . 3
     |
2 | 1 | heibor1 32206 |
. 2
       
           |
3 | | cmetmet 22334 |
. . . 4
    
      |
4 | 3 | adantr 472 |
. . 3
          
      |
5 | | metxmet 21427 |
. . . . . 6
    
       |
6 | 1 | mopntop 21533 |
. . . . . 6
        |
7 | 3, 5, 6 | 3syl 18 |
. . . . 5
    
  |
8 | 7 | adantr 472 |
. . . 4
          
  |
9 | | istotbnd 32165 |
. . . . . . . . . . . . 13
         
   


            |
10 | 9 | simprbi 471 |
. . . . . . . . . . . 12
    
   


           |
11 | | 2nn 10790 |
. . . . . . . . . . . . . . 15
 |
12 | | nnexpcl 12323 |
. . . . . . . . . . . . . . 15
 
       |
13 | 11, 12 | mpan 684 |
. . . . . . . . . . . . . 14

      |
14 | 13 | nnrpd 11362 |
. . . . . . . . . . . . 13

      |
15 | 14 | rpreccld 11374 |
. . . . . . . . . . . 12

        |
16 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                               |
17 | 16 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . 17
               
                 |
18 | 17 | rexbidv 2892 |
. . . . . . . . . . . . . . . 16
        
       

                 |
19 | 18 | ralbidv 2829 |
. . . . . . . . . . . . . . 15
        

       


                 |
20 | 19 | anbi2d 718 |
. . . . . . . . . . . . . 14
          

          


                  |
21 | 20 | rexbidv 2892 |
. . . . . . . . . . . . 13
        
             
                      |
22 | 21 | rspccva 3135 |
. . . . . . . . . . . 12
     
 
                                      |
23 | 10, 15, 22 | syl2an 485 |
. . . . . . . . . . 11
         


                 |
24 | 23 | expcom 442 |
. . . . . . . . . 10

    
  


                  |
25 | 24 | adantl 473 |
. . . . . . . . 9
       
      


                  |
26 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
                                       |
27 | 26 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
                   
                     |
28 | 27 | ac6sfi 7833 |
. . . . . . . . . . . . 13
   
                      
                     |
29 | 28 | adantrl 730 |
. . . . . . . . . . . 12
                     
       
                     |
30 | 29 | adantl 473 |
. . . . . . . . . . 11
      
 
 
 
                
       
                     |
31 | | simp3l 1058 |
. . . . . . . . . . . . . . . . . . 19
      
 
                                  |
32 | | frn 5747 |
. . . . . . . . . . . . . . . . . . 19
    
  |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      
 
                           
  |
34 | 1 | mopnuni 21534 |
. . . . . . . . . . . . . . . . . . . . 21
         |
35 | 3, 5, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
    
   |
36 | 35 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
          |
37 | 36 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . 18
      
 
                               |
38 | 33, 37 | sseqtrd 3454 |
. . . . . . . . . . . . . . . . 17
      
 
                           
   |
39 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . 20
     |
40 | 1, 39 | eqeltri 2545 |
. . . . . . . . . . . . . . . . . . 19
 |
41 | 40 | uniex 6606 |
. . . . . . . . . . . . . . . . . 18
  |
42 | 41 | elpw2 4565 |
. . . . . . . . . . . . . . . . 17
      |
43 | 38, 42 | sylibr 217 |
. . . . . . . . . . . . . . . 16
      
 
                           
    |
44 | | simp2l 1056 |
. . . . . . . . . . . . . . . . 17
      
 
                              |
45 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . 19
    
  |
46 | | dffn4 5812 |
. . . . . . . . . . . . . . . . . . 19

      |
47 | 45, 46 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
           |
48 | | fofi 7878 |
. . . . . . . . . . . . . . . . . 18
      
  |
49 | 47, 48 | sylan2 482 |
. . . . . . . . . . . . . . . . 17
      
  |
50 | 44, 31, 49 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
      
 
                           
  |
51 | 43, 50 | elind 3609 |
. . . . . . . . . . . . . . 15
      
 
                           
      |
52 | 26 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . . 20
                   
                     |
53 | 52 | rexrn 6039 |
. . . . . . . . . . . . . . . . . . 19
  
             

                     |
54 | | eliun 4274 |
. . . . . . . . . . . . . . . . . . 19
                
                 |
55 | | eliun 4274 |
. . . . . . . . . . . . . . . . . . 19
                   

                    |
56 | 53, 54, 55 | 3bitr4g 296 |
. . . . . . . . . . . . . . . . . 18
                 
                      |
57 | 56 | eqrdv 2469 |
. . . . . . . . . . . . . . . . 17
                                      |
58 | 31, 45, 57 | 3syl 18 |
. . . . . . . . . . . . . . . 16
      
 
                                            
                    |
59 | | simp3r 1059 |
. . . . . . . . . . . . . . . . 17
      
 
                            
                    |
60 | | uniiun 4322 |
. . . . . . . . . . . . . . . . . 18
   |
61 | | iuneq2 4286 |
. . . . . . . . . . . . . . . . . 18
 
                  
                     |
62 | 60, 61 | syl5eq 2517 |
. . . . . . . . . . . . . . . . 17
 
                                        |
63 | 59, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
      
 
                             
                    |
64 | | simp2r 1057 |
. . . . . . . . . . . . . . . 16
      
 
                               |
65 | 58, 63, 64 | 3eqtr2rd 2512 |
. . . . . . . . . . . . . . 15
      
 
                            
                 |
66 | | iuneq1 4283 |
. . . . . . . . . . . . . . . . 17
 
                                |
67 | 66 | eqeq2d 2481 |
. . . . . . . . . . . . . . . 16
  
             
                   |
68 | 67 | rspcev 3136 |
. . . . . . . . . . . . . . 15
                       
    

                |
69 | 51, 65, 68 | syl2anc 673 |
. . . . . . . . . . . . . 14
      
 
                                  
                |
70 | 69 | 3expia 1233 |
. . . . . . . . . . . . 13
      
 
         
                   
    

                 |
71 | 70 | adantrrr 739 |
. . . . . . . . . . . 12
      
 
 
 
                
                          
    

                 |
72 | 71 | exlimdv 1787 |
. . . . . . . . . . 11
      
 
 
 
                
        
                   
    

                 |
73 | 30, 72 | mpd 15 |
. . . . . . . . . 10
      
 
 
 
                
                       |
74 | 73 | rexlimdvaa 2872 |
. . . . . . . . 9
        
                         
                 |
75 | 25, 74 | syld 44 |
. . . . . . . 8
       
                            |
76 | 75 | ralrimdva 2812 |
. . . . . . 7
    
           

                 |
77 | 41 | pwex 4584 |
. . . . . . . . 9
 
 |
78 | 77 | inex1 4537 |
. . . . . . . 8
   
 |
79 | | nn0ennn 12230 |
. . . . . . . . 9
 |
80 | | nnenom 12231 |
. . . . . . . . 9
 |
81 | 79, 80 | entri 7641 |
. . . . . . . 8
 |
82 | | iuneq1 4283 |
. . . . . . . . 9
     
              
                     |
83 | 82 | eqeq2d 2481 |
. . . . . . . 8
     
              
                       |
84 | 78, 81, 83 | axcc4 8887 |
. . . . . . 7
 
                                

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

                       |
86 | | elpwi 3951 |
. . . . . . . . . 10
 
  |
87 | | eqid 2471 |
. . . . . . . . . . . 12
         
       |
88 | | eqid 2471 |
. . . . . . . . . . . 12
    
                                       
                                    |
89 | | eqid 2471 |
. . . . . . . . . . . 12
                  
                |
90 | | simpl 464 |
. . . . . . . . . . . 12
               

                    
      |
91 | 35 | pweqd 3947 |
. . . . . . . . . . . . . . . 16
    
     |
92 | 91 | ineq1d 3624 |
. . . . . . . . . . . . . . 15
    
         |
93 | 92 | feq3d 5726 |
. . . . . . . . . . . . . 14
    
       
           |
94 | 93 | biimpar 493 |
. . . . . . . . . . . . 13
                        |
95 | 94 | adantrr 731 |
. . . . . . . . . . . 12
               

                    
         |
96 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . 19
                         
                   |
97 | 96 | cbviunv 4308 |
. . . . . . . . . . . . . . . . . 18
         
                 
        
                  |
98 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
99 | | inss1 3643 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
100 | 99, 91 | syl5sseqr 3467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       |
101 | | fss 5749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
102 | 98, 100, 101 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
                      |
103 | 102 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
104 | 103 | elpwid 3952 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
105 | 104 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . 20
       
        

       |
106 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . 20
       
        

    
  |
107 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . 21
                               |
108 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
109 | 108 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
110 | 109 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . 21
                               |
111 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . 21
               |
112 | 107, 110,
89, 111 | ovmpt2 6451 |
. . . . . . . . . . . . . . . . . . . 20
 
                                      |
113 | 105, 106,
112 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
       
        

                                          |
114 | 113 | iuneq2dv 4291 |
. . . . . . . . . . . . . . . . . 18
                          
                 
                     |
115 | 97, 114 | syl5eq 2517 |
. . . . . . . . . . . . . . . . 17
                          
                 
                     |
116 | 115 | eqeq2d 2481 |
. . . . . . . . . . . . . . . 16
                 
         
                
                       |
117 | 116 | biimprd 231 |
. . . . . . . . . . . . . . 15
                 
                                                  |
118 | 117 | ralimdva 2805 |
. . . . . . . . . . . . . 14
                 
                   
         
                    |
119 | 118 | impr 631 |
. . . . . . . . . . . . 13
               

                    
 
        
                   |
120 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
           |
121 | 120 | iuneq1d 4294 |
. . . . . . . . . . . . . . . 16
          
                 
        
                   |
122 | | simpl 464 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
123 | 122 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
 
                             
                   |
124 | 123 | iuneq2dv 4291 |
. . . . . . . . . . . . . . . 16
          
                 
        
                   |
125 | 121, 124 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
          
                 
        
                   |
126 | 125 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
 
         
                
                              |
127 | 126 | cbvralv 3005 |
. . . . . . . . . . . . 13
 
                                     
                   |
128 | 119, 127 | sylib 201 |
. . . . . . . . . . . 12
               

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

                    

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

                    
   
            |
132 | 131 | ralrimiv 2808 |
. . . . . . . 8
               

                    
   
           |
133 | 132 | ex 441 |
. . . . . . 7
    
          

                                    |
134 | 133 | exlimdv 1787 |
. . . . . 6
    
                                 
   
            |
135 | 85, 134 | syld 44 |
. . . . 5
    
                     |
136 | 135 | imp 436 |
. . . 4
          
   
           |
137 | | eqid 2471 |
. . . . 5
   |
138 | 137 | iscmp 20480 |
. . . 4


   
            |
139 | 8, 136, 138 | sylanbrc 677 |
. . 3
          
  |
140 | 4, 139 | jca 541 |
. 2
          
    
   |
141 | 2, 140 | impbii 192 |
1
      
    
       |