Step | Hyp | Ref
| Expression |
1 | | 1rp 11329 |
. . . 4
 |
2 | 1 | ne0ii 3729 |
. . 3
 |
3 | | ral0 3865 |
. . . . 5
           |
4 | | simpr 468 |
. . . . . 6
 

  |
5 | 4 | raleqdv 2979 |
. . . . 5
 

 

                     |
6 | 3, 5 | mpbiri 241 |
. . . 4
 



          |
7 | 6 | ralrimivw 2810 |
. . 3
 

             |
8 | | r19.2z 3849 |
. . 3
 



        
             |
9 | 2, 7, 8 | sylancr 676 |
. 2
 

             |
10 | | lebnum.j |
. . . . . . 7
     |
11 | | lebnum.d |
. . . . . . 7
       |
12 | | lebnum.c |
. . . . . . 7
   |
13 | | lebnum.s |
. . . . . . 7

  |
14 | | lebnum.u |
. . . . . . 7
    |
15 | | lebnumlem1OLD.u |
. . . . . . 7
   |
16 | | lebnumlem1OLD.n |
. . . . . . 7
   |
17 | | lebnumlem1OLD.f |
. . . . . . 7
                |
18 | 10, 11, 12, 13, 14, 15, 16, 17 | lebnumlem1OLD 22070 |
. . . . . 6
       |
19 | 18 | adantr 472 |
. . . . 5
 

      |
20 | | frn 5747 |
. . . . 5
    
  |
21 | 19, 20 | syl 17 |
. . . 4
 

  |
22 | | eqid 2471 |
. . . . . . 7
   |
23 | | lebnumlem2OLD.k |
. . . . . . 7
     |
24 | 12 | adantr 472 |
. . . . . . 7
 

  |
25 | 10, 11, 12, 13, 14, 15, 16, 17, 23 | lebnumlem2OLD 22071 |
. . . . . . . 8
     |
26 | 25 | adantr 472 |
. . . . . . 7
 


   |
27 | | metxmet 21427 |
. . . . . . . . . 10
    
       |
28 | 10 | mopnuni 21534 |
. . . . . . . . . 10
         |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . 9
    |
30 | 29 | neeq1d 2702 |
. . . . . . . 8
 
    |
31 | 30 | biimpa 492 |
. . . . . . 7
 

   |
32 | 22, 23, 24, 26, 31 | evth2 22066 |
. . . . . 6
 

                |
33 | 29 | adantr 472 |
. . . . . . 7
 

   |
34 | | raleq 2973 |
. . . . . . . 8
                  
       |
35 | 34 | rexeqbi1dv 2982 |
. . . . . . 7
                
     
       |
36 | 33, 35 | syl 17 |
. . . . . 6
 

 

                         |
37 | 32, 36 | mpbird 240 |
. . . . 5
 



          |
38 | | ffn 5739 |
. . . . . 6
       |
39 | | breq1 4398 |
. . . . . . . 8
     
   
           |
40 | 39 | ralbidv 2829 |
. . . . . . 7
      
   

           |
41 | 40 | rexrn 6039 |
. . . . . 6
  
     


           |
42 | 19, 38, 41 | 3syl 18 |
. . . . 5
 

 
 
     
           |
43 | 37, 42 | mpbird 240 |
. . . 4
 

  
      |
44 | | ssrexv 3480 |
. . . 4

 
               |
45 | 21, 43, 44 | sylc 61 |
. . 3
 

        |
46 | | simpr 468 |
. . . . . 6
       |
47 | 14 | ad2antrr 740 |
. . . . . . . . . 10
        |
48 | | simplr 770 |
. . . . . . . . . 10
       |
49 | 47, 48 | eqnetrrd 2711 |
. . . . . . . . 9
        |
50 | | unieq 4198 |
. . . . . . . . . . 11

    |
51 | | uni0 4217 |
. . . . . . . . . . 11
  |
52 | 50, 51 | syl6eq 2521 |
. . . . . . . . . 10

   |
53 | 52 | necon3i 2675 |
. . . . . . . . 9
 
  |
54 | 49, 53 | syl 17 |
. . . . . . . 8
       |
55 | 15 | ad2antrr 740 |
. . . . . . . . 9
       |
56 | | hashnncl 12585 |
. . . . . . . . 9
     
   |
57 | 55, 56 | syl 17 |
. . . . . . . 8
         
   |
58 | 54, 57 | mpbird 240 |
. . . . . . 7
           |
59 | 58 | nnrpd 11362 |
. . . . . 6
           |
60 | 46, 59 | rpdivcld 11381 |
. . . . 5
             |
61 | | ralnex 2834 |
. . . . . . . 8
 
                            
  |
62 | 55 | adantr 472 |
. . . . . . . . . . . 12
                       
  |
63 | 54 | adantr 472 |
. . . . . . . . . . . 12
                          |
64 | | simprl 772 |
. . . . . . . . . . . . . . 15
                       
  |
65 | 64 | adantr 472 |
. . . . . . . . . . . . . 14
     
 
                
   |
66 | | eqid 2471 |
. . . . . . . . . . . . . . 15
                             |
67 | 66 | metdsvalOLD 21957 |
. . . . . . . . . . . . . 14
                                 |
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . 13
     
 
                
                                 |
69 | 11 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
           |
70 | 69 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
     
 
                
       |
71 | | difssd 3550 |
. . . . . . . . . . . . . . 15
     
 
                
  
  |
72 | | elssuni 4219 |
. . . . . . . . . . . . . . . . . 18
    |
73 | 72 | adantl 473 |
. . . . . . . . . . . . . . . . 17
     
 
                

   |
74 | 47 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
     
 
                
    |
75 | 73, 74 | sseqtr4d 3455 |
. . . . . . . . . . . . . . . 16
     
 
                

  |
76 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
77 | 76 | notbid 301 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
78 | 16, 77 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . . . 19
 
   |
79 | 78 | necon2ad 2658 |
. . . . . . . . . . . . . . . . . 18
     |
80 | 79 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . 17
                            |
81 | 80 | imp 436 |
. . . . . . . . . . . . . . . 16
     
 
                
   |
82 | | pssdifn0 3743 |
. . . . . . . . . . . . . . . 16
 
     |
83 | 75, 81, 82 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     
 
                
     |
84 | 66 | metdsreOLD 21963 |
. . . . . . . . . . . . . . 15
                               |
85 | 70, 71, 83, 84 | syl3anc 1292 |
. . . . . . . . . . . . . 14
     
 
                
                     |
86 | 85, 65 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
     
 
                
                     |
87 | 68, 86 | eqeltrrd 2550 |
. . . . . . . . . . . 12
     
 
                
               |
88 | 60 | ad2antrr 740 |
. . . . . . . . . . . . 13
     
 
                
         |
89 | 88 | rpred 11364 |
. . . . . . . . . . . 12
     
 
                
         |
90 | | simprr 774 |
. . . . . . . . . . . . . . . 16
                        
                |
91 | | sseq2 3440 |
. . . . . . . . . . . . . . . . . 18
                                 |
92 | 91 | notbid 301 |
. . . . . . . . . . . . . . . . 17
                             
   |
93 | 92 | rspccva 3135 |
. . . . . . . . . . . . . . . 16
                 
                |
94 | 90, 93 | sylan 479 |
. . . . . . . . . . . . . . 15
     
 
                
              
  |
95 | 70, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
     
 
                
        |
96 | 88 | rpxrd 11365 |
. . . . . . . . . . . . . . . . 17
     
 
                
         |
97 | 66 | metdsgeOLD 21959 |
. . . . . . . . . . . . . . . . 17
       
 

                                                     |
98 | 95, 71, 65, 96, 97 | syl31anc 1295 |
. . . . . . . . . . . . . . . 16
     
 
                
       
                                       |
99 | | blssm 21511 |
. . . . . . . . . . . . . . . . . 18
                              |
100 | 95, 65, 96, 99 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
     
 
                
                 |
101 | | difin0ss 3745 |
. . . . . . . . . . . . . . . . 17
   
                             
                 |
102 | 100, 101 | syl5com 30 |
. . . . . . . . . . . . . . . 16
     
 
                
                   
                 |
103 | 98, 102 | sylbid 223 |
. . . . . . . . . . . . . . 15
     
 
                
       
                               
   |
104 | 94, 103 | mtod 182 |
. . . . . . . . . . . . . 14
     
 
                
      
                    |
105 | 86, 89 | ltnled 9799 |
. . . . . . . . . . . . . 14
     
 
                
                         
                           |
106 | 104, 105 | mpbird 240 |
. . . . . . . . . . . . 13
     
 
                
                  
        |
107 | 68, 106 | eqbrtrrd 4418 |
. . . . . . . . . . . 12
     
 
                
                     |
108 | 62, 63, 87, 89, 107 | fsumlt 13937 |
. . . . . . . . . . 11
                                    
         |
109 | | oveq1 6315 |
. . . . . . . . . . . . . . . . 17
           |
110 | 109 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . 16
                   |
111 | 110 | rneqd 5068 |
. . . . . . . . . . . . . . 15
                   |
112 | 111 | supeq1d 7978 |
. . . . . . . . . . . . . 14
            
              |
113 | 112 | sumeq2sdv 13847 |
. . . . . . . . . . . . 13
 
            
           
  |
114 | | sumex 13831 |
. . . . . . . . . . . . 13

             |
115 | 113, 17, 114 | fvmpt 5963 |
. . . . . . . . . . . 12
                    |
116 | 64, 115 | syl 17 |
. . . . . . . . . . 11
                            
              |
117 | 60 | adantr 472 |
. . . . . . . . . . . . . 14
                                |
118 | 117 | rpcnd 11366 |
. . . . . . . . . . . . 13
                                |
119 | | fsumconst 13928 |
. . . . . . . . . . . . 13
                              |
120 | 62, 118, 119 | syl2anc 673 |
. . . . . . . . . . . 12
                                             |
121 | | simplr 770 |
. . . . . . . . . . . . . 14
                          |
122 | 121 | rpcnd 11366 |
. . . . . . . . . . . . 13
                          |
123 | 58 | adantr 472 |
. . . . . . . . . . . . . 14
                              |
124 | 123 | nncnd 10647 |
. . . . . . . . . . . . 13
                              |
125 | 123 | nnne0d 10676 |
. . . . . . . . . . . . 13
                              |
126 | 122, 124,
125 | divcan2d 10407 |
. . . . . . . . . . . 12
                                      |
127 | 120, 126 | eqtr2d 2506 |
. . . . . . . . . . 11
                        
        |
128 | 108, 116,
127 | 3brtr4d 4426 |
. . . . . . . . . 10
                           
  |
129 | 19 | ad2antrr 740 |
. . . . . . . . . . . . 13
                              |
130 | 129, 64 | ffvelrnd 6038 |
. . . . . . . . . . . 12
                              |
131 | 130 | rpred 11364 |
. . . . . . . . . . 11
                              |
132 | 121 | rpred 11364 |
. . . . . . . . . . 11
                          |
133 | 131, 132 | ltnled 9799 |
. . . . . . . . . 10
                            
       |
134 | 128, 133 | mpbid 215 |
. . . . . . . . 9
                       
      |
135 | 134 | expr 626 |
. . . . . . . 8
        
             
       |
136 | 61, 135 | syl5bir 226 |
. . . . . . 7
                      
       |
137 | 136 | con4d 108 |
. . . . . 6
       
    
             
   |
138 | 137 | ralimdva 2805 |
. . . . 5
      
    

             
   |
139 | | oveq2 6316 |
. . . . . . . . 9
      
                        |
140 | 139 | sseq1d 3445 |
. . . . . . . 8
      
                          |
141 | 140 | rexbidv 2892 |
. . . . . . 7
      
 
                          |
142 | 141 | ralbidv 2829 |
. . . . . 6
      
 

         
                 |
143 | 142 | rspcev 3136 |
. . . . 5
       


             
   
          |
144 | 60, 138, 143 | syl6an 554 |
. . . 4
      
                  |
145 | 144 | rexlimdva 2871 |
. . 3
 

 

      
           |
146 | 45, 145 | mpd 15 |
. 2
 

             |
147 | 9, 146 | pm2.61dane 2730 |
1
   
          |