Step | Hyp | Ref
| Expression |
1 | | nnnn0 12425 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ0) |
2 | | faccl 14189 |
. . . . 5
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
3 | | nnrp 12931 |
. . . . 5
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ+) |
4 | 1, 2, 3 | 3syl 18 |
. . . 4
โข (๐ โ โ โ
(!โ๐) โ
โ+) |
5 | | 2rp 12925 |
. . . . . . . 8
โข 2 โ
โ+ |
6 | 5 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
โ+) |
7 | | nnrp 12931 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ+) |
8 | 6, 7 | rpmulcld 12978 |
. . . . . 6
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
9 | 8 | rpsqrtcld 15302 |
. . . . 5
โข (๐ โ โ โ
(โโ(2 ยท ๐)) โ
โ+) |
10 | | epr 16095 |
. . . . . . . 8
โข e โ
โ+ |
11 | 10 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ e โ
โ+) |
12 | 7, 11 | rpdivcld 12979 |
. . . . . 6
โข (๐ โ โ โ (๐ / e) โ
โ+) |
13 | | nnz 12525 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
14 | 12, 13 | rpexpcld 14156 |
. . . . 5
โข (๐ โ โ โ ((๐ / e)โ๐) โ
โ+) |
15 | 9, 14 | rpmulcld 12978 |
. . . 4
โข (๐ โ โ โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ
โ+) |
16 | 4, 15 | rpdivcld 12979 |
. . 3
โข (๐ โ โ โ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ
โ+) |
17 | | stirlinglem2.1 |
. . . . . 6
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
18 | | fveq2 6843 |
. . . . . . . 8
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
19 | | oveq2 7366 |
. . . . . . . . . 10
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
20 | 19 | fveq2d 6847 |
. . . . . . . . 9
โข (๐ = ๐ โ (โโ(2 ยท ๐)) = (โโ(2 ยท
๐))) |
21 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ / e) = (๐ / e)) |
22 | | id 22 |
. . . . . . . . . 10
โข (๐ = ๐ โ ๐ = ๐) |
23 | 21, 22 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ / e)โ๐) = ((๐ / e)โ๐)) |
24 | 20, 23 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
25 | 18, 24 | oveq12d 7376 |
. . . . . . 7
โข (๐ = ๐ โ ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
26 | 25 | cbvmptv 5219 |
. . . . . 6
โข (๐ โ โ โฆ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
27 | 17, 26 | eqtri 2761 |
. . . . 5
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
28 | 27 | a1i 11 |
. . . 4
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))))) |
29 | | simpr 486 |
. . . . . 6
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ๐ = ๐) |
30 | 29 | fveq2d 6847 |
. . . . 5
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (!โ๐) = (!โ๐)) |
31 | 29 | oveq2d 7374 |
. . . . . . 7
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (2 ยท ๐) = (2 ยท ๐)) |
32 | 31 | fveq2d 6847 |
. . . . . 6
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (โโ(2 ยท ๐)) = (โโ(2 ยท
๐))) |
33 | 29 | oveq1d 7373 |
. . . . . . 7
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (๐ / e) = (๐ / e)) |
34 | 33, 29 | oveq12d 7376 |
. . . . . 6
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ((๐ / e)โ๐) = ((๐ / e)โ๐)) |
35 | 32, 34 | oveq12d 7376 |
. . . . 5
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
36 | 30, 35 | oveq12d 7376 |
. . . 4
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
37 | | simpl 484 |
. . . 4
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ โ
โ) |
38 | | simpr 486 |
. . . 4
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ
โ+) |
39 | 28, 36, 37, 38 | fvmptd 6956 |
. . 3
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(๐ดโ๐) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
40 | 16, 39 | mpdan 686 |
. 2
โข (๐ โ โ โ (๐ดโ๐) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
41 | 40, 16 | eqeltrd 2834 |
1
โข (๐ โ โ โ (๐ดโ๐) โ
โ+) |