Step | Hyp | Ref
| Expression |
1 | | nnuz 11201 |
. . . . 5
     |
2 | | 1zzd 10975 |
. . . . 5
   |
3 | | stirlinglem5.1 |
. . . . . . . . 9
                  |
4 | 3 | a1i 11 |
. . . . . . . 8
                    |
5 | | 1cnd 9664 |
. . . . . . . . . . . . 13
 

  |
6 | 5 | negcld 9978 |
. . . . . . . . . . . 12
 

   |
7 | | nnm1nn0 10918 |
. . . . . . . . . . . . 13
     |
8 | 7 | adantl 468 |
. . . . . . . . . . . 12
 

    |
9 | 6, 8 | expcld 12423 |
. . . . . . . . . . 11
 

         |
10 | | nncn 10624 |
. . . . . . . . . . . 12
   |
11 | 10 | adantl 468 |
. . . . . . . . . . 11
 

  |
12 | | stirlinglem5.6 |
. . . . . . . . . . . . . . 15
   |
13 | 12 | rpred 11348 |
. . . . . . . . . . . . . 14
   |
14 | 13 | recnd 9674 |
. . . . . . . . . . . . 13
   |
15 | 14 | adantr 467 |
. . . . . . . . . . . 12
 

  |
16 | | nnnn0 10883 |
. . . . . . . . . . . . 13
   |
17 | 16 | adantl 468 |
. . . . . . . . . . . 12
 

  |
18 | 15, 17 | expcld 12423 |
. . . . . . . . . . 11
 

      |
19 | | nnne0 10649 |
. . . . . . . . . . . 12
   |
20 | 19 | adantl 468 |
. . . . . . . . . . 11
 

  |
21 | 9, 11, 18, 20 | div32d 10413 |
. . . . . . . . . 10
 

                                |
22 | 5, 15 | pncan2d 9993 |
. . . . . . . . . . . . 13
 

      |
23 | 22 | eqcomd 2459 |
. . . . . . . . . . . 12
 

      |
24 | 23 | oveq1d 6310 |
. . . . . . . . . . 11
 

              |
25 | 24 | oveq2d 6311 |
. . . . . . . . . 10
 

                                    |
26 | 21, 25 | eqtr3d 2489 |
. . . . . . . . 9
 

                                    |
27 | 26 | mpteq2dva 4492 |
. . . . . . . 8
                                         |
28 | 4, 27 | eqtrd 2487 |
. . . . . . 7
                        |
29 | 28 | seqeq3d 12228 |
. . . . . 6
                              |
30 | | 1cnd 9664 |
. . . . . . . . . 10
   |
31 | 30, 14 | addcld 9667 |
. . . . . . . . . 10
     |
32 | | eqid 2453 |
. . . . . . . . . . 11

  |
33 | 32 | cnmetdval 21803 |
. . . . . . . . . 10
                      |
34 | 30, 31, 33 | syl2anc 667 |
. . . . . . . . 9
   
              |
35 | | 1m1e0 10685 |
. . . . . . . . . . . . . 14
   |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
     |
37 | 36 | oveq1d 6310 |
. . . . . . . . . . . 12
         |
38 | 30, 30, 14 | subsub4d 10022 |
. . . . . . . . . . . 12
           |
39 | | df-neg 9868 |
. . . . . . . . . . . . . 14
    |
40 | 39 | eqcomi 2462 |
. . . . . . . . . . . . 13
    |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
      |
42 | 37, 38, 41 | 3eqtr3d 2495 |
. . . . . . . . . . 11
        |
43 | 42 | fveq2d 5874 |
. . . . . . . . . 10
                |
44 | 14 | absnegd 13523 |
. . . . . . . . . . 11
            |
45 | | stirlinglem5.7 |
. . . . . . . . . . 11
    
  |
46 | 44, 45 | eqbrtrd 4426 |
. . . . . . . . . 10
     
  |
47 | 43, 46 | eqbrtrd 4426 |
. . . . . . . . 9
           |
48 | 34, 47 | eqbrtrd 4426 |
. . . . . . . 8
   
      |
49 | | cnxmet 21805 |
. . . . . . . . . 10

      |
50 | 49 | a1i 11 |
. . . . . . . . 9
 
       |
51 | | 1red 9663 |
. . . . . . . . . 10
   |
52 | 51 | rexrd 9695 |
. . . . . . . . 9
   |
53 | | elbl2 21417 |
. . . . . . . . 9
   
                      
          |
54 | 50, 52, 30, 31, 53 | syl22anc 1270 |
. . . . . . . 8
            
          |
55 | 48, 54 | mpbird 236 |
. . . . . . 7
              |
56 | | eqid 2453 |
. . . . . . . 8
                   |
57 | 56 | logtayl2 23619 |
. . . . . . 7
           
                                |
58 | 55, 57 | syl 17 |
. . . . . 6
                                 |
59 | 29, 58 | eqbrtrd 4426 |
. . . . 5
            |
60 | | seqex 12222 |
. . . . . 6
    |
61 | 60 | a1i 11 |
. . . . 5
      |
62 | | stirlinglem5.2 |
. . . . . . . 8
         |
63 | 62 | a1i 11 |
. . . . . . 7
           |
64 | 63 | seqeq3d 12228 |
. . . . . 6
                 |
65 | | logtayl 23617 |
. . . . . . 7
                           |
66 | 14, 45, 65 | syl2anc 667 |
. . . . . 6
                     |
67 | 64, 66 | eqbrtrd 4426 |
. . . . 5
             |
68 | | simpr 463 |
. . . . . . 7
 

  |
69 | 68, 1 | syl6eleq 2541 |
. . . . . 6
 

      |
70 | 3 | a1i 11 |
. . . . . . . 8
                            |
71 | | oveq1 6302 |
. . . . . . . . . . 11
       |
72 | 71 | oveq2d 6311 |
. . . . . . . . . 10
                 |
73 | | oveq2 6303 |
. . . . . . . . . . 11
           |
74 | | id 22 |
. . . . . . . . . . 11
   |
75 | 73, 74 | oveq12d 6313 |
. . . . . . . . . 10
               |
76 | 72, 75 | oveq12d 6313 |
. . . . . . . . 9
                                 |
77 | 76 | adantl 468 |
. . . . . . . 8
   

     
                                |
78 | | elfznn 11835 |
. . . . . . . . 9
       |
79 | 78 | adantl 468 |
. . . . . . . 8
           |
80 | | 1cnd 9664 |
. . . . . . . . . . . 12
   |
81 | 80 | negcld 9978 |
. . . . . . . . . . 11
    |
82 | | nnm1nn0 10918 |
. . . . . . . . . . 11
     |
83 | 81, 82 | expcld 12423 |
. . . . . . . . . 10
          |
84 | 79, 83 | syl 17 |
. . . . . . . . 9
                  |
85 | 14 | ad2antrr 733 |
. . . . . . . . . . 11
           |
86 | 79 | nnnn0d 10932 |
. . . . . . . . . . 11
           |
87 | 85, 86 | expcld 12423 |
. . . . . . . . . 10
               |
88 | 79 | nncnd 10632 |
. . . . . . . . . 10
           |
89 | 79 | nnne0d 10661 |
. . . . . . . . . 10
           |
90 | 87, 88, 89 | divcld 10390 |
. . . . . . . . 9
                 |
91 | 84, 90 | mulcld 9668 |
. . . . . . . 8
                          |
92 | 70, 77, 79, 91 | fvmptd 5959 |
. . . . . . 7
                              |
93 | 92, 91 | eqeltrd 2531 |
. . . . . 6
               |
94 | | addcl 9626 |
. . . . . . 7
 
     |
95 | 94 | adantl 468 |
. . . . . 6
    
 
    |
96 | 69, 93, 95 | seqcl 12240 |
. . . . 5
 

        |
97 | 62 | a1i 11 |
. . . . . . . 8
                   |
98 | 75 | adantl 468 |
. . . . . . . 8
   

     
              |
99 | 97, 98, 79, 90 | fvmptd 5959 |
. . . . . . 7
                     |
100 | 99, 90 | eqeltrd 2531 |
. . . . . 6
               |
101 | 69, 100, 95 | seqcl 12240 |
. . . . 5
 

        |
102 | | simpll 761 |
. . . . . . 7
           |
103 | | stirlinglem5.3 |
. . . . . . . . . 10
                          |
104 | 103 | a1i 11 |
. . . . . . . . 9
 

                           |
105 | 76, 75 | oveq12d 6313 |
. . . . . . . . . 10
                                                 |
106 | 105 | adantl 468 |
. . . . . . . . 9
                                                     |
107 | | simpr 463 |
. . . . . . . . 9
 

  |
108 | 83 | adantl 468 |
. . . . . . . . . . 11
 

         |
109 | 14 | adantr 467 |
. . . . . . . . . . . . 13
 

  |
110 | 107 | nnnn0d 10932 |
. . . . . . . . . . . . 13
 

  |
111 | 109, 110 | expcld 12423 |
. . . . . . . . . . . 12
 

      |
112 | 107 | nncnd 10632 |
. . . . . . . . . . . 12
 

  |
113 | 107 | nnne0d 10661 |
. . . . . . . . . . . 12
 

  |
114 | 111, 112,
113 | divcld 10390 |
. . . . . . . . . . 11
 

        |
115 | 108, 114 | mulcld 9668 |
. . . . . . . . . 10
 

                 |
116 | 115, 114 | addcld 9667 |
. . . . . . . . 9
 

                         |
117 | 104, 106,
107, 116 | fvmptd 5959 |
. . . . . . . 8
 

                             |
118 | 3 | a1i 11 |
. . . . . . . . . . 11
 

                   |
119 | 76 | adantl 468 |
. . . . . . . . . . 11
                                     |
120 | 118, 119,
107, 115 | fvmptd 5959 |
. . . . . . . . . 10
 

                     |
121 | 120 | eqcomd 2459 |
. . . . . . . . 9
 

                     |
122 | 62 | a1i 11 |
. . . . . . . . . . 11
 

          |
123 | 75 | adantl 468 |
. . . . . . . . . . 11
                   |
124 | 122, 123,
107, 114 | fvmptd 5959 |
. . . . . . . . . 10
 

            |
125 | 124 | eqcomd 2459 |
. . . . . . . . 9
 

            |
126 | 121, 125 | oveq12d 6313 |
. . . . . . . 8
 

                                   |
127 | 117, 126 | eqtrd 2487 |
. . . . . . 7
 

                |
128 | 102, 79, 127 | syl2anc 667 |
. . . . . 6
                         |
129 | 69, 93, 100, 128 | seradd 12262 |
. . . . 5
 

                      |
130 | 1, 2, 59, 61, 67, 96, 101, 129 | climadd 13707 |
. . . 4
                     |
131 | | 1rp 11313 |
. . . . . . . . 9
 |
132 | 131 | a1i 11 |
. . . . . . . 8
   |
133 | 132, 12 | rpaddcld 11363 |
. . . . . . 7
     |
134 | 133 | rpne0d 11353 |
. . . . . 6
     |
135 | 31, 134 | logcld 23532 |
. . . . 5
         |
136 | 30, 14 | subcld 9991 |
. . . . . 6
     |
137 | 13, 51 | absltd 13503 |
. . . . . . . . . 10
     
      |
138 | 45, 137 | mpbid 214 |
. . . . . . . . 9
  
   |
139 | 138 | simprd 465 |
. . . . . . . 8
   |
140 | 13, 139 | gtned 9775 |
. . . . . . 7
   |
141 | 30, 14, 140 | subne0d 10000 |
. . . . . 6
     |
142 | 136, 141 | logcld 23532 |
. . . . 5
         |
143 | 135, 142 | negsubd 9997 |
. . . 4
                                |
144 | 130, 143 | breqtrd 4430 |
. . 3
                    |
145 | | nn0uz 11200 |
. . . 4
     |
146 | | 0zd 10956 |
. . . 4
   |
147 | | stirlinglem5.5 |
. . . . . 6
       |
148 | | 2nn0 10893 |
. . . . . . . . 9
 |
149 | 148 | a1i 11 |
. . . . . . . 8

  |
150 | | id 22 |
. . . . . . . 8

  |
151 | 149, 150 | nn0mulcld 10937 |
. . . . . . 7

    |
152 | | nn0p1nn 10916 |
. . . . . . 7
  
      |
153 | 151, 152 | syl 17 |
. . . . . 6

      |
154 | 147, 153 | fmpti 6050 |
. . . . 5
     |
155 | 154 | a1i 11 |
. . . 4
       |
156 | | 2re 10686 |
. . . . . . . . 9
 |
157 | 156 | a1i 11 |
. . . . . . . 8

  |
158 | | nn0re 10885 |
. . . . . . . 8

  |
159 | 157, 158 | remulcld 9676 |
. . . . . . 7

    |
160 | | 1red 9663 |
. . . . . . . . 9

  |
161 | 158, 160 | readdcld 9675 |
. . . . . . . 8

    |
162 | 157, 161 | remulcld 9676 |
. . . . . . 7

      |
163 | | 2rp 11314 |
. . . . . . . . 9
 |
164 | 163 | a1i 11 |
. . . . . . . 8

  |
165 | 158 | ltp1d 10544 |
. . . . . . . 8

    |
166 | 158, 161,
164, 165 | ltmul2dd 11401 |
. . . . . . 7

        |
167 | 159, 162,
160, 166 | ltadd1dd 10231 |
. . . . . 6

            |
168 | 147 | a1i 11 |
. . . . . . 7

        |
169 | | simpr 463 |
. . . . . . . . 9
 
   |
170 | 169 | oveq2d 6311 |
. . . . . . . 8
 
       |
171 | 170 | oveq1d 6310 |
. . . . . . 7
 
           |
172 | | id 22 |
. . . . . . 7

  |
173 | | 2cnd 10689 |
. . . . . . . . 9

  |
174 | | nn0cn 10886 |
. . . . . . . . 9

  |
175 | 173, 174 | mulcld 9668 |
. . . . . . . 8

    |
176 | | 1cnd 9664 |
. . . . . . . 8

  |
177 | 175, 176 | addcld 9667 |
. . . . . . 7

      |
178 | 168, 171,
172, 177 | fvmptd 5959 |
. . . . . 6

          |
179 | | simpr 463 |
. . . . . . . . 9
 
       |
180 | 179 | oveq2d 6311 |
. . . . . . . 8
 
           |
181 | 180 | oveq1d 6310 |
. . . . . . 7
 
               |
182 | | peano2nn0 10917 |
. . . . . . 7

    |
183 | 174, 176 | addcld 9667 |
. . . . . . . . 9

    |
184 | 173, 183 | mulcld 9668 |
. . . . . . . 8

      |
185 | 184, 176 | addcld 9667 |
. . . . . . 7

        |
186 | 168, 181,
182, 185 | fvmptd 5959 |
. . . . . 6

              |
187 | 167, 178,
186 | 3brtr4d 4436 |
. . . . 5

            |
188 | 187 | adantl 468 |
. . . 4
 

            |
189 | | eldifi 3557 |
. . . . . . 7
     |
190 | 189 | adantl 468 |
. . . . . 6
 

    |
191 | | 1cnd 9664 |
. . . . . . . . . . 11
     |
192 | 191 | negcld 9978 |
. . . . . . . . . 10
      |
193 | 189, 82 | syl 17 |
. . . . . . . . . 10
       |
194 | 192, 193 | expcld 12423 |
. . . . . . . . 9
            |
195 | 194 | adantl 468 |
. . . . . . . 8
 

           |
196 | 14 | adantr 467 |
. . . . . . . . . 10
 

    |
197 | 190 | nnnn0d 10932 |
. . . . . . . . . 10
 

    |
198 | 196, 197 | expcld 12423 |
. . . . . . . . 9
 

        |
199 | 190 | nncnd 10632 |
. . . . . . . . 9
 

    |
200 | 190 | nnne0d 10661 |
. . . . . . . . 9
 

    |
201 | 198, 199,
200 | divcld 10390 |
. . . . . . . 8
 

          |
202 | 195, 201 | mulcld 9668 |
. . . . . . 7
 

                   |
203 | 202, 201 | addcld 9667 |
. . . . . 6
 

                           |
204 | 105, 103 | fvmptg 5951 |
. . . . . 6
                                                       |
205 | 190, 203,
204 | syl2anc 667 |
. . . . 5
 

                               |
206 | | eldifn 3558 |
. . . . . . . . . . . 12
  
  |
207 | | 0nn0 10891 |
. . . . . . . . . . . . . . . 16
 |
208 | | 1nn0 10892 |
. . . . . . . . . . . . . . . . 17
 |
209 | 148, 208 | num0h 11068 |
. . . . . . . . . . . . . . . 16
     |
210 | | oveq2 6303 |
. . . . . . . . . . . . . . . . . . 19
       |
211 | 210 | oveq1d 6310 |
. . . . . . . . . . . . . . . . . 18
           |
212 | 211 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . 17
     
       |
213 | 212 | rspcev 3152 |
. . . . . . . . . . . . . . . 16
 
     
      |
214 | 207, 209,
213 | mp2an 679 |
. . . . . . . . . . . . . . 15
      |
215 | | ax-1cn 9602 |
. . . . . . . . . . . . . . . 16
 |
216 | 147 | elrnmpt 5084 |
. . . . . . . . . . . . . . . 16
          |
217 | 215, 216 | ax-mp 5 |
. . . . . . . . . . . . . . 15

       |
218 | 214, 217 | mpbir 213 |
. . . . . . . . . . . . . 14
 |
219 | 218 | a1i 11 |
. . . . . . . . . . . . 13
   |
220 | | eleq1 2519 |
. . . . . . . . . . . . 13
     |
221 | 219, 220 | mpbird 236 |
. . . . . . . . . . . 12
   |
222 | 206, 221 | nsyl 125 |
. . . . . . . . . . 11
  
  |
223 | | nn1m1nn 10636 |
. . . . . . . . . . . . 13
       |
224 | 189, 223 | syl 17 |
. . . . . . . . . . . 12
         |
225 | 224 | ord 379 |
. . . . . . . . . . 11
   
     |
226 | 222, 225 | mpd 15 |
. . . . . . . . . 10
       |
227 | | nfcv 2594 |
. . . . . . . . . . . . . . . . . 18
   |
228 | | nfmpt1 4495 |
. . . . . . . . . . . . . . . . . . . 20
         |
229 | 147, 228 | nfcxfr 2592 |
. . . . . . . . . . . . . . . . . . 19
   |
230 | 229 | nfrn 5080 |
. . . . . . . . . . . . . . . . . 18
   |
231 | 227, 230 | nfdif 3556 |
. . . . . . . . . . . . . . . . 17
     |
232 | 231 | nfcri 2588 |
. . . . . . . . . . . . . . . 16
 
  |
233 | 147 | elrnmpt 5084 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
234 | 206, 233 | mtbid 302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
235 | | ralnex 2836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   
       |
236 | 234, 235 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
237 | 236 | r19.21bi 2759 |
. . . . . . . . . . . . . . . . . . . . . 22
  


      |
238 | 237 | neqned 2633 |
. . . . . . . . . . . . . . . . . . . . 21
  

       |
239 | 238 | necomd 2681 |
. . . . . . . . . . . . . . . . . . . 20
  

       |
240 | 239 | adantlr 722 |
. . . . . . . . . . . . . . . . . . 19
    

       |
241 | | simplr 763 |
. . . . . . . . . . . . . . . . . . . 20
    

   |
242 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
    


  |
243 | 189 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . 20
    

   |
244 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
245 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
246 | 245 | zred 11047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
247 | 244, 246 | remulcld 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     |
248 | | 0red 9649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
249 | | 1red 9663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
250 | | 2cnd 10689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
251 | 246 | recnd 9674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
252 | 250, 251 | mulcomd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       |
253 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 

  |
254 | | elnn0z 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

    |
255 | 253, 254 | sylnib 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 

    |
256 | | nan 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
  
    
   |
257 | 255, 256 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
  |
258 | 257 | anabss1 824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

  |
259 | 246, 248 | ltnled 9787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
 
   |
260 | 258, 259 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
261 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
262 | 261 | rpregt0d 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
     |
263 | | mulltgt0 37353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
264 | 246, 260,
262, 263 | syl21anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     |
265 | 252, 264 | eqbrtrd 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     |
266 | 247, 248,
249, 265 | ltadd1dd 10231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
267 | | 1cnd 9664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
268 | 267 | addid2d 9839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
269 | 266, 268 | breqtrd 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
270 | 247, 249 | readdcld 9675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       |
271 | 270, 249 | ltnled 9787 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     
       |
272 | 269, 271 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

      |
273 | | nnge1 10642 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
274 | 272, 273 | nsyl 125 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

      |
275 | 274 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
    
      |
276 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
277 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
278 | 276, 277 | eqeltrd 2531 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
279 | 278 | adantll 721 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
280 | 275, 279 | mtand 665 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
281 | 280 | neqned 2633 |
. . . . . . . . . . . . . . . . . . . 20
           |
282 | 241, 242,
243, 281 | syl21anc 1268 |
. . . . . . . . . . . . . . . . . . 19
    

       |
283 | 240, 282 | pm2.61dan 801 |
. . . . . . . . . . . . . . . . . 18
  

       |
284 | 283 | neneqd 2631 |
. . . . . . . . . . . . . . . . 17
  


      |
285 | 284 | ex 436 |
. . . . . . . . . . . . . . . 16
           |
286 | 232, 285 | ralrimi 2790 |
. . . . . . . . . . . . . . 15
          |
287 | | ralnex 2836 |
. . . . . . . . . . . . . . 15
 
   
       |
288 | 286, 287 | sylib 200 |
. . . . . . . . . . . . . 14
          |
289 | 189 | nnzd 11046 |
. . . . . . . . . . . . . . 15
     |
290 | | odd2np1 14377 |
. . . . . . . . . . . . . . 15
 
        |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . 14
   
        |
292 | 288, 291 | mtbird 303 |
. . . . . . . . . . . . 13
  
  |
293 | 292 | notnotrd 117 |
. . . . . . . . . . . 12
     |
294 | 189 | nncnd 10632 |
. . . . . . . . . . . . 13
     |
295 | 294, 191 | npcand 9995 |
. . . . . . . . . . . 12
         |
296 | 293, 295 | breqtrrd 4432 |
. . . . . . . . . . 11
         |
297 | 193 | nn0zd 11045 |
. . . . . . . . . . . 12
       |
298 | | oddp1even 14379 |
. . . . . . . . . . . 12
   
 
       |
299 | 297, 298 | syl 17 |
. . . . . . . . . . 11
   
 
       |
300 | 296, 299 | mpbird 236 |
. . . . . . . . . 10
       |
301 | | oexpneg 14380 |
. . . . . . . . . 10
  

                   |
302 | 191, 226,
300, 301 | syl3anc 1269 |
. . . . . . . . 9
                   |
303 | | 1exp 12308 |
. . . . . . . . . . 11
           |
304 | 297, 303 | syl 17 |
. . . . . . . . . 10
           |
305 | 304 | negeqd 9874 |
. . . . . . . . 9
             |
306 | 302, 305 | eqtrd 2487 |
. . . . . . . 8
             |
307 | 306 | adantl 468 |
. . . . . . 7
 

            |
308 | 307 | oveq1d 6310 |
. . . . . 6
 

                            |
309 | 308 | oveq1d 6310 |
. . . . 5
 

                                            |
310 | 201 | mulm1d 10077 |
. . . . . . 7
 

                    |
311 | 310 | oveq1d 6310 |
. . . . . 6
 

                                    |
312 | 201 | negcld 9978 |
. . . . . . 7
 

           |
313 | 312, 201 | addcomd 9840 |
. . . . . 6
 

                                  |
314 | 201 | negidd 9981 |
. . . . . 6
 

                   |
315 | 311, 313,
314 | 3eqtrd 2491 |
. . . . 5
 

                     |
316 | 205, 309,
315 | 3eqtrd 2491 |
. . . 4
 

        |
317 | 117, 116 | eqeltrd 2531 |
. . . 4
 

      |
318 | 103 | a1i 11 |
. . . . . . 7
 

                           |
319 | | simpr 463 |
. . . . . . . . . . 11
               |
320 | 319 | oveq1d 6310 |
. . . . . . . . . 10
                   |
321 | 320 | oveq2d 6311 |
. . . . . . . . 9
                             |
322 | 319 | oveq2d 6311 |
. . . . . . . . . 10
                       |
323 | 322, 319 | oveq12d 6313 |
. . . . . . . . 9
                               |
324 | 321, 323 | oveq12d 6313 |
. . . . . . . 8
                                                     |
325 | 324, 323 | oveq12d 6313 |
. . . . . . 7
                                                                             |
326 | 148 | a1i 11 |
. . . . . . . . 9
 

  |
327 | | simpr 463 |
. . . . . . . . 9
 

  |
328 | 326, 327 | nn0mulcld 10937 |
. . . . . . . 8
 

    |
329 | | nn0p1nn 10916 |
. . . . . . . 8
  
      |
330 | 328, 329 | syl 17 |
. . . . . . 7
 

      |
331 | 176 | negcld 9978 |
. . . . . . . . . . 11

   |
332 | 175, 176 | pncand 9992 |
. . . . . . . . . . . 12

          |
333 | 148 | a1i 11 |
. . . . . . . . . . . . 13

  |
334 | 333, 172 | nn0mulcld 10937 |
. . . . . . . . . . . 12

    |
335 | 332, 334 | eqeltrd 2531 |
. . . . . . . . . . 11

        |
336 | 331, 335 | expcld 12423 |
. . . . . . . . . 10

             |
337 | 336 | adantl 468 |
. . . . . . . . 9
 

             |
338 | 14 | adantr 467 |
. . . . . . . . . . 11
 

  |
339 | 208 | a1i 11 |
. . . . . . . . . . . 12
 

  |
340 | 328, 339 | nn0addcld 10936 |
. . . . . . . . . . 11
 

      |
341 | 338, 340 | expcld 12423 |
. . . . . . . . . 10
 

          |
342 | | 2cnd 10689 |
. . . . . . . . . . . 12
 

  |
343 | 174 | adantl 468 |
. . . . . . . . . . . 12
 

  |
344 | 342, 343 | mulcld 9668 |
. . . . . . . . . . 11
 

    |
345 | | 1cnd 9664 |
. . . . . . . . . . 11
 

  |
346 | 344, 345 | addcld 9667 |
. . . . . . . . . 10
 

      |
347 | | 0red 9649 |
. . . . . . . . . . 11
 

  |
348 | 156 | a1i 11 |
. . . . . . . . . . . . 13
 

  |
349 | 158 | adantl 468 |
. . . . . . . . . . . . 13
 

  |
350 | 348, 349 | remulcld 9676 |
. . . . . . . . . . . 12
 

    |
351 | | 1red 9663 |
. . . . . . . . . . . 12
 

  |
352 | | 0le2 10707 |
. . . . . . . . . . . . . 14
 |
353 | 352 | a1i 11 |
. . . . . . . . . . . . 13
 

  |
354 | 327 | nn0ge0d 10935 |
. . . . . . . . . . . . 13
 

  |
355 | 348, 349,
353, 354 | mulge0d 10197 |
. . . . . . . . . . . 12
 

    |
356 | | 0lt1 10143 |
. . . . . . . . . . . . 13
 |
357 | 356 | a1i 11 |
. . . . . . . . . . . 12
 

  |
358 | 350, 351,
355, 357 | addgegt0d 10194 |
. . . . . . . . . . 11
 

      |
359 | 347, 358 | gtned 9775 |
. . . . . . . . . 10
 

      |
360 | 341, 346,
359 | divcld 10390 |
. . . . . . . . 9
 

                |
361 | 337, 360 | mulcld 9668 |
. . . . . . . 8
 

                             |
362 | 361, 360 | addcld 9667 |
. . . . . . 7
 

                                             |
363 | 318, 325,
330, 362 | fvmptd 5959 |
. . . . . 6
 

                                                     |
364 | 332 | adantl 468 |
. . . . . . . . . . . 12
 

          |
365 | 364 | oveq2d 6311 |
. . . . . . . . . . 11
 

                    |
366 | | nn0z 10967 |
. . . . . . . . . . . . 13

  |
367 | | m1expeven 12326 |
. . . . . . . . . . . . 13
          |
368 | 366, 367 | syl 17 |
. . . . . . . . . . . 12

         |
369 | 368 | adantl 468 |
. . . . . . . . . . 11
 

         |
370 | 365, 369 | eqtrd 2487 |
. . . . . . . . . 10
 

             |
371 | 370 | oveq1d 6310 |
. . . . . . . . 9
 

                                             |
372 | 360 | mulid2d 9666 |
. . . . . . . . 9
 

                                |
373 | 371, 372 | eqtrd 2487 |
. . . . . . . 8
 

                                           |
374 | 373 | oveq1d 6310 |
. . . . . . 7
 

                                                                           |
375 | 360 | 2timesd 10862 |
. . . . . . 7
 

                                                |
376 | 341, 346,
359 | divrec2d 10394 |
. . . . . . . 8
 

                                |
377 | 376 | oveq2d 6311 |
. . . . . . 7
 

                                    |
378 | 374, 375,
377 | 3eqtr2d 2493 |
. . . . . 6
 

                                                               |
379 | 363, 378 | eqtr2d 2488 |
. . . . 5
 

                            |
380 | | stirlinglem5.4 |
. . . . . . 7
                     |
381 | 380 | a1i 11 |
. . . . . 6
 

                      |
382 | | simpr 463 |
. . . . . . . . . . 11
       |
383 | 382 | oveq2d 6311 |
. . . . . . . . . 10
           |
384 | 383 | oveq1d 6310 |
. . . . . . . . 9
               |
385 | 384 | oveq2d 6311 |
. . . . . . . 8
                   |
386 | 384 | oveq2d 6311 |
. . . . . . . 8
                       |
387 | 385, 386 | oveq12d 6313 |
. . . . . . 7
                                       |
388 | 387 | oveq2d 6311 |
. . . . . 6
                                           |
389 | 346, 359 | reccld 10383 |
. . . . . . . 8
 

        |
390 | 389, 341 | mulcld 9668 |
. . . . . . 7
 

                  |
391 | 342, 390 | mulcld 9668 |
. . . . . 6
 

                    |
392 | 381, 388,
327, 391 | fvmptd 5959 |
. . . . 5
 

                        |
393 | 208 | a1i 11 |
. . . . . . . . 9

  |
394 | 334, 393 | nn0addcld 10936 |
. . . . . . . 8

      |
395 | 168, 171,
172, 394 | fvmptd 5959 |
. . . . . . 7

          |
396 | 395 | adantl 468 |
. . . . . 6
 

          |
397 | 396 | fveq2d 5874 |
. . . . 5
 

                  |
398 | 379, 392,
397 | 3eqtr4d 2497 |
. . . 4
 

              |
399 | 145, 1, 146, 2, 155, 188, 316, 317, 398 | isercoll2 13744 |
. . 3
                 
                    |
400 | 144, 399 | mpbird 236 |
. 2
                    |
401 | 51, 13 | resubcld 10054 |
. . . 4
     |
402 | 14 | subidd 9979 |
. . . . . 6
     |
403 | 402 | eqcomd 2459 |
. . . . 5
     |
404 | 13, 51, 13, 139 | ltsub1dd 10232 |
. . . . 5
  
    |
405 | 403, 404 | eqbrtrd 4426 |
. . . 4
     |
406 | 401, 405 | elrpd 11345 |
. . 3
     |
407 | 133, 406 | relogdivd 23587 |
. 2
                           |
408 | 400, 407 | breqtrrd 4432 |
1
                |