Step | Hyp | Ref
| Expression |
1 | | 0red 9641 |
. . 3
   |
2 | | stirlinglem11.3 |
. . . . . 6
                       |
3 | 2 | a1i 11 |
. . . . 5
                         |
4 | | simpr 463 |
. . . . . . . . 9
 
   |
5 | 4 | oveq2d 6304 |
. . . . . . . 8
 
       |
6 | 5 | oveq1d 6303 |
. . . . . . 7
 
           |
7 | 6 | oveq2d 6304 |
. . . . . 6
 
               |
8 | 5 | oveq2d 6304 |
. . . . . 6
 
                           |
9 | 7, 8 | oveq12d 6306 |
. . . . 5
 
                                           |
10 | | 1nn 10617 |
. . . . . 6
 |
11 | 10 | a1i 11 |
. . . . 5
   |
12 | | 2cnd 10679 |
. . . . . . . . 9
   |
13 | | 1cnd 9656 |
. . . . . . . . 9
   |
14 | 12, 13 | mulcld 9660 |
. . . . . . . 8
     |
15 | 14, 13 | addcld 9659 |
. . . . . . 7
       |
16 | | 2t1e2 10755 |
. . . . . . . . . . 11
   |
17 | 16 | oveq1i 6298 |
. . . . . . . . . 10
       |
18 | | 2p1e3 10730 |
. . . . . . . . . 10
   |
19 | 17, 18 | eqtri 2472 |
. . . . . . . . 9
     |
20 | | 3ne0 10701 |
. . . . . . . . 9
 |
21 | 19, 20 | eqnetri 2693 |
. . . . . . . 8
     |
22 | 21 | a1i 11 |
. . . . . . 7
       |
23 | 15, 22 | reccld 10373 |
. . . . . 6
         |
24 | | nncn 10614 |
. . . . . . . . . 10
   |
25 | 12, 24 | mulcld 9660 |
. . . . . . . . 9
     |
26 | 25, 13 | addcld 9659 |
. . . . . . . 8
       |
27 | | 1red 9655 |
. . . . . . . . . 10
   |
28 | | 2re 10676 |
. . . . . . . . . . . . 13
 |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
   |
30 | | nnre 10613 |
. . . . . . . . . . . 12
   |
31 | 29, 30 | remulcld 9668 |
. . . . . . . . . . 11
     |
32 | 31, 27 | readdcld 9667 |
. . . . . . . . . 10
       |
33 | | 0lt1 10133 |
. . . . . . . . . . 11
 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
   |
35 | | 2rp 11304 |
. . . . . . . . . . . . 13
 |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
   |
37 | | nnrp 11308 |
. . . . . . . . . . . 12
   |
38 | 36, 37 | rpmulcld 11354 |
. . . . . . . . . . 11
     |
39 | 27, 38 | ltaddrp2d 11369 |
. . . . . . . . . 10
       |
40 | 1, 27, 32, 34, 39 | lttrd 9793 |
. . . . . . . . 9
       |
41 | 40 | gt0ne0d 10175 |
. . . . . . . 8
       |
42 | 26, 41 | reccld 10373 |
. . . . . . 7
         |
43 | | 2nn0 10883 |
. . . . . . . . 9
 |
44 | 43 | a1i 11 |
. . . . . . . 8
   |
45 | | 1nn0 10882 |
. . . . . . . . 9
 |
46 | 45 | a1i 11 |
. . . . . . . 8
   |
47 | 44, 46 | nn0mulcld 10927 |
. . . . . . 7
     |
48 | 42, 47 | expcld 12413 |
. . . . . 6
               |
49 | 23, 48 | mulcld 9660 |
. . . . 5
                       |
50 | 3, 9, 11, 49 | fvmptd 5952 |
. . . 4
                           |
51 | | 1re 9639 |
. . . . . . . . 9
 |
52 | 28, 51 | remulcli 9654 |
. . . . . . . 8
   |
53 | 52, 51 | readdcli 9653 |
. . . . . . 7
     |
54 | 53, 21 | rereccli 10369 |
. . . . . 6
       |
55 | 54 | a1i 11 |
. . . . 5
         |
56 | 32, 41 | rereccld 10431 |
. . . . . 6
         |
57 | 56, 47 | reexpcld 12430 |
. . . . 5
               |
58 | 55, 57 | remulcld 9668 |
. . . 4
                       |
59 | 50, 58 | eqeltrd 2528 |
. . 3
       |
60 | | stirlinglem11.1 |
. . . . . . . 8
                       |
61 | 60 | stirlinglem2 37931 |
. . . . . . 7
       |
62 | 61 | relogcld 23565 |
. . . . . 6
           |
63 | | nfcv 2591 |
. . . . . . 7
   |
64 | | nfcv 2591 |
. . . . . . . 8
   |
65 | | nfmpt1 4491 |
. . . . . . . . . 10
                         |
66 | 60, 65 | nfcxfr 2589 |
. . . . . . . . 9
   |
67 | 66, 63 | nffv 5870 |
. . . . . . . 8
       |
68 | 64, 67 | nffv 5870 |
. . . . . . 7
           |
69 | | fveq2 5863 |
. . . . . . . 8
           |
70 | 69 | fveq2d 5867 |
. . . . . . 7
                   |
71 | | stirlinglem11.2 |
. . . . . . 7
           |
72 | 63, 68, 70, 71 | fvmptf 5964 |
. . . . . 6
                         |
73 | 62, 72 | mpdan 673 |
. . . . 5
               |
74 | 73, 62 | eqeltrd 2528 |
. . . 4
       |
75 | | peano2nn 10618 |
. . . . . 6
 
   |
76 | 60 | stirlinglem2 37931 |
. . . . . . . 8
           |
77 | 75, 76 | syl 17 |
. . . . . . 7
         |
78 | 77 | relogcld 23565 |
. . . . . 6
       
     |
79 | | nfcv 2591 |
. . . . . . 7
     |
80 | 66, 79 | nffv 5870 |
. . . . . . . 8
     
   |
81 | 64, 80 | nffv 5870 |
. . . . . . 7
             |
82 | | fveq2 5863 |
. . . . . . . 8
          
    |
83 | 82 | fveq2d 5867 |
. . . . . . 7
                       |
84 | 79, 81, 83, 71 | fvmptf 5964 |
. . . . . 6
                  
        
     |
85 | 75, 78, 84 | syl2anc 666 |
. . . . 5
                   |
86 | 85, 78 | eqeltrd 2528 |
. . . 4
         |
87 | 74, 86 | resubcld 10044 |
. . 3
               |
88 | 29, 27 | remulcld 9668 |
. . . . . . . 8
     |
89 | | 0le2 10697 |
. . . . . . . . . 10
 |
90 | 89 | a1i 11 |
. . . . . . . . 9
   |
91 | | 0le1 10134 |
. . . . . . . . . 10
 |
92 | 91 | a1i 11 |
. . . . . . . . 9
   |
93 | 29, 27, 90, 92 | mulge0d 10187 |
. . . . . . . 8
     |
94 | 88, 93 | ge0p1rpd 11365 |
. . . . . . 7
       |
95 | 94 | rpreccld 11348 |
. . . . . 6
         |
96 | 37 | rpge0d 11342 |
. . . . . . . . . 10
   |
97 | 29, 30, 90, 96 | mulge0d 10187 |
. . . . . . . . 9
     |
98 | 31, 97 | ge0p1rpd 11365 |
. . . . . . . 8
       |
99 | 98 | rpreccld 11348 |
. . . . . . 7
         |
100 | | 2z 10966 |
. . . . . . . . 9
 |
101 | 100 | a1i 11 |
. . . . . . . 8
   |
102 | | 1z 10964 |
. . . . . . . . 9
 |
103 | 102 | a1i 11 |
. . . . . . . 8
   |
104 | 101, 103 | zmulcld 11043 |
. . . . . . 7
     |
105 | 99, 104 | rpexpcld 12436 |
. . . . . 6
               |
106 | 95, 105 | rpmulcld 11354 |
. . . . 5
                       |
107 | 50, 106 | eqeltrd 2528 |
. . . 4
       |
108 | 107 | rpgt0d 11341 |
. . 3
       |
109 | 87, 59 | resubcld 10044 |
. . . . 5
                     |
110 | | eqid 2450 |
. . . . . . 7
             |
111 | 103 | peano2zd 11040 |
. . . . . . 7
     |
112 | | nnuz 11191 |
. . . . . . . 8
     |
113 | 2 | a1i 11 |
. . . . . . . . . 10
 
                         |
114 | | oveq2 6296 |
. . . . . . . . . . . . . 14
       |
115 | 114 | oveq1d 6303 |
. . . . . . . . . . . . 13
           |
116 | 115 | oveq2d 6304 |
. . . . . . . . . . . 12
               |
117 | 114 | oveq2d 6304 |
. . . . . . . . . . . 12
                           |
118 | 116, 117 | oveq12d 6306 |
. . . . . . . . . . 11
                                           |
119 | 118 | adantl 468 |
. . . . . . . . . 10
    
                                          |
120 | | simpr 463 |
. . . . . . . . . 10
 
   |
121 | | 2cnd 10679 |
. . . . . . . . . . . . . 14
 
   |
122 | | nncn 10614 |
. . . . . . . . . . . . . . 15
   |
123 | 122 | adantl 468 |
. . . . . . . . . . . . . 14
 
   |
124 | 121, 123 | mulcld 9660 |
. . . . . . . . . . . . 13
 
     |
125 | | 1cnd 9656 |
. . . . . . . . . . . . 13
 
   |
126 | 124, 125 | addcld 9659 |
. . . . . . . . . . . 12
 
       |
127 | | 0red 9641 |
. . . . . . . . . . . . . 14
 
   |
128 | | 1red 9655 |
. . . . . . . . . . . . . 14
 
   |
129 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
130 | | nnre 10613 |
. . . . . . . . . . . . . . . . 17
   |
131 | 130 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
   |
132 | 129, 131 | remulcld 9668 |
. . . . . . . . . . . . . . 15
 
     |
133 | 132, 128 | readdcld 9667 |
. . . . . . . . . . . . . 14
 
       |
134 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
135 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
136 | | nnrp 11308 |
. . . . . . . . . . . . . . . . 17
   |
137 | 136 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
   |
138 | 135, 137 | rpmulcld 11354 |
. . . . . . . . . . . . . . 15
 
     |
139 | 128, 138 | ltaddrp2d 11369 |
. . . . . . . . . . . . . 14
 
       |
140 | 127, 128,
133, 134, 139 | lttrd 9793 |
. . . . . . . . . . . . 13
 
       |
141 | 140 | gt0ne0d 10175 |
. . . . . . . . . . . 12
 
       |
142 | 126, 141 | reccld 10373 |
. . . . . . . . . . 11
 
         |
143 | 24 | adantr 467 |
. . . . . . . . . . . . . . 15
 
   |
144 | 121, 143 | mulcld 9660 |
. . . . . . . . . . . . . 14
 
     |
145 | 144, 125 | addcld 9659 |
. . . . . . . . . . . . 13
 
       |
146 | 41 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
147 | 145, 146 | reccld 10373 |
. . . . . . . . . . . 12
 
         |
148 | 43 | a1i 11 |
. . . . . . . . . . . . 13
 
   |
149 | | nnnn0 10873 |
. . . . . . . . . . . . . 14
   |
150 | 149 | adantl 468 |
. . . . . . . . . . . . 13
 
   |
151 | 148, 150 | nn0mulcld 10927 |
. . . . . . . . . . . 12
 
     |
152 | 147, 151 | expcld 12413 |
. . . . . . . . . . 11
 
               |
153 | 142, 152 | mulcld 9660 |
. . . . . . . . . 10
 
                       |
154 | 113, 119,
120, 153 | fvmptd 5952 |
. . . . . . . . 9
 
                           |
155 | | 0red 9641 |
. . . . . . . . . . . . . 14
   |
156 | | 1red 9655 |
. . . . . . . . . . . . . 14
   |
157 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
158 | 157, 130 | remulcld 9668 |
. . . . . . . . . . . . . . 15
     |
159 | 158, 156 | readdcld 9667 |
. . . . . . . . . . . . . 14
       |
160 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
   |
161 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
162 | 161, 136 | rpmulcld 11354 |
. . . . . . . . . . . . . . 15
     |
163 | 156, 162 | ltaddrp2d 11369 |
. . . . . . . . . . . . . 14
       |
164 | 155, 156,
159, 160, 163 | lttrd 9793 |
. . . . . . . . . . . . 13
       |
165 | 164 | gt0ne0d 10175 |
. . . . . . . . . . . 12
       |
166 | 165 | adantl 468 |
. . . . . . . . . . 11
 
       |
167 | 126, 166 | reccld 10373 |
. . . . . . . . . 10
 
         |
168 | 167, 152 | mulcld 9660 |
. . . . . . . . 9
 
                       |
169 | 154, 168 | eqeltrd 2528 |
. . . . . . . 8
 
       |
170 | | eqid 2450 |
. . . . . . . . 9
                                         |
171 | 60, 71, 170, 2 | stirlinglem9 37938 |
. . . . . . . 8
            
     |
172 | 112, 11, 169, 171 | clim2ser 13711 |
. . . . . . 7
                            |
173 | | peano2nn 10618 |
. . . . . . . . . . . . 13
     |
174 | | uznnssnn 11203 |
. . . . . . . . . . . . 13
           |
175 | 10, 173, 174 | mp2b 10 |
. . . . . . . . . . . 12
       |
176 | 175 | a1i 11 |
. . . . . . . . . . 11
         |
177 | 176 | sseld 3430 |
. . . . . . . . . 10
           |
178 | 177 | imdistani 695 |
. . . . . . . . 9
 
           |
179 | 178, 154 | syl 17 |
. . . . . . . 8
 
                                 |
180 | 28 | a1i 11 |
. . . . . . . . . . . . 13
      
  |
181 | | eluzelre 11166 |
. . . . . . . . . . . . 13
      
  |
182 | 180, 181 | remulcld 9668 |
. . . . . . . . . . . 12
      
    |
183 | | 1red 9655 |
. . . . . . . . . . . 12
      
  |
184 | 182, 183 | readdcld 9667 |
. . . . . . . . . . 11
      
      |
185 | 175 | sseli 3427 |
. . . . . . . . . . . 12
      
  |
186 | 185, 165 | syl 17 |
. . . . . . . . . . 11
      
      |
187 | 184, 186 | rereccld 10431 |
. . . . . . . . . 10
      
        |
188 | 187 | adantl 468 |
. . . . . . . . 9
 
               |
189 | 32 | adantr 467 |
. . . . . . . . . . 11
 
             |
190 | 41 | adantr 467 |
. . . . . . . . . . 11
 
             |
191 | 189, 190 | rereccld 10431 |
. . . . . . . . . 10
 
               |
192 | 178, 151 | syl 17 |
. . . . . . . . . 10
 
           |
193 | 191, 192 | reexpcld 12430 |
. . . . . . . . 9
 
                     |
194 | 188, 193 | remulcld 9668 |
. . . . . . . 8
 
                             |
195 | 179, 194 | eqeltrd 2528 |
. . . . . . 7
 
             |
196 | | 1red 9655 |
. . . . . . . . . 10
 
         |
197 | 28 | a1i 11 |
. . . . . . . . . . . 12
 
         |
198 | 178, 131 | syl 17 |
. . . . . . . . . . . 12
 
         |
199 | 197, 198 | remulcld 9668 |
. . . . . . . . . . 11
 
           |
200 | 89 | a1i 11 |
. . . . . . . . . . . 12
 
      
  |
201 | | 0red 9641 |
. . . . . . . . . . . . . 14
      
  |
202 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
      
  |
203 | | 1p1e2 10720 |
. . . . . . . . . . . . . . 15
   |
204 | | eluzle 11168 |
. . . . . . . . . . . . . . 15
      
    |
205 | 203, 204 | syl5eqbrr 4436 |
. . . . . . . . . . . . . 14
      
  |
206 | 201, 180,
181, 202, 205 | letrd 9789 |
. . . . . . . . . . . . 13
      
  |
207 | 206 | adantl 468 |
. . . . . . . . . . . 12
 
      
  |
208 | 197, 198,
200, 207 | mulge0d 10187 |
. . . . . . . . . . 11
 
      
    |
209 | 199, 208 | ge0p1rpd 11365 |
. . . . . . . . . 10
 
             |
210 | 91 | a1i 11 |
. . . . . . . . . 10
 
      
  |
211 | 196, 209,
210 | divge0d 11375 |
. . . . . . . . 9
 
      
        |
212 | 30 | adantr 467 |
. . . . . . . . . . . . 13
 
      
  |
213 | 197, 212 | remulcld 9668 |
. . . . . . . . . . . 12
 
           |
214 | 96 | adantr 467 |
. . . . . . . . . . . . 13
 
      
  |
215 | 197, 212,
200, 214 | mulge0d 10187 |
. . . . . . . . . . . 12
 
      
    |
216 | 213, 215 | ge0p1rpd 11365 |
. . . . . . . . . . 11
 
             |
217 | 196, 216,
210 | divge0d 11375 |
. . . . . . . . . 10
 
      
        |
218 | 191, 192,
217 | expge0d 12431 |
. . . . . . . . 9
 
      
              |
219 | 188, 193,
211, 218 | mulge0d 10187 |
. . . . . . . 8
 
      
                      |
220 | 219, 179 | breqtrrd 4428 |
. . . . . . 7
 
      
      |
221 | 110, 111,
172, 195, 220 | iserge0 13717 |
. . . . . 6
                       |
222 | | seq1 12223 |
. . . . . . . 8
             |
223 | 102, 222 | mp1i 13 |
. . . . . . 7
             |
224 | 223 | oveq2d 6304 |
. . . . . 6
                                         |
225 | 221, 224 | breqtrd 4426 |
. . . . 5
                     |
226 | 1, 109, 59, 225 | leadd1dd 10224 |
. . . 4
                                 |
227 | 50, 49 | eqeltrd 2528 |
. . . . 5
       |
228 | 227 | addid2d 9831 |
. . . 4
             |
229 | 74 | recnd 9666 |
. . . . . 6
       |
230 | 86 | recnd 9666 |
. . . . . 6
         |
231 | 229, 230 | subcld 9983 |
. . . . 5
               |
232 | 231, 227 | npcand 9987 |
. . . 4
                                       |
233 | 226, 228,
232 | 3brtr3d 4431 |
. . 3
                   |
234 | 1, 59, 87, 108, 233 | ltletrd 9792 |
. 2
               |
235 | 86, 74 | posdifd 10197 |
. 2
     
     
               |
236 | 234, 235 | mpbird 236 |
1
             |