Step | Hyp | Ref
| Expression |
1 | | rankon 8297 |
. . 3
     |
2 | | onzsl 6705 |
. . 3
                            |
3 | 1, 2 | mpbi 213 |
. 2
                      |
4 | | sdom0 7735 |
. . . 4
 |
5 | | fveq2 5892 |
. . . . . 6
    
              |
6 | | cf0 8712 |
. . . . . 6
   
 |
7 | 5, 6 | syl6eq 2512 |
. . . . 5
    
          |
8 | 7 | breq2d 4430 |
. . . 4
    
            |
9 | 4, 8 | mtbiri 309 |
. . 3
    
          |
10 | | fveq2 5892 |
. . . . . . 7
                   |
11 | | cfsuc 8718 |
. . . . . . 7
       |
12 | 10, 11 | sylan9eqr 2518 |
. . . . . 6
                 |
13 | | nsuceq0 5526 |
. . . . . . . . 9
 |
14 | | neeq1 2698 |
. . . . . . . . 9
             |
15 | 13, 14 | mpbiri 241 |
. . . . . . . 8
           |
16 | | fveq2 5892 |
. . . . . . . . . . 11

          |
17 | | 0elon 5499 |
. . . . . . . . . . . . 13
 |
18 | | r1fnon 8269 |
. . . . . . . . . . . . . 14
 |
19 | | fndm 5701 |
. . . . . . . . . . . . . 14
   |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
21 | 17, 20 | eleqtrri 2539 |
. . . . . . . . . . . 12
 |
22 | | rankonid 8331 |
. . . . . . . . . . . 12

   
  |
23 | 21, 22 | mpbi 213 |
. . . . . . . . . . 11
     |
24 | 16, 23 | syl6eq 2512 |
. . . . . . . . . 10

      |
25 | 24 | necon3i 2668 |
. . . . . . . . 9
    
  |
26 | | rankvaln 8301 |
. . . . . . . . . . 11
            |
27 | 26 | necon1ai 2663 |
. . . . . . . . . 10
    
       |
28 | | breq2 4422 |
. . . . . . . . . . 11
 
   |
29 | | neeq1 2698 |
. . . . . . . . . . 11
 
   |
30 | | 0sdom1dom 7801 |
. . . . . . . . . . . 12

  |
31 | | vex 3060 |
. . . . . . . . . . . . 13
 |
32 | 31 | 0sdom 7734 |
. . . . . . . . . . . 12
   |
33 | 30, 32 | bitr3i 259 |
. . . . . . . . . . 11
   |
34 | 28, 29, 33 | vtoclbg 3120 |
. . . . . . . . . 10
      
   |
35 | 27, 34 | syl 17 |
. . . . . . . . 9
    
    |
36 | 25, 35 | mpbird 240 |
. . . . . . . 8
    
  |
37 | 15, 36 | syl 17 |
. . . . . . 7
       |
38 | 37 | adantl 472 |
. . . . . 6
         |
39 | 12, 38 | eqbrtrd 4439 |
. . . . 5
                 |
40 | 39 | rexlimiva 2887 |
. . . 4
                |
41 | | domnsym 7729 |
. . . 4
        
          |
42 | 40, 41 | syl 17 |
. . 3
                |
43 | | nlim0 5504 |
. . . . . . . . . . . . . . . . 17
 |
44 | | limeq 5458 |
. . . . . . . . . . . . . . . . 17
    
        |
45 | 43, 44 | mtbiri 309 |
. . . . . . . . . . . . . . . 16
    
      |
46 | 26, 45 | syl 17 |
. . . . . . . . . . . . . . 15
            |
47 | 46 | con4i 135 |
. . . . . . . . . . . . . 14
    
       |
48 | | r1elssi 8307 |
. . . . . . . . . . . . . 14
             |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . 13
    
       |
50 | 49 | sselda 3444 |
. . . . . . . . . . . 12
     
        |
51 | | ranksnb 8329 |
. . . . . . . . . . . 12
                  |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
     
             |
53 | | rankelb 8326 |
. . . . . . . . . . . . . 14
                  |
54 | 47, 53 | syl 17 |
. . . . . . . . . . . . 13
    

           |
55 | | limsuc 6708 |
. . . . . . . . . . . . 13
    
                    |
56 | 54, 55 | sylibd 222 |
. . . . . . . . . . . 12
    

           |
57 | 56 | imp 435 |
. . . . . . . . . . 11
     
           |
58 | 52, 57 | eqeltrd 2540 |
. . . . . . . . . 10
     
             |
59 | | eleq1a 2535 |
. . . . . . . . . 10
                         |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
     
               |
61 | 60 | rexlimdva 2891 |
. . . . . . . 8
    
 
     
       |
62 | 61 | abssdv 3515 |
. . . . . . 7
    
 
      
      |
63 | | snex 4658 |
. . . . . . . . . . . . 13
 
 |
64 | 63 | dfiun2 4326 |
. . . . . . . . . . . 12

 
       |
65 | | iunid 4347 |
. . . . . . . . . . . 12

 
 |
66 | 64, 65 | eqtr3i 2486 |
. . . . . . . . . . 11
  
    |
67 | 66 | fveq2i 5895 |
. . . . . . . . . 10
     
         |
68 | 48 | sselda 3444 |
. . . . . . . . . . . . . . 15
      
        |
69 | | snwf 8311 |
. . . . . . . . . . . . . . 15
               |
70 | | eleq1a 2535 |
. . . . . . . . . . . . . . 15
                   |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . 14
      
            |
72 | 71 | rexlimdva 2891 |
. . . . . . . . . . . . 13
                  |
73 | 72 | abssdv 3515 |
. . . . . . . . . . . 12
       
          |
74 | | abrexexg 6800 |
. . . . . . . . . . . . 13
       
     |
75 | | eleq1 2528 |
. . . . . . . . . . . . . 14
  
  
     
 
  
        |
76 | | sseq1 3465 |
. . . . . . . . . . . . . 14
  
  
     
 
           |
77 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
78 | 77 | r1elss 8308 |
. . . . . . . . . . . . . 14
     
       |
79 | 75, 76, 78 | vtoclbg 3120 |
. . . . . . . . . . . . 13
  
  
  
       
 
           |
80 | 74, 79 | syl 17 |
. . . . . . . . . . . 12
        
  
    
 
  
        |
81 | 73, 80 | mpbird 240 |
. . . . . . . . . . 11
       
          |
82 | | rankuni2b 8355 |
. . . . . . . . . . 11
  
       
     
    
 
  
      |
83 | 81, 82 | syl 17 |
. . . . . . . . . 10
                  
         |
84 | 67, 83 | syl5eqr 2510 |
. . . . . . . . 9
            
         |
85 | | fvex 5902 |
. . . . . . . . . . 11
     |
86 | 85 | dfiun2 4326 |
. . . . . . . . . 10
  
           
          |
87 | | fveq2 5892 |
. . . . . . . . . . . 12
               |
88 | 63, 87 | abrexco 6179 |
. . . . . . . . . . 11
   
         

        |
89 | 88 | unieqi 4221 |
. . . . . . . . . 10
    
           
        |
90 | 86, 89 | eqtri 2484 |
. . . . . . . . 9
  
         
        |
91 | 84, 90 | syl6req 2513 |
. . . . . . . 8
        
             |
92 | 47, 91 | syl 17 |
. . . . . . 7
    
  
             |
93 | | fvex 5902 |
. . . . . . . 8
     |
94 | 93 | cfslb 8727 |
. . . . . . 7
     
 
      
     

                     
         |
95 | 62, 92, 94 | mpd3an23 1375 |
. . . . . 6
    
         
         |
96 | | fveq2 5892 |
. . . . . . . . . . 11
           |
97 | 96 | fveq2d 5896 |
. . . . . . . . . 10
                   |
98 | | breq12 4423 |
. . . . . . . . . 10
                  
                    |
99 | 97, 98 | mpdan 679 |
. . . . . . . . 9
                     |
100 | | rexeq 3000 |
. . . . . . . . . . 11
  
      
         |
101 | 100 | abbidv 2580 |
. . . . . . . . . 10
           
         |
102 | | breq12 4423 |
. . . . . . . . . 10
   
        
         

        
          |
103 | 101, 102 | mpancom 680 |
. . . . . . . . 9
  

        
          |
104 | 99, 103 | imbi12d 326 |
. . . . . . . 8
                    
          
           |
105 | | eqid 2462 |
. . . . . . . . . 10
                 |
106 | 105 | rnmpt 5102 |
. . . . . . . . 9
         
        |
107 | | cfon 8716 |
. . . . . . . . . . 11
         |
108 | | sdomdom 7628 |
. . . . . . . . . . 11
                   |
109 | | ondomen 8499 |
. . . . . . . . . . 11
                     |
110 | 107, 108,
109 | sylancr 674 |
. . . . . . . . . 10
           |
111 | | fvex 5902 |
. . . . . . . . . . . 12
       |
112 | 111, 105 | fnmpti 5732 |
. . . . . . . . . . 11
         |
113 | | dffn4 5826 |
. . . . . . . . . . 11
                               |
114 | 112, 113 | mpbi 213 |
. . . . . . . . . 10
                     |
115 | | fodomnum 8519 |
. . . . . . . . . 10
                                 |
116 | 110, 114,
115 | mpisyl 21 |
. . . . . . . . 9
        

         |
117 | 106, 116 | syl5eqbrr 4453 |
. . . . . . . 8
                    |
118 | 104, 117 | vtoclg 3119 |
. . . . . . 7
                
          |
119 | 47, 118 | syl 17 |
. . . . . 6
    
          
          |
120 | | domtr 7653 |
. . . . . . 7
           
        
                  |
121 | 120, 41 | syl 17 |
. . . . . 6
           
        
       
          |
122 | 95, 119, 121 | syl6an 552 |
. . . . 5
    
        
           |
123 | 122 | pm2.01d 174 |
. . . 4
    
          |
124 | 123 | adantl 472 |
. . 3
                     |
125 | 9, 42, 124 | 3jaoi 1340 |
. 2
      
              
          |
126 | 3, 125 | ax-mp 5 |
1
         |