Step | Hyp | Ref
| Expression |
1 | | stirlinglem8.1 |
. . 3
|
2 | | stirlinglem8.7 |
. . . 4
|
3 | | nfmpt1 4747 |
. . . 4
|
4 | 2, 3 | nfcxfr 2762 |
. . 3
|
5 | | stirlinglem8.8 |
. . . 4
|
6 | | nfmpt1 4747 |
. . . 4
|
7 | 5, 6 | nfcxfr 2762 |
. . 3
|
8 | | stirlinglem8.6 |
. . . 4
|
9 | | nfmpt1 4747 |
. . . 4
|
10 | 8, 9 | nfcxfr 2762 |
. . 3
|
11 | | nnuz 11723 |
. . 3
|
12 | | 1zzd 11408 |
. . 3
|
13 | | stirlinglem8.2 |
. . . 4
|
14 | | stirlinglem8.5 |
. . . . 5
|
15 | | rrpsscn 39820 |
. . . . 5
|
16 | | fss 6056 |
. . . . 5
|
17 | 14, 15, 16 | sylancl 694 |
. . . 4
|
18 | | stirlinglem8.11 |
. . . 4
|
19 | | 4nn0 11311 |
. . . . 5
|
20 | 19 | a1i 11 |
. . . 4
|
21 | | nnex 11026 |
. . . . . . 7
|
22 | 21 | mptex 6486 |
. . . . . 6
|
23 | 2, 22 | eqeltri 2697 |
. . . . 5
|
24 | 23 | a1i 11 |
. . . 4
|
25 | | simpr 477 |
. . . . 5
|
26 | 14 | ffvelrnda 6359 |
. . . . . . 7
|
27 | 26 | rpcnd 11874 |
. . . . . 6
|
28 | 19 | a1i 11 |
. . . . . 6
|
29 | 27, 28 | expcld 13008 |
. . . . 5
|
30 | 2 | fvmpt2 6291 |
. . . . 5
|
31 | 25, 29, 30 | syl2anc 693 |
. . . 4
|
32 | 1, 13, 4, 11, 12, 17, 18, 20, 24, 31 | climexp 39837 |
. . 3
|
33 | 21 | mptex 6486 |
. . . . 5
|
34 | 8, 33 | eqeltri 2697 |
. . . 4
|
35 | 34 | a1i 11 |
. . 3
|
36 | | stirlinglem8.3 |
. . . 4
|
37 | 17 | adantr 481 |
. . . . . 6
|
38 | | 2nn 11185 |
. . . . . . . . 9
|
39 | 38 | a1i 11 |
. . . . . . . 8
|
40 | | id 22 |
. . . . . . . 8
|
41 | 39, 40 | nnmulcld 11068 |
. . . . . . 7
|
42 | 41 | adantl 482 |
. . . . . 6
|
43 | 37, 42 | ffvelrnd 6360 |
. . . . 5
|
44 | | stirlinglem8.4 |
. . . . 5
|
45 | 1, 43, 44 | fmptdf 6387 |
. . . 4
|
46 | | nfmpt1 4747 |
. . . . 5
|
47 | | fex 6490 |
. . . . . 6
|
48 | 17, 21, 47 | sylancl 694 |
. . . . 5
|
49 | | 1nn 11031 |
. . . . . . 7
|
50 | | 2cnd 11093 |
. . . . . . . 8
|
51 | | 1cnd 10056 |
. . . . . . . 8
|
52 | 50, 51 | mulcld 10060 |
. . . . . . 7
|
53 | | oveq2 6658 |
. . . . . . . 8
|
54 | | eqid 2622 |
. . . . . . . 8
|
55 | 53, 54 | fvmptg 6280 |
. . . . . . 7
|
56 | 49, 52, 55 | sylancr 695 |
. . . . . 6
|
57 | 38 | a1i 11 |
. . . . . . 7
|
58 | 49 | a1i 11 |
. . . . . . 7
|
59 | 57, 58 | nnmulcld 11068 |
. . . . . 6
|
60 | 56, 59 | eqeltrd 2701 |
. . . . 5
|
61 | | 1red 10055 |
. . . . . . . . 9
|
62 | 39 | nnred 11035 |
. . . . . . . . 9
|
63 | 41 | nnred 11035 |
. . . . . . . . 9
|
64 | 39 | nnge1d 11063 |
. . . . . . . . 9
|
65 | 61, 62, 63, 64 | leadd2dd 10642 |
. . . . . . . 8
|
66 | 54 | fvmpt2 6291 |
. . . . . . . . . 10
|
67 | 41, 66 | mpdan 702 |
. . . . . . . . 9
|
68 | 67 | oveq1d 6665 |
. . . . . . . 8
|
69 | | oveq2 6658 |
. . . . . . . . . . . 12
|
70 | 69 | cbvmptv 4750 |
. . . . . . . . . . 11
|
71 | 70 | a1i 11 |
. . . . . . . . . 10
|
72 | | simpr 477 |
. . . . . . . . . . 11
|
73 | 72 | oveq2d 6666 |
. . . . . . . . . 10
|
74 | | peano2nn 11032 |
. . . . . . . . . 10
|
75 | 39, 74 | nnmulcld 11068 |
. . . . . . . . . 10
|
76 | 71, 73, 74, 75 | fvmptd 6288 |
. . . . . . . . 9
|
77 | | 2cnd 11093 |
. . . . . . . . . 10
|
78 | | nncn 11028 |
. . . . . . . . . 10
|
79 | | 1cnd 10056 |
. . . . . . . . . 10
|
80 | 77, 78, 79 | adddid 10064 |
. . . . . . . . 9
|
81 | 77 | mulid1d 10057 |
. . . . . . . . . 10
|
82 | 81 | oveq2d 6666 |
. . . . . . . . 9
|
83 | 76, 80, 82 | 3eqtrd 2660 |
. . . . . . . 8
|
84 | 65, 68, 83 | 3brtr4d 4685 |
. . . . . . 7
|
85 | 41 | nnzd 11481 |
. . . . . . . . . 10
|
86 | 67, 85 | eqeltrd 2701 |
. . . . . . . . 9
|
87 | 86 | peano2zd 11485 |
. . . . . . . 8
|
88 | 75 | nnzd 11481 |
. . . . . . . . 9
|
89 | 76, 88 | eqeltrd 2701 |
. . . . . . . 8
|
90 | | eluz 11701 |
. . . . . . . 8
|
91 | 87, 89, 90 | syl2anc 693 |
. . . . . . 7
|
92 | 84, 91 | mpbird 247 |
. . . . . 6
|
93 | 92 | adantl 482 |
. . . . 5
|
94 | 21 | mptex 6486 |
. . . . . . 7
|
95 | 44, 94 | eqeltri 2697 |
. . . . . 6
|
96 | 95 | a1i 11 |
. . . . 5
|
97 | 44 | fvmpt2 6291 |
. . . . . . 7
|
98 | 25, 43, 97 | syl2anc 693 |
. . . . . 6
|
99 | 67 | adantl 482 |
. . . . . . . 8
|
100 | 99 | eqcomd 2628 |
. . . . . . 7
|
101 | 100 | fveq2d 6195 |
. . . . . 6
|
102 | 98, 101 | eqtrd 2656 |
. . . . 5
|
103 | 1, 13, 36, 46, 11, 12, 48, 27, 18, 60, 93, 96, 102 | climsuse 39840 |
. . . 4
|
104 | | 2nn0 11309 |
. . . . 5
|
105 | 104 | a1i 11 |
. . . 4
|
106 | 21 | mptex 6486 |
. . . . . 6
|
107 | 5, 106 | eqeltri 2697 |
. . . . 5
|
108 | 107 | a1i 11 |
. . . 4
|
109 | | stirlinglem8.9 |
. . . . . . 7
|
110 | 109 | rpcnd 11874 |
. . . . . 6
|
111 | 110 | sqcld 13006 |
. . . . 5
|
112 | 5 | fvmpt2 6291 |
. . . . 5
|
113 | 25, 111, 112 | syl2anc 693 |
. . . 4
|
114 | 1, 36, 7, 11, 12, 45, 103, 105, 108, 113 | climexp 39837 |
. . 3
|
115 | | stirlinglem8.10 |
. . . . 5
|
116 | 115 | rpcnd 11874 |
. . . 4
|
117 | 115 | rpne0d 11877 |
. . . 4
|
118 | | 2z 11409 |
. . . . 5
|
119 | 118 | a1i 11 |
. . . 4
|
120 | 116, 117,
119 | expne0d 13014 |
. . 3
|
121 | 1, 29, 2 | fmptdf 6387 |
. . . 4
|
122 | 121 | ffvelrnda 6359 |
. . 3
|
123 | 113, 111 | eqeltrd 2701 |
. . . 4
|
124 | 98 | oveq1d 6665 |
. . . . . . . . 9
|
125 | 113, 124 | eqtrd 2656 |
. . . . . . . 8
|
126 | 98, 109 | eqeltrrd 2702 |
. . . . . . . . 9
|
127 | 118 | a1i 11 |
. . . . . . . . 9
|
128 | 126, 127 | rpexpcld 13032 |
. . . . . . . 8
|
129 | 125, 128 | eqeltrd 2701 |
. . . . . . 7
|
130 | 129 | rpne0d 11877 |
. . . . . 6
|
131 | 130 | neneqd 2799 |
. . . . 5
|
132 | | 0cn 10032 |
. . . . . 6
|
133 | | elsn2g 4210 |
. . . . . 6
|
134 | 132, 133 | ax-mp 5 |
. . . . 5
|
135 | 131, 134 | sylnibr 319 |
. . . 4
|
136 | 123, 135 | eldifd 3585 |
. . 3
|
137 | 28 | nn0zd 11480 |
. . . . . . 7
|
138 | 26, 137 | rpexpcld 13032 |
. . . . . 6
|
139 | 109, 127 | rpexpcld 13032 |
. . . . . 6
|
140 | 138, 139 | rpdivcld 11889 |
. . . . 5
|
141 | 8 | fvmpt2 6291 |
. . . . 5
|
142 | 25, 140, 141 | syl2anc 693 |
. . . 4
|
143 | 2 | fvmpt2 6291 |
. . . . . 6
|
144 | 25, 138, 143 | syl2anc 693 |
. . . . 5
|
145 | 144, 113 | oveq12d 6668 |
. . . 4
|
146 | 142, 145 | eqtr4d 2659 |
. . 3
|
147 | 1, 4, 7, 10, 11, 12, 32, 35, 114, 120, 122, 136, 146 | climdivf 39844 |
. 2
|
148 | | 2cn 11091 |
. . . . . 6
|
149 | | 2p2e4 11144 |
. . . . . 6
|
150 | 148, 148,
149 | mvlladdi 10299 |
. . . . 5
|
151 | 150 | a1i 11 |
. . . 4
|
152 | 151 | oveq2d 6666 |
. . 3
|
153 | 20 | nn0zd 11480 |
. . . 4
|
154 | 116, 117,
119, 153 | expsubd 13019 |
. . 3
|
155 | 152, 154 | eqtrd 2656 |
. 2
|
156 | 147, 155 | breqtrrd 4681 |
1
|