Step | Hyp | Ref
| Expression |
1 | | climinf.5 |
. . . . . . . . . . . 12
       |
2 | | frn 5676 |
. . . . . . . . . . . 12
    
  |
3 | 1, 2 | syl 16 |
. . . . . . . . . . 11
   |
4 | | ffn 5670 |
. . . . . . . . . . . . . 14
       |
5 | 1, 4 | syl 16 |
. . . . . . . . . . . . 13
   |
6 | | climinf.4 |
. . . . . . . . . . . . . . 15
   |
7 | | uzid 10989 |
. . . . . . . . . . . . . . 15
       |
8 | 6, 7 | syl 16 |
. . . . . . . . . . . . . 14
       |
9 | | climinf.3 |
. . . . . . . . . . . . . 14
     |
10 | 8, 9 | syl6eleqr 2553 |
. . . . . . . . . . . . 13
   |
11 | | fnfvelrn 5952 |
. . . . . . . . . . . . 13
 
       |
12 | 5, 10, 11 | syl2anc 661 |
. . . . . . . . . . . 12
       |
13 | | ne0i 3754 |
. . . . . . . . . . . 12
       |
14 | 12, 13 | syl 16 |
. . . . . . . . . . 11
   |
15 | | climinf.7 |
. . . . . . . . . . . 12
         |
16 | | breq2 4407 |
. . . . . . . . . . . . . . 15
     
       |
17 | 16 | ralrn 5958 |
. . . . . . . . . . . . . 14
  

       |
18 | 17 | rexbidv 2868 |
. . . . . . . . . . . . 13
  

         |
19 | 5, 18 | syl 16 |
. . . . . . . . . . . 12
   

        |
20 | 15, 19 | mpbird 232 |
. . . . . . . . . . 11
     |
21 | 3, 14, 20 | 3jca 1168 |
. . . . . . . . . 10
   
   |
22 | 21 | adantr 465 |
. . . . . . . . 9
 


 
   |
23 | | infmrcl 10423 |
. . . . . . . . 9
 

     
  |
24 | 22, 23 | syl 16 |
. . . . . . . 8
 

      |
25 | | simpr 461 |
. . . . . . . 8
 

  |
26 | 24, 25 | ltaddrpd 11170 |
. . . . . . 7
 

        
   |
27 | | rpre 11111 |
. . . . . . . . . 10

  |
28 | 27 | adantl 466 |
. . . . . . . . 9
 

  |
29 | 24, 28 | readdcld 9527 |
. . . . . . . 8
 

    
   |
30 | | infrglb 29939 |
. . . . . . . 8
    
     
      
           
    |
31 | 22, 29, 30 | syl2anc 661 |
. . . . . . 7
 

    
           
    |
32 | 26, 31 | mpbid 210 |
. . . . . 6
 

         |
33 | 3 | sselda 3467 |
. . . . . . . . . . 11
 
   |
34 | 33 | adantlr 714 |
. . . . . . . . . 10
       |
35 | 24 | adantr 465 |
. . . . . . . . . . 11
        
  |
36 | 27 | ad2antlr 726 |
. . . . . . . . . . 11
       |
37 | 35, 36 | readdcld 9527 |
. . . . . . . . . 10
             |
38 | 34, 37, 36 | ltsub1d 10062 |
. . . . . . . . 9
          

             |
39 | 3, 14, 20, 23 | syl3anc 1219 |
. . . . . . . . . . . . 13
       |
40 | 39 | recnd 9526 |
. . . . . . . . . . . 12
       |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . 11
        
  |
42 | 36 | recnd 9526 |
. . . . . . . . . . 11
       |
43 | 41, 42 | pncand 9834 |
. . . . . . . . . 10
                   |
44 | 43 | breq2d 4415 |
. . . . . . . . 9
                 
       |
45 | 38, 44 | bitrd 253 |
. . . . . . . 8
          

     
   |
46 | 45 | biimpd 207 |
. . . . . . 7
          
  
       |
47 | 46 | reximdva 2934 |
. . . . . 6
 

 
     
       
   |
48 | 32, 47 | mpd 15 |
. . . . 5
 

       
  |
49 | | oveq1 6210 |
. . . . . . . . 9
               |
50 | 49 | breq1d 4413 |
. . . . . . . 8
       
   
         
   |
51 | 50 | rexrn 5957 |
. . . . . . 7
  
  
   

         
   |
52 | 5, 51 | syl 16 |
. . . . . 6
         

     
       |
53 | 52 | biimpa 484 |
. . . . 5
 
       


         
  |
54 | 48, 53 | syldan 470 |
. . . 4
 


         
  |
55 | 1 | adantr 465 |
. . . . . . . . . . 11
 

      |
56 | 9 | uztrn2 10992 |
. . . . . . . . . . 11
 
       |
57 | | ffvelrn 5953 |
. . . . . . . . . . 11
     
       |
58 | 55, 56, 57 | syl2an 477 |
. . . . . . . . . 10
    
            |
59 | | simpl 457 |
. . . . . . . . . . 11
 
       |
60 | | ffvelrn 5953 |
. . . . . . . . . . 11
     
       |
61 | 55, 59, 60 | syl2an 477 |
. . . . . . . . . 10
    
            |
62 | 39 | ad2antrr 725 |
. . . . . . . . . 10
    
            |
63 | | simprr 756 |
. . . . . . . . . . 11
    
            |
64 | | fzssuz 11619 |
. . . . . . . . . . . . . 14
         |
65 | | uzss 10995 |
. . . . . . . . . . . . . . . . 17
    
          |
66 | 65, 9 | syl6sseqr 3514 |
. . . . . . . . . . . . . . . 16
    
      |
67 | 66, 9 | eleq2s 2562 |
. . . . . . . . . . . . . . 15
       |
68 | 67 | ad2antrl 727 |
. . . . . . . . . . . . . 14
    
         
  |
69 | 64, 68 | syl5ss 3478 |
. . . . . . . . . . . . 13
    
            |
70 | | ffvelrn 5953 |
. . . . . . . . . . . . . . . 16
     
       |
71 | 70 | ralrimiva 2830 |
. . . . . . . . . . . . . . 15
            |
72 | 1, 71 | syl 16 |
. . . . . . . . . . . . . 14
        |
73 | 72 | ad2antrr 725 |
. . . . . . . . . . . . 13
    
             |
74 | | ssralv 3527 |
. . . . . . . . . . . . 13
      
                 |
75 | 69, 73, 74 | sylc 60 |
. . . . . . . . . . . 12
    
                  |
76 | 75 | r19.21bi 2920 |
. . . . . . . . . . 11
   
 
                 |
77 | | fzssuz 11619 |
. . . . . . . . . . . . . 14
           |
78 | 77, 68 | syl5ss 3478 |
. . . . . . . . . . . . 13
    
              |
79 | 78 | sselda 3467 |
. . . . . . . . . . . 12
   
 
               |
80 | | climinf.6 |
. . . . . . . . . . . . . . 15
 
             |
81 | 80 | ralrimiva 2830 |
. . . . . . . . . . . . . 14
              |
82 | 81 | ad2antrr 725 |
. . . . . . . . . . . . 13
    
                   |
83 | | oveq1 6210 |
. . . . . . . . . . . . . . . 16
       |
84 | 83 | fveq2d 5806 |
. . . . . . . . . . . . . . 15
          
    |
85 | | fveq2 5802 |
. . . . . . . . . . . . . . 15
           |
86 | 84, 85 | breq12d 4416 |
. . . . . . . . . . . . . 14
       
   
             |
87 | 86 | rspccva 3178 |
. . . . . . . . . . . . 13
                          |
88 | 82, 87 | sylan 471 |
. . . . . . . . . . . 12
   
 
                   |
89 | 79, 88 | syldan 470 |
. . . . . . . . . . 11
   
 
                         |
90 | 63, 76, 89 | monoord2 11957 |
. . . . . . . . . 10
    
                |
91 | 58, 61, 62, 90 | lesub1dd 10069 |
. . . . . . . . 9
    
              

            |
92 | 58, 62 | resubcld 9890 |
. . . . . . . . . 10
    
              
   |
93 | 61, 62 | resubcld 9890 |
. . . . . . . . . 10
    
              
   |
94 | 27 | ad2antlr 726 |
. . . . . . . . . 10
    
        |
95 | | lelttr 9579 |
. . . . . . . . . 10
          
                      

                                  |
96 | 92, 93, 94, 95 | syl3anc 1219 |
. . . . . . . . 9
    
                          
         
          
    |
97 | 91, 96 | mpand 675 |
. . . . . . . 8
    
                
             |
98 | | ltsub23 9933 |
. . . . . . . . 9
     
   
       
   
             |
99 | 61, 94, 62, 98 | syl3anc 1219 |
. . . . . . . 8
    
                
        
    |
100 | 3 | ad2antrr 725 |
. . . . . . . . . . 11
    
     
  |
101 | 5 | adantr 465 |
. . . . . . . . . . . 12
 

  |
102 | | fnfvelrn 5952 |
. . . . . . . . . . . 12
 
       |
103 | 101, 56, 102 | syl2an 477 |
. . . . . . . . . . 11
    
            |
104 | 100, 103 | sseldd 3468 |
. . . . . . . . . 10
    
            |
105 | 20 | ad2antrr 725 |
. . . . . . . . . . 11
    
          |
106 | | infmrlb 10425 |
. . . . . . . . . . 11
            
      |
107 | 100, 105,
103, 106 | syl3anc 1219 |
. . . . . . . . . 10
    
                |
108 | 62, 104, 107 | abssubge0d 13039 |
. . . . . . . . 9
    
                            
   |
109 | 108 | breq1d 4413 |
. . . . . . . 8
    
                  
 
             |
110 | 97, 99, 109 | 3imtr4d 268 |
. . . . . . 7
    
                
                 |
111 | 110 | anassrs 648 |
. . . . . 6
   


               
                 |
112 | 111 | ralrimdva 2912 |
. . . . 5
           
                           |
113 | 112 | reximdva 2934 |
. . . 4
 

 
           
                      |
114 | 54, 113 | mpd 15 |
. . 3
 


                      |
115 | 114 | ralrimiva 2830 |
. 2
   
                
    |
116 | | fvex 5812 |
. . . . 5
     |
117 | 9, 116 | eqeltri 2538 |
. . . 4
 |
118 | | fex 6062 |
. . . 4
     
   |
119 | 1, 117, 118 | sylancl 662 |
. . 3
   |
120 | | eqidd 2455 |
. . 3
 
           |
121 | 1 | ffvelrnda 5955 |
. . . 4
 
       |
122 | 121 | recnd 9526 |
. . 3
 
       |
123 | 9, 6, 119, 120, 40, 122 | clim2c 13104 |
. 2
     
                         |
124 | 115, 123 | mpbird 232 |
1
       |