Step | Hyp | Ref
| Expression |
1 | | stirlinglem8.1 |
. . 3
   |
2 | | stirlinglem8.7 |
. . . 4
           |
3 | | nfmpt1 4492 |
. . . 4
             |
4 | 2, 3 | nfcxfr 2590 |
. . 3
   |
5 | | stirlinglem8.8 |
. . . 4
           |
6 | | nfmpt1 4492 |
. . . 4
             |
7 | 5, 6 | nfcxfr 2590 |
. . 3
   |
8 | | stirlinglem8.6 |
. . . 4
                     |
9 | | nfmpt1 4492 |
. . . 4
                       |
10 | 8, 9 | nfcxfr 2590 |
. . 3
   |
11 | | nnuz 11194 |
. . 3
     |
12 | | 1zzd 10968 |
. . 3
   |
13 | | stirlinglem8.2 |
. . . 4
   |
14 | | stirlinglem8.5 |
. . . . 5
       |
15 | | rrpsscn 37666 |
. . . . 5
 |
16 | | fss 5737 |
. . . . 5
             |
17 | 14, 15, 16 | sylancl 668 |
. . . 4
       |
18 | | stirlinglem8.11 |
. . . 4
   |
19 | | 4nn0 10888 |
. . . . 5
 |
20 | 19 | a1i 11 |
. . . 4
   |
21 | | nnex 10615 |
. . . . . . 7
 |
22 | 21 | mptex 6136 |
. . . . . 6
           |
23 | 2, 22 | eqeltri 2525 |
. . . . 5
 |
24 | 23 | a1i 11 |
. . . 4
   |
25 | | simpr 463 |
. . . . 5
 

  |
26 | 14 | ffvelrnda 6022 |
. . . . . . 7
 

      |
27 | 26 | rpcnd 11343 |
. . . . . 6
 

      |
28 | 19 | a1i 11 |
. . . . . 6
 

  |
29 | 27, 28 | expcld 12416 |
. . . . 5
 

          |
30 | 2 | fvmpt2 5957 |
. . . . 5
                         |
31 | 25, 29, 30 | syl2anc 667 |
. . . 4
 

              |
32 | 1, 13, 4, 11, 12, 17, 18, 20, 24, 31 | climexp 37683 |
. . 3
       |
33 | 21 | mptex 6136 |
. . . . 5
                     |
34 | 8, 33 | eqeltri 2525 |
. . . 4
 |
35 | 34 | a1i 11 |
. . 3
   |
36 | | stirlinglem8.3 |
. . . 4
   |
37 | 17 | adantr 467 |
. . . . . 6
 

      |
38 | | 2nn 10767 |
. . . . . . . . 9
 |
39 | 38 | a1i 11 |
. . . . . . . 8
   |
40 | | id 22 |
. . . . . . . 8
   |
41 | 39, 40 | nnmulcld 10657 |
. . . . . . 7
     |
42 | 41 | adantl 468 |
. . . . . 6
 

    |
43 | 37, 42 | ffvelrnd 6023 |
. . . . 5
 

        |
44 | | stirlinglem8.4 |
. . . . 5
         |
45 | 1, 43, 44 | fmptdf 6048 |
. . . 4
       |
46 | | nfmpt1 4492 |
. . . . 5
       |
47 | | fex 6138 |
. . . . . 6
      
  |
48 | 17, 21, 47 | sylancl 668 |
. . . . 5
   |
49 | | 1nn 10620 |
. . . . . . 7
 |
50 | | 2cnd 10682 |
. . . . . . . 8
   |
51 | | 1cnd 9659 |
. . . . . . . 8
   |
52 | 50, 51 | mulcld 9663 |
. . . . . . 7
     |
53 | | oveq2 6298 |
. . . . . . . 8
       |
54 | | eqid 2451 |
. . . . . . . 8
         |
55 | 53, 54 | fvmptg 5946 |
. . . . . . 7
                 |
56 | 49, 52, 55 | sylancr 669 |
. . . . . 6
             |
57 | 38 | a1i 11 |
. . . . . . 7
   |
58 | 49 | a1i 11 |
. . . . . . 7
   |
59 | 57, 58 | nnmulcld 10657 |
. . . . . 6
     |
60 | 56, 59 | eqeltrd 2529 |
. . . . 5
           |
61 | | 1red 9658 |
. . . . . . . . 9
   |
62 | 39 | nnred 10624 |
. . . . . . . . 9
   |
63 | 41 | nnred 10624 |
. . . . . . . . 9
     |
64 | 39 | nnge1d 10652 |
. . . . . . . . 9
   |
65 | 61, 62, 63, 64 | leadd2dd 10228 |
. . . . . . . 8
           |
66 | 54 | fvmpt2 5957 |
. . . . . . . . . 10
                 |
67 | 41, 66 | mpdan 674 |
. . . . . . . . 9
             |
68 | 67 | oveq1d 6305 |
. . . . . . . 8
                 |
69 | | oveq2 6298 |
. . . . . . . . . . . 12
       |
70 | 69 | cbvmptv 4495 |
. . . . . . . . . . 11
         |
71 | 70 | a1i 11 |
. . . . . . . . . 10
           |
72 | | simpr 463 |
. . . . . . . . . . 11
 
       |
73 | 72 | oveq2d 6306 |
. . . . . . . . . 10
 
           |
74 | | peano2nn 10621 |
. . . . . . . . . 10
     |
75 | 39, 74 | nnmulcld 10657 |
. . . . . . . . . 10
       |
76 | 71, 73, 74, 75 | fvmptd 5954 |
. . . . . . . . 9
                 |
77 | | 2cnd 10682 |
. . . . . . . . . 10
   |
78 | | nncn 10617 |
. . . . . . . . . 10
   |
79 | | 1cnd 9659 |
. . . . . . . . . 10
   |
80 | 77, 78, 79 | adddid 9667 |
. . . . . . . . 9
             |
81 | 77 | mulid1d 9660 |
. . . . . . . . . 10
     |
82 | 81 | oveq2d 6306 |
. . . . . . . . 9
             |
83 | 76, 80, 82 | 3eqtrd 2489 |
. . . . . . . 8
                 |
84 | 65, 68, 83 | 3brtr4d 4433 |
. . . . . . 7
          
            |
85 | 41 | nnzd 11039 |
. . . . . . . . . 10
     |
86 | 67, 85 | eqeltrd 2529 |
. . . . . . . . 9
           |
87 | 86 | peano2zd 11043 |
. . . . . . . 8
             |
88 | 75 | nnzd 11039 |
. . . . . . . . 9
       |
89 | 76, 88 | eqeltrd 2529 |
. . . . . . . 8
             |
90 | | eluz 11172 |
. . . . . . . 8
                   
                           
                       |
91 | 87, 89, 90 | syl2anc 667 |
. . . . . . 7
         
                                       |
92 | 84, 91 | mpbird 236 |
. . . . . 6
                           |
93 | 92 | adantl 468 |
. . . . 5
 

                          |
94 | 21 | mptex 6136 |
. . . . . . 7
         |
95 | 44, 94 | eqeltri 2525 |
. . . . . 6
 |
96 | 95 | a1i 11 |
. . . . 5
   |
97 | 44 | fvmpt2 5957 |
. . . . . . 7
                     |
98 | 25, 43, 97 | syl2anc 667 |
. . . . . 6
 

            |
99 | 67 | adantl 468 |
. . . . . . . 8
 

            |
100 | 99 | eqcomd 2457 |
. . . . . . 7
 

            |
101 | 100 | fveq2d 5869 |
. . . . . 6
 

                    |
102 | 98, 101 | eqtrd 2485 |
. . . . 5
 

                  |
103 | 1, 13, 36, 46, 11, 12, 48, 27, 18, 60, 93, 96, 102 | climsuse 37687 |
. . . 4
   |
104 | | 2nn0 10886 |
. . . . 5
 |
105 | 104 | a1i 11 |
. . . 4
   |
106 | 21 | mptex 6136 |
. . . . . 6
           |
107 | 5, 106 | eqeltri 2525 |
. . . . 5
 |
108 | 107 | a1i 11 |
. . . 4
   |
109 | | stirlinglem8.9 |
. . . . . . 7
 

      |
110 | 109 | rpcnd 11343 |
. . . . . 6
 

      |
111 | 110 | sqcld 12414 |
. . . . 5
 

          |
112 | 5 | fvmpt2 5957 |
. . . . 5
                         |
113 | 25, 111, 112 | syl2anc 667 |
. . . 4
 

              |
114 | 1, 36, 7, 11, 12, 45, 103, 105, 108, 113 | climexp 37683 |
. . 3
       |
115 | | stirlinglem8.10 |
. . . . 5
   |
116 | 115 | rpcnd 11343 |
. . . 4
   |
117 | 115 | rpne0d 11346 |
. . . 4
   |
118 | | 2z 10969 |
. . . . 5
 |
119 | 118 | a1i 11 |
. . . 4
   |
120 | 116, 117,
119 | expne0d 12422 |
. . 3
       |
121 | 1, 29, 2 | fmptdf 6048 |
. . . 4
       |
122 | 121 | ffvelrnda 6022 |
. . 3
 

      |
123 | 113, 111 | eqeltrd 2529 |
. . . 4
 

      |
124 | 98 | oveq1d 6305 |
. . . . . . . . 9
 

                    |
125 | 113, 124 | eqtrd 2485 |
. . . . . . . 8
 

                |
126 | 98, 109 | eqeltrrd 2530 |
. . . . . . . . 9
 

        |
127 | 118 | a1i 11 |
. . . . . . . . 9
 

  |
128 | 126, 127 | rpexpcld 12439 |
. . . . . . . 8
 

            |
129 | 125, 128 | eqeltrd 2529 |
. . . . . . 7
 

      |
130 | 129 | rpne0d 11346 |
. . . . . 6
 

      |
131 | 130 | neneqd 2629 |
. . . . 5
 

      |
132 | | 0cn 9635 |
. . . . . 6
 |
133 | | elsnc2g 3998 |
. . . . . 6
               |
134 | 132, 133 | ax-mp 5 |
. . . . 5
             |
135 | 131, 134 | sylnibr 307 |
. . . 4
 

        |
136 | 123, 135 | eldifd 3415 |
. . 3
 

          |
137 | 28 | nn0zd 11038 |
. . . . . . 7
 

  |
138 | 26, 137 | rpexpcld 12439 |
. . . . . 6
 

          |
139 | 109, 127 | rpexpcld 12439 |
. . . . . 6
 

          |
140 | 138, 139 | rpdivcld 11358 |
. . . . 5
 

                    |
141 | 8 | fvmpt2 5957 |
. . . . 5
                                             |
142 | 25, 140, 141 | syl2anc 667 |
. . . 4
 

                        |
143 | 2 | fvmpt2 5957 |
. . . . . 6
                         |
144 | 25, 138, 143 | syl2anc 667 |
. . . . 5
 

              |
145 | 144, 113 | oveq12d 6308 |
. . . 4
 

                              |
146 | 142, 145 | eqtr4d 2488 |
. . 3
 

                |
147 | 1, 4, 7, 10, 11, 12, 32, 35, 114, 120, 122, 136, 146 | climdivf 37692 |
. 2
             |
148 | | 2cn 10680 |
. . . . . 6
 |
149 | | 2p2e4 10727 |
. . . . . 6
   |
150 | 148, 148,
149 | mvlladdi 9892 |
. . . . 5
   |
151 | 150 | a1i 11 |
. . . 4
     |
152 | 151 | oveq2d 6306 |
. . 3
             |
153 | 20 | nn0zd 11038 |
. . . 4
   |
154 | 116, 117,
119, 153 | expsubd 12427 |
. . 3
                   |
155 | 152, 154 | eqtrd 2485 |
. 2
                 |
156 | 147, 155 | breqtrrd 4429 |
1
       |