Step | Hyp | Ref
| Expression |
1 | | xrltso 11437 |
. . . 4
 |
2 | 1 | supex 7974 |
. . 3
           
  |
3 | 2 | a1i 11 |
. 2
                        
   |
4 | | limsupval.1 |
. . 3
            
   |
5 | 4 | a1i 11 |
. 2
                            |
6 | 4 | limsupgval 13527 |
. . . 4
                    |
7 | 6 | adantl 468 |
. . 3
                                |
8 | | simpl3 1012 |
. . . . . . 7
                   |
9 | | limsupgre.z |
. . . . . . . . . . 11
     |
10 | | uzssz 11175 |
. . . . . . . . . . 11
     |
11 | 9, 10 | eqsstri 3461 |
. . . . . . . . . 10
 |
12 | | zssre 10941 |
. . . . . . . . . 10
 |
13 | 11, 12 | sstri 3440 |
. . . . . . . . 9
 |
14 | 13 | a1i 11 |
. . . . . . . 8
               |
15 | | simpl2 1011 |
. . . . . . . . 9
                   |
16 | | ressxr 9681 |
. . . . . . . . 9
 |
17 | | fss 5735 |
. . . . . . . . 9
             |
18 | 15, 16, 17 | sylancl 667 |
. . . . . . . 8
                   |
19 | | pnfxr 11409 |
. . . . . . . . 9
 |
20 | 19 | a1i 11 |
. . . . . . . 8
               |
21 | 4 | limsuplt 13531 |
. . . . . . . 8
 
    
             |
22 | 14, 18, 20, 21 | syl3anc 1267 |
. . . . . . 7
                          |
23 | 8, 22 | mpbid 214 |
. . . . . 6
                    |
24 | | fzfi 12182 |
. . . . . . . 8
         |
25 | 15 | adantr 467 |
. . . . . . . . . 10
                           |
26 | | elfzuz 11793 |
. . . . . . . . . . 11
        
      |
27 | 26, 9 | syl6eleqr 2539 |
. . . . . . . . . 10
        
  |
28 | | ffvelrn 6018 |
. . . . . . . . . 10
     
       |
29 | 25, 27, 28 | syl2an 480 |
. . . . . . . . 9
             
       
               |
30 | 29 | ralrimiva 2801 |
. . . . . . . 8
                                     |
31 | | fimaxre3 10550 |
. . . . . . . 8
          
                            
  |
32 | 24, 30, 31 | sylancr 668 |
. . . . . . 7
                                   
  |
33 | | simpr 463 |
. . . . . . . . . 10
               |
34 | 33 | ad2antrr 731 |
. . . . . . . . 9
             
                      
 
  |
35 | 4 | limsupgf 13526 |
. . . . . . . . . 10
     |
36 | 35 | ffvelrni 6019 |
. . . . . . . . 9
       |
37 | 34, 36 | syl 17 |
. . . . . . . 8
             
                      
 
      |
38 | | simprl 763 |
. . . . . . . . . 10
             
                      
 
  |
39 | 16, 38 | sseldi 3429 |
. . . . . . . . 9
             
                      
 
  |
40 | | simprl 763 |
. . . . . . . . . . 11
                       |
41 | 40 | adantr 467 |
. . . . . . . . . 10
             
                      
 
  |
42 | 35 | ffvelrni 6019 |
. . . . . . . . . 10
       |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
             
                      
 
      |
44 | 39, 43 | ifcld 3923 |
. . . . . . . 8
             
                      
 
     
         |
45 | 19 | a1i 11 |
. . . . . . . 8
             
                      
 
  |
46 | 40 | ad2antrr 731 |
. . . . . . . . . . . 12
                                     
 
   |
47 | 13 | a1i 11 |
. . . . . . . . . . . . 13
             
                      
 
  |
48 | 47 | sselda 3431 |
. . . . . . . . . . . 12
                                     
 
   |
49 | | xrleid 11446 |
. . . . . . . . . . . . . . . . 17
    
          |
50 | 43, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
             
                      
 
          |
51 | 18 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
             
                      
 
      |
52 | 4 | limsupgle 13528 |
. . . . . . . . . . . . . . . . 17
       
               
            |
53 | 47, 51, 41, 43, 52 | syl211anc 1273 |
. . . . . . . . . . . . . . . 16
             
                      
 
          
   
        |
54 | 50, 53 | mpbid 214 |
. . . . . . . . . . . . . . 15
             
                      
 


           |
55 | 54 | r19.21bi 2756 |
. . . . . . . . . . . . . 14
                                     
 
 
           |
56 | 55 | imp 431 |
. . . . . . . . . . . . 13
                                      
 
            |
57 | 46, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
                                     
 
       |
58 | 39 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                     
 
   |
59 | | xrmax1 11467 |
. . . . . . . . . . . . . . . 16
                          |
60 | 57, 58, 59 | syl2anc 666 |
. . . . . . . . . . . . . . 15
                                     
 
                    |
61 | 51 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . 16
                                     
 
       |
62 | 44 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                     
 
                |
63 | | xrletr 11452 |
. . . . . . . . . . . . . . . 16
               
                     
     
       
                    |
64 | 61, 57, 62, 63 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
                                     
 
              
     
       
                    |
65 | 60, 64 | mpan2d 679 |
. . . . . . . . . . . . . 14
                                     
 
     
                        |
66 | 65 | adantr 467 |
. . . . . . . . . . . . 13
                                      
 
      
                        |
67 | 56, 66 | mpd 15 |
. . . . . . . . . . . 12
                                      
 
                     |
68 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
                                     
 
   |
69 | 68, 9 | syl6eleq 2538 |
. . . . . . . . . . . . . . . . 17
                                     
 
       |
70 | 41 | flcld 12031 |
. . . . . . . . . . . . . . . . . 18
             
                      
 
      |
71 | 70 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                                     
 
       |
72 | | elfz5 11789 |
. . . . . . . . . . . . . . . . 17
                   
       |
73 | 69, 71, 72 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
                                     
 
         
       |
74 | 11, 68 | sseldi 3429 |
. . . . . . . . . . . . . . . . 17
                                     
 
   |
75 | | flge 12038 |
. . . . . . . . . . . . . . . . 17
 
         |
76 | 46, 74, 75 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
                                     
 
 
       |
77 | 73, 76 | bitr4d 260 |
. . . . . . . . . . . . . . 15
                                     
 
         
   |
78 | 77 | biimpar 488 |
. . . . . . . . . . . . . 14
                                      
 
            |
79 | | simprr 765 |
. . . . . . . . . . . . . . 15
             
                      
 
             
  |
80 | 79 | ad2antrr 731 |
. . . . . . . . . . . . . 14
                                      
 
               
  |
81 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
82 | 81 | breq1d 4411 |
. . . . . . . . . . . . . . 15
     
       |
83 | 82 | rspcv 3145 |
. . . . . . . . . . . . . 14
        
 
            
       |
84 | 78, 80, 83 | sylc 62 |
. . . . . . . . . . . . 13
                                      
 
        |
85 | | xrmax2 11468 |
. . . . . . . . . . . . . . . . 17
                      |
86 | 43, 39, 85 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
             
                      
 
               |
87 | 86 | adantr 467 |
. . . . . . . . . . . . . . 15
                                     
 
                |
88 | | xrletr 11452 |
. . . . . . . . . . . . . . . 16
           
             
     
       
                    |
89 | 61, 58, 62, 88 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
                                     
 
      
     
       
                    |
90 | 87, 89 | mpan2d 679 |
. . . . . . . . . . . . . 14
                                     
 
     
                    |
91 | 90 | adantr 467 |
. . . . . . . . . . . . 13
                                      
 
      
                    |
92 | 84, 91 | mpd 15 |
. . . . . . . . . . . 12
                                      
 
                     |
93 | 46, 48, 67, 92 | lecasei 9737 |
. . . . . . . . . . 11
                                     
 
                    |
94 | 93 | a1d 26 |
. . . . . . . . . 10
                                     
 
 
                    |
95 | 94 | ralrimiva 2801 |
. . . . . . . . 9
             
                      
 


                    |
96 | 4 | limsupgle 13528 |
. . . . . . . . . 10
       
                                     
     
           |
97 | 47, 51, 34, 44, 96 | syl211anc 1273 |
. . . . . . . . 9
             
                      
 
                 


                     |
98 | 95, 97 | mpbird 236 |
. . . . . . . 8
             
                      
 
                   |
99 | 38 | ltpnfd 11420 |
. . . . . . . . 9
             
                      
 
  |
100 | | simplrr 770 |
. . . . . . . . 9
             
                      
 
      |
101 | | breq1 4404 |
. . . . . . . . . 10
                               |
102 | | breq1 4404 |
. . . . . . . . . 10
                                       |
103 | 101, 102 | ifboth 3916 |
. . . . . . . . 9
                      |
104 | 99, 100, 103 | syl2anc 666 |
. . . . . . . 8
             
                      
 
     
         |
105 | 37, 44, 45, 98, 104 | xrlelttrd 11454 |
. . . . . . 7
             
                      
 
      |
106 | 32, 105 | rexlimddv 2882 |
. . . . . 6
                           |
107 | 23, 106 | rexlimddv 2882 |
. . . . 5
                   |
108 | 7, 107 | eqbrtrrd 4424 |
. . . 4
                        
   |
109 | | imassrn 5178 |
. . . . . . . . 9
        |
110 | | frn 5733 |
. . . . . . . . . 10
    
  |
111 | 15, 110 | syl 17 |
. . . . . . . . 9
               |
112 | 109, 111 | syl5ss 3442 |
. . . . . . . 8
                      |
113 | 112, 16 | syl6ss 3443 |
. . . . . . 7
                      |
114 | | df-ss 3417 |
. . . . . . 7
                
         |
115 | 113, 114 | sylib 200 |
. . . . . 6
                  
 
     
    |
116 | 115, 112 | eqsstrd 3465 |
. . . . 5
                  
 
   |
117 | | simpl1 1010 |
. . . . . . . . . . 11
               |
118 | | flcl 12028 |
. . . . . . . . . . . . . 14
       |
119 | 118 | adantl 468 |
. . . . . . . . . . . . 13
                   |
120 | 119 | peano2zd 11040 |
. . . . . . . . . . . 12
                     |
121 | 120, 117 | ifcld 3923 |
. . . . . . . . . . 11
              
                 |
122 | 117 | zred 11037 |
. . . . . . . . . . . 12
               |
123 | 120 | zred 11037 |
. . . . . . . . . . . 12
                     |
124 | | max1 11477 |
. . . . . . . . . . . 12
          
                 |
125 | 122, 123,
124 | syl2anc 666 |
. . . . . . . . . . 11
                                |
126 | | eluz2 11162 |
. . . . . . . . . . 11
                     
  
                                   |
127 | 117, 121,
125, 126 | syl3anbrc 1191 |
. . . . . . . . . 10
              
                     |
128 | 127, 9 | syl6eleqr 2539 |
. . . . . . . . 9
              
                 |
129 | | fdm 5731 |
. . . . . . . . . 10
       |
130 | 15, 129 | syl 17 |
. . . . . . . . 9
               |
131 | 128, 130 | eleqtrrd 2531 |
. . . . . . . 8
              
                 |
132 | 121 | zred 11037 |
. . . . . . . . 9
              
                 |
133 | | fllep1 12034 |
. . . . . . . . . . 11
         |
134 | 133 | adantl 468 |
. . . . . . . . . 10
                     |
135 | | max2 11479 |
. . . . . . . . . . 11
                
                 |
136 | 122, 123,
135 | syl2anc 666 |
. . . . . . . . . 10
                                      |
137 | 33, 123, 132, 134, 136 | letrd 9789 |
. . . . . . . . 9
                                |
138 | | elicopnf 11727 |
. . . . . . . . . 10
                     
  
                                    |
139 | 138 | adantl 468 |
. . . . . . . . 9
                                 
  
                                    |
140 | 132, 137,
139 | mpbir2and 932 |
. . . . . . . 8
              
                    |
141 | | inelcm 3818 |
. . . . . . . 8
                                               |
142 | 131, 140,
141 | syl2anc 666 |
. . . . . . 7
                    |
143 | | imadisj 5186 |
. . . . . . . 8
       
       |
144 | 143 | necon3bii 2675 |
. . . . . . 7
               |
145 | 142, 144 | sylibr 216 |
. . . . . 6
                      |
146 | 115, 145 | eqnetrd 2690 |
. . . . 5
                  
 
   |
147 | | supxrre1 11613 |
. . . . 5
                
 
 
            

           
    |
148 | 116, 146,
147 | syl2anc 666 |
. . . 4
                         

           
    |
149 | 108, 148 | mpbird 236 |
. . 3
                        
   |
150 | 7, 149 | eqeltrd 2528 |
. 2
                   |
151 | 3, 5, 150 | fmpt2d 6051 |
1
                 |