Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . 6
|
2 | | stirlinglem13.2 |
. . . . . . 7
|
3 | 2 | elrnmpt 5372 |
. . . . . 6
|
4 | 1, 3 | ax-mp 5 |
. . . . 5
|
5 | | simpr 477 |
. . . . . . 7
|
6 | | stirlinglem13.1 |
. . . . . . . . . 10
|
7 | 6 | stirlinglem2 40292 |
. . . . . . . . 9
|
8 | 7 | relogcld 24369 |
. . . . . . . 8
|
9 | 8 | adantr 481 |
. . . . . . 7
|
10 | 5, 9 | eqeltrd 2701 |
. . . . . 6
|
11 | 10 | rexlimiva 3028 |
. . . . 5
|
12 | 4, 11 | sylbi 207 |
. . . 4
|
13 | 12 | ssriv 3607 |
. . 3
|
14 | | 1nn 11031 |
. . . . . 6
|
15 | 6 | stirlinglem2 40292 |
. . . . . . . 8
|
16 | | relogcl 24322 |
. . . . . . . 8
|
17 | 14, 15, 16 | mp2b 10 |
. . . . . . 7
|
18 | | nfcv 2764 |
. . . . . . . 8
|
19 | | nfcv 2764 |
. . . . . . . . 9
|
20 | | nfmpt1 4747 |
. . . . . . . . . . 11
|
21 | 6, 20 | nfcxfr 2762 |
. . . . . . . . . 10
|
22 | 21, 18 | nffv 6198 |
. . . . . . . . 9
|
23 | 19, 22 | nffv 6198 |
. . . . . . . 8
|
24 | | fveq2 6191 |
. . . . . . . . 9
|
25 | 24 | fveq2d 6195 |
. . . . . . . 8
|
26 | 18, 23, 25, 2 | fvmptf 6301 |
. . . . . . 7
|
27 | 14, 17, 26 | mp2an 708 |
. . . . . 6
|
28 | | fveq2 6191 |
. . . . . . . . 9
|
29 | 28 | fveq2d 6195 |
. . . . . . . 8
|
30 | 29 | eqeq2d 2632 |
. . . . . . 7
|
31 | 30 | rspcev 3309 |
. . . . . 6
|
32 | 14, 27, 31 | mp2an 708 |
. . . . 5
|
33 | 27, 17 | eqeltri 2697 |
. . . . . 6
|
34 | | nfcv 2764 |
. . . . . . . . 9
|
35 | | nfcv 2764 |
. . . . . . . . . . 11
|
36 | 21, 35 | nffv 6198 |
. . . . . . . . . 10
|
37 | 19, 36 | nffv 6198 |
. . . . . . . . 9
|
38 | | fveq2 6191 |
. . . . . . . . . 10
|
39 | 38 | fveq2d 6195 |
. . . . . . . . 9
|
40 | 34, 37, 39 | cbvmpt 4749 |
. . . . . . . 8
|
41 | 2, 40 | eqtri 2644 |
. . . . . . 7
|
42 | 41 | elrnmpt 5372 |
. . . . . 6
|
43 | 33, 42 | ax-mp 5 |
. . . . 5
|
44 | 32, 43 | mpbir 221 |
. . . 4
|
45 | 44 | ne0ii 3923 |
. . 3
|
46 | | 4re 11097 |
. . . . . . 7
|
47 | | 4ne0 11117 |
. . . . . . 7
|
48 | 46, 47 | rereccli 10790 |
. . . . . 6
|
49 | 33, 48 | resubcli 10343 |
. . . . 5
|
50 | | eqid 2622 |
. . . . . . 7
|
51 | 6, 2, 50 | stirlinglem12 40302 |
. . . . . 6
|
52 | 51 | rgen 2922 |
. . . . 5
|
53 | | breq1 4656 |
. . . . . . 7
|
54 | 53 | ralbidv 2986 |
. . . . . 6
|
55 | 54 | rspcev 3309 |
. . . . 5
|
56 | 49, 52, 55 | mp2an 708 |
. . . 4
|
57 | | simpr 477 |
. . . . . . . 8
|
58 | 8 | rgen 2922 |
. . . . . . . . 9
|
59 | 2 | fnmpt 6020 |
. . . . . . . . 9
|
60 | | fvelrnb 6243 |
. . . . . . . . 9
|
61 | 58, 59, 60 | mp2b 10 |
. . . . . . . 8
|
62 | 57, 61 | sylib 208 |
. . . . . . 7
|
63 | | nfra1 2941 |
. . . . . . . . 9
|
64 | | nfv 1843 |
. . . . . . . . 9
|
65 | 63, 64 | nfan 1828 |
. . . . . . . 8
|
66 | | nfv 1843 |
. . . . . . . 8
|
67 | | simp1l 1085 |
. . . . . . . . . . 11
|
68 | | simp2 1062 |
. . . . . . . . . . 11
|
69 | | rsp 2929 |
. . . . . . . . . . 11
|
70 | 67, 68, 69 | sylc 65 |
. . . . . . . . . 10
|
71 | | simp3 1063 |
. . . . . . . . . 10
|
72 | 70, 71 | breqtrd 4679 |
. . . . . . . . 9
|
73 | 72 | 3exp 1264 |
. . . . . . . 8
|
74 | 65, 66, 73 | rexlimd 3026 |
. . . . . . 7
|
75 | 62, 74 | mpd 15 |
. . . . . 6
|
76 | 75 | ralrimiva 2966 |
. . . . 5
|
77 | 76 | reximi 3011 |
. . . 4
|
78 | 56, 77 | ax-mp 5 |
. . 3
|
79 | | infrecl 11005 |
. . 3
inf |
80 | 13, 45, 78, 79 | mp3an 1424 |
. 2
inf |
81 | | nnuz 11723 |
. . . 4
|
82 | | 1zzd 11408 |
. . . 4
|
83 | 2, 8 | fmpti 6383 |
. . . . 5
|
84 | 83 | a1i 11 |
. . . 4
|
85 | | peano2nn 11032 |
. . . . . . . 8
|
86 | 6 | a1i 11 |
. . . . . . . . . . 11
|
87 | | simpr 477 |
. . . . . . . . . . . . 13
|
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . 12
|
89 | 87 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
90 | 89 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
91 | 87 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
92 | 91, 87 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
93 | 90, 92 | oveq12d 6668 |
. . . . . . . . . . . 12
|
94 | 88, 93 | oveq12d 6668 |
. . . . . . . . . . 11
|
95 | 85 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
96 | | faccl 13070 |
. . . . . . . . . . . . 13
|
97 | | nncn 11028 |
. . . . . . . . . . . . 13
|
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . 12
|
99 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
100 | | nncn 11028 |
. . . . . . . . . . . . . . . 16
|
101 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
102 | 100, 101 | addcld 10059 |
. . . . . . . . . . . . . . 15
|
103 | 99, 102 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
104 | 103 | sqrtcld 14176 |
. . . . . . . . . . . . 13
|
105 | | ere 14819 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | recni 10052 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . 15
|
108 | | 0re 10040 |
. . . . . . . . . . . . . . . . 17
|
109 | | epos 14935 |
. . . . . . . . . . . . . . . . 17
|
110 | 108, 109 | gtneii 10149 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . 15
|
112 | 102, 107,
111 | divcld 10801 |
. . . . . . . . . . . . . 14
|
113 | 112, 95 | expcld 13008 |
. . . . . . . . . . . . 13
|
114 | 104, 113 | mulcld 10060 |
. . . . . . . . . . . 12
|
115 | | 2rp 11837 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
117 | | nnre 11027 |
. . . . . . . . . . . . . . . . 17
|
118 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
119 | | 1red 10055 |
. . . . . . . . . . . . . . . . . 18
|
120 | | 0le1 10551 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
122 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . 18
|
123 | 118, 119,
117, 121, 122 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
|
124 | 117, 123 | ge0p1rpd 11902 |
. . . . . . . . . . . . . . . 16
|
125 | 116, 124 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
|
126 | 125 | sqrtgt0d 14151 |
. . . . . . . . . . . . . 14
|
127 | 126 | gt0ne0d 10592 |
. . . . . . . . . . . . 13
|
128 | 85 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
|
129 | 102, 107,
128, 111 | divne0d 10817 |
. . . . . . . . . . . . . 14
|
130 | | nnz 11399 |
. . . . . . . . . . . . . . 15
|
131 | 130 | peano2zd 11485 |
. . . . . . . . . . . . . 14
|
132 | 112, 129,
131 | expne0d 13014 |
. . . . . . . . . . . . 13
|
133 | 104, 113,
127, 132 | mulne0d 10679 |
. . . . . . . . . . . 12
|
134 | 98, 114, 133 | divcld 10801 |
. . . . . . . . . . 11
|
135 | 86, 94, 85, 134 | fvmptd 6288 |
. . . . . . . . . 10
|
136 | | nnrp 11842 |
. . . . . . . . . . . 12
|
137 | 95, 96, 136 | 3syl 18 |
. . . . . . . . . . 11
|
138 | 125 | rpsqrtcld 14150 |
. . . . . . . . . . . 12
|
139 | | epr 14936 |
. . . . . . . . . . . . . . 15
|
140 | 139 | a1i 11 |
. . . . . . . . . . . . . 14
|
141 | 124, 140 | rpdivcld 11889 |
. . . . . . . . . . . . 13
|
142 | 141, 131 | rpexpcld 13032 |
. . . . . . . . . . . 12
|
143 | 138, 142 | rpmulcld 11888 |
. . . . . . . . . . 11
|
144 | 137, 143 | rpdivcld 11889 |
. . . . . . . . . 10
|
145 | 135, 144 | eqeltrd 2701 |
. . . . . . . . 9
|
146 | 145 | relogcld 24369 |
. . . . . . . 8
|
147 | | nfcv 2764 |
. . . . . . . . 9
|
148 | 21, 147 | nffv 6198 |
. . . . . . . . . 10
|
149 | 19, 148 | nffv 6198 |
. . . . . . . . 9
|
150 | | fveq2 6191 |
. . . . . . . . . 10
|
151 | 150 | fveq2d 6195 |
. . . . . . . . 9
|
152 | 147, 149,
151, 2 | fvmptf 6301 |
. . . . . . . 8
|
153 | 85, 146, 152 | syl2anc 693 |
. . . . . . 7
|
154 | 153, 146 | eqeltrd 2701 |
. . . . . 6
|
155 | 83 | ffvelrni 6358 |
. . . . . 6
|
156 | | eqid 2622 |
. . . . . . 7
|
157 | 6, 2, 156 | stirlinglem11 40301 |
. . . . . 6
|
158 | 154, 155,
157 | ltled 10185 |
. . . . 5
|
159 | 158 | adantl 482 |
. . . 4
|
160 | 56 | a1i 11 |
. . . 4
|
161 | 81, 82, 84, 159, 160 | climinf 39838 |
. . 3
inf |
162 | 161 | trud 1493 |
. 2
inf |
163 | | breq2 4657 |
. . 3
inf
inf |
164 | 163 | rspcev 3309 |
. 2
inf
inf
|
165 | 80, 162, 164 | mp2an 708 |
1
|