Step | Hyp | Ref
| Expression |
1 | | xrltso 11440 |
. . . 4
 |
2 | 1 | supex 7977 |
. . 3
           
  |
3 | 2 | a1i 11 |
. 2
                        
   |
4 | | limsupval.1 |
. . 3
            
   |
5 | 4 | a1i 11 |
. 2
                            |
6 | 4 | limsupgval 13534 |
. . . 4
                    |
7 | 6 | adantl 468 |
. . 3
                                |
8 | | simpl3 1013 |
. . . . . . 7
                   |
9 | | limsupgre.z |
. . . . . . . . . . 11
     |
10 | | uzssz 11178 |
. . . . . . . . . . 11
     |
11 | 9, 10 | eqsstri 3462 |
. . . . . . . . . 10
 |
12 | | zssre 10944 |
. . . . . . . . . 10
 |
13 | 11, 12 | sstri 3441 |
. . . . . . . . 9
 |
14 | 13 | a1i 11 |
. . . . . . . 8
               |
15 | | simpl2 1012 |
. . . . . . . . 9
                   |
16 | | ressxr 9684 |
. . . . . . . . 9
 |
17 | | fss 5737 |
. . . . . . . . 9
             |
18 | 15, 16, 17 | sylancl 668 |
. . . . . . . 8
                   |
19 | | pnfxr 11412 |
. . . . . . . . 9
 |
20 | 19 | a1i 11 |
. . . . . . . 8
               |
21 | 4 | limsupltOLD 13539 |
. . . . . . . 8
 
    
             |
22 | 14, 18, 20, 21 | syl3anc 1268 |
. . . . . . 7
                          |
23 | 8, 22 | mpbid 214 |
. . . . . 6
                    |
24 | | fzfi 12185 |
. . . . . . . 8
         |
25 | 15 | adantr 467 |
. . . . . . . . . 10
                           |
26 | | elfzuz 11796 |
. . . . . . . . . . 11
        
      |
27 | 26, 9 | syl6eleqr 2540 |
. . . . . . . . . 10
        
  |
28 | | ffvelrn 6020 |
. . . . . . . . . 10
     
       |
29 | 25, 27, 28 | syl2an 480 |
. . . . . . . . 9
             
       
               |
30 | 29 | ralrimiva 2802 |
. . . . . . . 8
                                     |
31 | | fimaxre3 10553 |
. . . . . . . 8
          
                            
  |
32 | 24, 30, 31 | sylancr 669 |
. . . . . . 7
                                   
  |
33 | | simpr 463 |
. . . . . . . . . 10
               |
34 | 33 | ad2antrr 732 |
. . . . . . . . 9
             
                      
 
  |
35 | 4 | limsupgf 13533 |
. . . . . . . . . 10
     |
36 | 35 | ffvelrni 6021 |
. . . . . . . . 9
       |
37 | 34, 36 | syl 17 |
. . . . . . . 8
             
                      
 
      |
38 | | simprl 764 |
. . . . . . . . . 10
             
                      
 
  |
39 | 16, 38 | sseldi 3430 |
. . . . . . . . 9
             
                      
 
  |
40 | | simprl 764 |
. . . . . . . . . . 11
                       |
41 | 40 | adantr 467 |
. . . . . . . . . 10
             
                      
 
  |
42 | 35 | ffvelrni 6021 |
. . . . . . . . . 10
       |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
             
                      
 
      |
44 | 39, 43 | ifcld 3924 |
. . . . . . . 8
             
                      
 
     
         |
45 | 19 | a1i 11 |
. . . . . . . 8
             
                      
 
  |
46 | 40 | ad2antrr 732 |
. . . . . . . . . . . 12
                                     
 
   |
47 | 13 | a1i 11 |
. . . . . . . . . . . . 13
             
                      
 
  |
48 | 47 | sselda 3432 |
. . . . . . . . . . . 12
                                     
 
   |
49 | | xrleid 11449 |
. . . . . . . . . . . . . . . . 17
    
          |
50 | 43, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
             
                      
 
          |
51 | 18 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
             
                      
 
      |
52 | 4 | limsupgle 13535 |
. . . . . . . . . . . . . . . . 17
       
               
            |
53 | 47, 51, 41, 43, 52 | syl211anc 1274 |
. . . . . . . . . . . . . . . 16
             
                      
 
          
   
        |
54 | 50, 53 | mpbid 214 |
. . . . . . . . . . . . . . 15
             
                      
 


           |
55 | 54 | r19.21bi 2757 |
. . . . . . . . . . . . . 14
                                     
 
 
           |
56 | 55 | imp 431 |
. . . . . . . . . . . . 13
                                      
 
            |
57 | 46, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
                                     
 
       |
58 | 39 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                     
 
   |
59 | | xrmax1 11470 |
. . . . . . . . . . . . . . . 16
                          |
60 | 57, 58, 59 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                                     
 
                    |
61 | 51 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . 16
                                     
 
       |
62 | 44 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                     
 
                |
63 | | xrletr 11455 |
. . . . . . . . . . . . . . . 16
               
                     
     
       
                    |
64 | 61, 57, 62, 63 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
                                     
 
              
     
       
                    |
65 | 60, 64 | mpan2d 680 |
. . . . . . . . . . . . . 14
                                     
 
     
                        |
66 | 65 | adantr 467 |
. . . . . . . . . . . . 13
                                      
 
      
                        |
67 | 56, 66 | mpd 15 |
. . . . . . . . . . . 12
                                      
 
                     |
68 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
                                     
 
   |
69 | 68, 9 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . 17
                                     
 
       |
70 | 41 | flcld 12034 |
. . . . . . . . . . . . . . . . . 18
             
                      
 
      |
71 | 70 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                                     
 
       |
72 | | elfz5 11792 |
. . . . . . . . . . . . . . . . 17
                   
       |
73 | 69, 71, 72 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                                     
 
         
       |
74 | 11, 68 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17
                                     
 
   |
75 | | flge 12041 |
. . . . . . . . . . . . . . . . 17
 
         |
76 | 46, 74, 75 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                                     
 
 
       |
77 | 73, 76 | bitr4d 260 |
. . . . . . . . . . . . . . 15
                                     
 
         
   |
78 | 77 | biimpar 488 |
. . . . . . . . . . . . . 14
                                      
 
            |
79 | | simprr 766 |
. . . . . . . . . . . . . . 15
             
                      
 
             
  |
80 | 79 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                                      
 
               
  |
81 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
82 | 81 | breq1d 4412 |
. . . . . . . . . . . . . . 15
     
       |
83 | 82 | rspcv 3146 |
. . . . . . . . . . . . . 14
        
 
            
       |
84 | 78, 80, 83 | sylc 62 |
. . . . . . . . . . . . 13
                                      
 
        |
85 | | xrmax2 11471 |
. . . . . . . . . . . . . . . . 17
                      |
86 | 43, 39, 85 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
             
                      
 
               |
87 | 86 | adantr 467 |
. . . . . . . . . . . . . . 15
                                     
 
                |
88 | | xrletr 11455 |
. . . . . . . . . . . . . . . 16
           
             
     
       
                    |
89 | 61, 58, 62, 88 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
                                     
 
      
     
       
                    |
90 | 87, 89 | mpan2d 680 |
. . . . . . . . . . . . . 14
                                     
 
     
                    |
91 | 90 | adantr 467 |
. . . . . . . . . . . . 13
                                      
 
      
                    |
92 | 84, 91 | mpd 15 |
. . . . . . . . . . . 12
                                      
 
                     |
93 | 46, 48, 67, 92 | lecasei 9740 |
. . . . . . . . . . 11
                                     
 
                    |
94 | 93 | a1d 26 |
. . . . . . . . . 10
                                     
 
 
                    |
95 | 94 | ralrimiva 2802 |
. . . . . . . . 9
             
                      
 


                    |
96 | 4 | limsupgle 13535 |
. . . . . . . . . 10
       
                                     
     
           |
97 | 47, 51, 34, 44, 96 | syl211anc 1274 |
. . . . . . . . 9
             
                      
 
                 


                     |
98 | 95, 97 | mpbird 236 |
. . . . . . . 8
             
                      
 
                   |
99 | | ltpnf 11422 |
. . . . . . . . . 10
   |
100 | 38, 99 | syl 17 |
. . . . . . . . 9
             
                      
 
  |
101 | | simplrr 771 |
. . . . . . . . 9
             
                      
 
      |
102 | | breq1 4405 |
. . . . . . . . . 10
                               |
103 | | breq1 4405 |
. . . . . . . . . 10
                                       |
104 | 102, 103 | ifboth 3917 |
. . . . . . . . 9
                      |
105 | 100, 101,
104 | syl2anc 667 |
. . . . . . . 8
             
                      
 
     
         |
106 | 37, 44, 45, 98, 105 | xrlelttrd 11457 |
. . . . . . 7
             
                      
 
      |
107 | 32, 106 | rexlimddv 2883 |
. . . . . 6
                           |
108 | 23, 107 | rexlimddv 2883 |
. . . . 5
                   |
109 | 7, 108 | eqbrtrrd 4425 |
. . . 4
                        
   |
110 | | imassrn 5179 |
. . . . . . . . 9
        |
111 | | frn 5735 |
. . . . . . . . . 10
    
  |
112 | 15, 111 | syl 17 |
. . . . . . . . 9
               |
113 | 110, 112 | syl5ss 3443 |
. . . . . . . 8
                      |
114 | 113, 16 | syl6ss 3444 |
. . . . . . 7
                      |
115 | | df-ss 3418 |
. . . . . . 7
                
         |
116 | 114, 115 | sylib 200 |
. . . . . 6
                  
 
     
    |
117 | 116, 113 | eqsstrd 3466 |
. . . . 5
                  
 
   |
118 | | simpl1 1011 |
. . . . . . . . . . 11
               |
119 | | flcl 12031 |
. . . . . . . . . . . . . 14
       |
120 | 119 | adantl 468 |
. . . . . . . . . . . . 13
                   |
121 | 120 | peano2zd 11043 |
. . . . . . . . . . . 12
                     |
122 | 121, 118 | ifcld 3924 |
. . . . . . . . . . 11
              
                 |
123 | 118 | zred 11040 |
. . . . . . . . . . . 12
               |
124 | 121 | zred 11040 |
. . . . . . . . . . . 12
                     |
125 | | max1 11480 |
. . . . . . . . . . . 12
          
                 |
126 | 123, 124,
125 | syl2anc 667 |
. . . . . . . . . . 11
                                |
127 | | eluz2 11165 |
. . . . . . . . . . 11
                     
  
                                   |
128 | 118, 122,
126, 127 | syl3anbrc 1192 |
. . . . . . . . . 10
              
                     |
129 | 128, 9 | syl6eleqr 2540 |
. . . . . . . . 9
              
                 |
130 | | fdm 5733 |
. . . . . . . . . 10
       |
131 | 15, 130 | syl 17 |
. . . . . . . . 9
               |
132 | 129, 131 | eleqtrrd 2532 |
. . . . . . . 8
              
                 |
133 | 122 | zred 11040 |
. . . . . . . . 9
              
                 |
134 | | fllep1 12037 |
. . . . . . . . . . 11
         |
135 | 134 | adantl 468 |
. . . . . . . . . 10
                     |
136 | | max2 11482 |
. . . . . . . . . . 11
                
                 |
137 | 123, 124,
136 | syl2anc 667 |
. . . . . . . . . 10
                                      |
138 | 33, 124, 133, 135, 137 | letrd 9792 |
. . . . . . . . 9
                                |
139 | | elicopnf 11730 |
. . . . . . . . . 10
                     
  
                                    |
140 | 139 | adantl 468 |
. . . . . . . . 9
                                 
  
                                    |
141 | 133, 138,
140 | mpbir2and 933 |
. . . . . . . 8
              
                    |
142 | | inelcm 3819 |
. . . . . . . 8
                                               |
143 | 132, 141,
142 | syl2anc 667 |
. . . . . . 7
                    |
144 | | imadisj 5187 |
. . . . . . . 8
       
       |
145 | 144 | necon3bii 2676 |
. . . . . . 7
               |
146 | 143, 145 | sylibr 216 |
. . . . . 6
                      |
147 | 116, 146 | eqnetrd 2691 |
. . . . 5
                  
 
   |
148 | | supxrre1 11616 |
. . . . 5
                
 
 
            

           
    |
149 | 117, 147,
148 | syl2anc 667 |
. . . 4
                         

           
    |
150 | 109, 149 | mpbird 236 |
. . 3
                        
   |
151 | 7, 150 | eqeltrd 2529 |
. 2
                   |
152 | 3, 5, 151 | fmpt2d 6053 |
1
                 |