Step | Hyp | Ref
| Expression |
1 | | etransclem34.s |
. . 3
β’ (π β π β {β, β}) |
2 | | etransclem34.a |
. . 3
β’ (π β π β
((TopOpenββfld) βΎt π)) |
3 | | etransclem34.p |
. . 3
β’ (π β π β β) |
4 | | etransclem34.m |
. . 3
β’ (π β π β
β0) |
5 | | etransclem34.f |
. . 3
β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
6 | | etransclem34.n |
. . 3
β’ (π β π β
β0) |
7 | | etransclem34.h |
. . 3
β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
8 | | etransclem34.c |
. . 3
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | etransclem30 45565 |
. 2
β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯)))) |
10 | 1, 2 | dvdmsscn 45237 |
. . 3
β’ (π β π β β) |
11 | 8, 6 | etransclem16 45551 |
. . 3
β’ (π β (πΆβπ) β Fin) |
12 | 10 | adantr 480 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β π β β) |
13 | 6 | faccld 14261 |
. . . . . . . 8
β’ (π β (!βπ) β β) |
14 | 13 | nncnd 12244 |
. . . . . . 7
β’ (π β (!βπ) β β) |
15 | 14 | adantr 480 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β (!βπ) β β) |
16 | | fzfid 13956 |
. . . . . . 7
β’ ((π β§ π β (πΆβπ)) β (0...π) β Fin) |
17 | | fzssnn0 44612 |
. . . . . . . . . 10
β’
(0...π) β
β0 |
18 | | ssrab2 4073 |
. . . . . . . . . . . . 13
β’ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β ((0...π) βm (0...π)) |
19 | | simpr 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (πΆβπ)) β π β (πΆβπ)) |
20 | 8, 6 | etransclem12 45547 |
. . . . . . . . . . . . . . 15
β’ (π β (πΆβπ) = {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (πΆβπ)) β (πΆβπ) = {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
22 | 19, 21 | eleqtrd 2830 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (πΆβπ)) β π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
23 | 18, 22 | sselid 3976 |
. . . . . . . . . . . 12
β’ ((π β§ π β (πΆβπ)) β π β ((0...π) βm (0...π))) |
24 | | elmapi 8857 |
. . . . . . . . . . . 12
β’ (π β ((0...π) βm (0...π)) β π:(0...π)βΆ(0...π)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (πΆβπ)) β π:(0...π)βΆ(0...π)) |
26 | 25 | ffvelcdmda 7088 |
. . . . . . . . . 10
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (πβπ) β (0...π)) |
27 | 17, 26 | sselid 3976 |
. . . . . . . . 9
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (πβπ) β
β0) |
28 | 27 | faccld 14261 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (!β(πβπ)) β β) |
29 | 28 | nncnd 12244 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (!β(πβπ)) β β) |
30 | 16, 29 | fprodcl 15914 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β βπ β (0...π)(!β(πβπ)) β β) |
31 | 28 | nnne0d 12278 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (!β(πβπ)) β 0) |
32 | 16, 29, 31 | fprodn0 15941 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β βπ β (0...π)(!β(πβπ)) β 0) |
33 | 15, 30, 32 | divcld 12006 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β ((!βπ) / βπ β (0...π)(!β(πβπ))) β β) |
34 | | ssid 4000 |
. . . . . 6
β’ β
β β |
35 | 34 | a1i 11 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β β β
β) |
36 | 12, 33, 35 | constcncfg 45173 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β (π₯ β π β¦ ((!βπ) / βπ β (0...π)(!β(πβπ)))) β (πβcnββ)) |
37 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β {β, β}) |
38 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β
((TopOpenββfld) βΎt π)) |
39 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β β) |
40 | | etransclem5 45540 |
. . . . . . . . 9
β’ (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) = (π β (0...π) β¦ (π¦ β π β¦ ((π¦ β π)βif(π = 0, (π β 1), π)))) |
41 | 7, 40 | eqtri 2755 |
. . . . . . . 8
β’ π» = (π β (0...π) β¦ (π¦ β π β¦ ((π¦ β π)βif(π = 0, (π β 1), π)))) |
42 | | simpr 484 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β (0...π)) |
43 | 37, 38, 39, 41, 42, 27 | etransclem20 45555 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ) |
44 | 43 | 3adant2 1129 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π₯ β π β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ) |
45 | | simp2 1135 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π₯ β π β§ π β (0...π)) β π₯ β π) |
46 | 44, 45 | ffvelcdmd 7089 |
. . . . 5
β’ (((π β§ π β (πΆβπ)) β§ π₯ β π β§ π β (0...π)) β (((π Dπ (π»βπ))β(πβπ))βπ₯) β β) |
47 | 43 | feqmptd 6961 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)) = (π₯ β π β¦ (((π Dπ (π»βπ))β(πβπ))βπ₯))) |
48 | 37, 38, 39, 41, 42, 27 | etransclem22 45557 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)) β (πβcnββ)) |
49 | 47, 48 | eqeltrrd 2829 |
. . . . 5
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (π₯ β π β¦ (((π Dπ (π»βπ))β(πβπ))βπ₯)) β (πβcnββ)) |
50 | 12, 16, 46, 49 | fprodcncf 45201 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β (π₯ β π β¦ βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯)) β (πβcnββ)) |
51 | 36, 50 | mulcncf 25348 |
. . 3
β’ ((π β§ π β (πΆβπ)) β (π₯ β π β¦ (((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯))) β (πβcnββ)) |
52 | 10, 11, 51 | fsumcncf 45179 |
. 2
β’ (π β (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯))) β (πβcnββ)) |
53 | 9, 52 | eqeltrd 2828 |
1
β’ (π β ((π Dπ πΉ)βπ) β (πβcnββ)) |