Step | Hyp | Ref
| Expression |
1 | | limelon 5493 |
. . . . . 6
     |
2 | | 0ellim 5492 |
. . . . . . 7

  |
3 | 2 | adantl 473 |
. . . . . 6
     |
4 | | oe0m1 7241 |
. . . . . . 7
 
     |
5 | 4 | biimpa 492 |
. . . . . 6
       |
6 | 1, 3, 5 | syl2anc 673 |
. . . . 5
       |
7 | | eldif 3400 |
. . . . . . . . 9
  
    |
8 | | limord 5489 |
. . . . . . . . . . . 12

  |
9 | | ordelon 5454 |
. . . . . . . . . . . 12
     |
10 | 8, 9 | sylan 479 |
. . . . . . . . . . 11
     |
11 | | on0eln0 5485 |
. . . . . . . . . . . . 13
 
   |
12 | | el1o 7219 |
. . . . . . . . . . . . . 14

  |
13 | 12 | necon3bbii 2690 |
. . . . . . . . . . . . 13

  |
14 | 11, 13 | syl6bbr 271 |
. . . . . . . . . . . 12
 
   |
15 | | oe0m1 7241 |
. . . . . . . . . . . . 13
 
     |
16 | 15 | biimpd 212 |
. . . . . . . . . . . 12
       |
17 | 14, 16 | sylbird 243 |
. . . . . . . . . . 11
 

    |
18 | 10, 17 | syl 17 |
. . . . . . . . . 10
   

    |
19 | 18 | impr 631 |
. . . . . . . . 9
  
      |
20 | 7, 19 | sylan2b 483 |
. . . . . . . 8
         |
21 | 20 | iuneq2dv 4291 |
. . . . . . 7

            |
22 | | df-1o 7200 |
. . . . . . . . . . 11
 |
23 | | limsuc 6695 |
. . . . . . . . . . . 12

    |
24 | 2, 23 | mpbid 215 |
. . . . . . . . . . 11

  |
25 | 22, 24 | syl5eqel 2553 |
. . . . . . . . . 10

  |
26 | | 1on 7207 |
. . . . . . . . . . 11
 |
27 | 26 | onirri 5536 |
. . . . . . . . . 10
 |
28 | 25, 27 | jctir 547 |
. . . . . . . . 9


   |
29 | | eldif 3400 |
. . . . . . . . 9
  
    |
30 | 28, 29 | sylibr 217 |
. . . . . . . 8


   |
31 | | ne0i 3728 |
. . . . . . . 8
  
    |
32 | | iunconst 4278 |
. . . . . . . 8
  
      |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . 7

      |
34 | 21, 33 | eqtrd 2505 |
. . . . . 6

        |
35 | 34 | adantl 473 |
. . . . 5
           |
36 | 6, 35 | eqtr4d 2508 |
. . . 4
         
   |
37 | | oveq1 6315 |
. . . . 5

  
   |
38 | | oveq1 6315 |
. . . . . 6

  
   |
39 | 38 | iuneq2d 4296 |
. . . . 5

      
       |
40 | 37, 39 | eqeq12d 2486 |
. . . 4

        
           |
41 | 36, 40 | syl5ibr 229 |
. . 3

              |
42 | 41 | impcom 437 |
. 2
   
           |
43 | | oelim 7254 |
. . 3
         
    |
44 | | limsuc 6695 |
. . . . . . . . . . . . 13


   |
45 | 44 | biimpa 492 |
. . . . . . . . . . . 12
  
  |
46 | | nsuceq0 5510 |
. . . . . . . . . . . . 13
 |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
     |
48 | | dif1o 7220 |
. . . . . . . . . . . 12
  

   |
49 | 45, 47, 48 | sylanbrc 677 |
. . . . . . . . . . 11
  
    |
50 | 49 | ex 441 |
. . . . . . . . . 10


     |
51 | 50 | ad2antlr 741 |
. . . . . . . . 9
           |
52 | | sssucid 5507 |
. . . . . . . . . . 11
 |
53 | | ordelon 5454 |
. . . . . . . . . . . . . . . . 17
     |
54 | 8, 53 | sylan 479 |
. . . . . . . . . . . . . . . 16
     |
55 | | suceloni 6659 |
. . . . . . . . . . . . . . . 16

  |
56 | 54, 55 | jccir 548 |
. . . . . . . . . . . . . . 15
   
   |
57 | | id 22 |
. . . . . . . . . . . . . . . . 17
 
     |
58 | 57 | 3expa 1231 |
. . . . . . . . . . . . . . . 16
         |
59 | 58 | ancoms 460 |
. . . . . . . . . . . . . . 15
     
   |
60 | 56, 59 | sylan2 482 |
. . . . . . . . . . . . . 14
         |
61 | 60 | anassrs 660 |
. . . . . . . . . . . . 13
   
     |
62 | | oewordi 7310 |
. . . . . . . . . . . . 13
     
  
    |
63 | 61, 62 | sylan 479 |
. . . . . . . . . . . 12
    
 
   
    |
64 | 63 | an32s 821 |
. . . . . . . . . . 11
    

 
 
     |
65 | 52, 64 | mpi 20 |
. . . . . . . . . 10
    

   
   |
66 | 65 | ex 441 |
. . . . . . . . 9
       
     |
67 | 51, 66 | jcad 542 |
. . . . . . . 8
                 |
68 | | oveq2 6316 |
. . . . . . . . . 10
       |
69 | 68 | sseq2d 3446 |
. . . . . . . . 9
     
       |
70 | 69 | rspcev 3136 |
. . . . . . . 8
        
          |
71 | 67, 70 | syl6 33 |
. . . . . . 7
           
     |
72 | 71 | ralrimiv 2808 |
. . . . . 6
     

         |
73 | | iunss2 4314 |
. . . . . 6
 

     

           |
74 | 72, 73 | syl 17 |
. . . . 5
     


        |
75 | | difss 3549 |
. . . . . . . 8
   |
76 | | iunss1 4281 |
. . . . . . . 8
         
    |
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
      
   |
78 | | oveq2 6316 |
. . . . . . . 8
       |
79 | 78 | cbviunv 4308 |
. . . . . . 7

  
   |
80 | 77, 79 | sseqtri 3450 |
. . . . . 6
      
   |
81 | 80 | a1i 11 |
. . . . 5
     
      
   |
82 | 74, 81 | eqssd 3435 |
. . . 4
     

         |
83 | 82 | adantlrl 734 |
. . 3
        
         |
84 | 43, 83 | eqtrd 2505 |
. 2
         
       |
85 | 42, 84 | oe0lem 7233 |
1
  
    
       |