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 45711 |
. 2
β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯)))) |
10 | 1, 2 | dvdmsscn 45383 |
. . 3
β’ (π β π β β) |
11 | 8, 6 | etransclem16 45697 |
. . 3
β’ (π β (πΆβπ) β Fin) |
12 | 10 | adantr 479 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β π β β) |
13 | 6 | faccld 14270 |
. . . . . . . 8
β’ (π β (!βπ) β β) |
14 | 13 | nncnd 12253 |
. . . . . . 7
β’ (π β (!βπ) β β) |
15 | 14 | adantr 479 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β (!βπ) β β) |
16 | | fzfid 13965 |
. . . . . . 7
β’ ((π β§ π β (πΆβπ)) β (0...π) β Fin) |
17 | | fzssnn0 44758 |
. . . . . . . . . 10
β’
(0...π) β
β0 |
18 | | ssrab2 4070 |
. . . . . . . . . . . . 13
β’ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β ((0...π) βm (0...π)) |
19 | | simpr 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (πΆβπ)) β π β (πΆβπ)) |
20 | 8, 6 | etransclem12 45693 |
. . . . . . . . . . . . . . 15
β’ (π β (πΆβπ) = {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
21 | 20 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (πΆβπ)) β (πΆβπ) = {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
22 | 19, 21 | eleqtrd 2827 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (πΆβπ)) β π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
23 | 18, 22 | sselid 3971 |
. . . . . . . . . . . 12
β’ ((π β§ π β (πΆβπ)) β π β ((0...π) βm (0...π))) |
24 | | elmapi 8861 |
. . . . . . . . . . . 12
β’ (π β ((0...π) βm (0...π)) β π:(0...π)βΆ(0...π)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (πΆβπ)) β π:(0...π)βΆ(0...π)) |
26 | 25 | ffvelcdmda 7087 |
. . . . . . . . . 10
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (πβπ) β (0...π)) |
27 | 17, 26 | sselid 3971 |
. . . . . . . . 9
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (πβπ) β
β0) |
28 | 27 | faccld 14270 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (!β(πβπ)) β β) |
29 | 28 | nncnd 12253 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (!β(πβπ)) β β) |
30 | 16, 29 | fprodcl 15923 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β βπ β (0...π)(!β(πβπ)) β β) |
31 | 28 | nnne0d 12287 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (!β(πβπ)) β 0) |
32 | 16, 29, 31 | fprodn0 15950 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β βπ β (0...π)(!β(πβπ)) β 0) |
33 | 15, 30, 32 | divcld 12015 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β ((!βπ) / βπ β (0...π)(!β(πβπ))) β β) |
34 | | ssid 3996 |
. . . . . 6
β’ β
β β |
35 | 34 | a1i 11 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β β β
β) |
36 | 12, 33, 35 | constcncfg 45319 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β (π₯ β π β¦ ((!βπ) / βπ β (0...π)(!β(πβπ)))) β (πβcnββ)) |
37 | 1 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β {β, β}) |
38 | 2 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β
((TopOpenββfld) βΎt π)) |
39 | 3 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β β) |
40 | | etransclem5 45686 |
. . . . . . . . 9
β’ (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) = (π β (0...π) β¦ (π¦ β π β¦ ((π¦ β π)βif(π = 0, (π β 1), π)))) |
41 | 7, 40 | eqtri 2753 |
. . . . . . . 8
β’ π» = (π β (0...π) β¦ (π¦ β π β¦ ((π¦ β π)βif(π = 0, (π β 1), π)))) |
42 | | simpr 483 |
. . . . . . . 8
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β π β (0...π)) |
43 | 37, 38, 39, 41, 42, 27 | etransclem20 45701 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ) |
44 | 43 | 3adant2 1128 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π₯ β π β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ) |
45 | | simp2 1134 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π₯ β π β§ π β (0...π)) β π₯ β π) |
46 | 44, 45 | ffvelcdmd 7088 |
. . . . 5
β’ (((π β§ π β (πΆβπ)) β§ π₯ β π β§ π β (0...π)) β (((π Dπ (π»βπ))β(πβπ))βπ₯) β β) |
47 | 43 | feqmptd 6960 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)) = (π₯ β π β¦ (((π Dπ (π»βπ))β(πβπ))βπ₯))) |
48 | 37, 38, 39, 41, 42, 27 | etransclem22 45703 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β ((π Dπ (π»βπ))β(πβπ)) β (πβcnββ)) |
49 | 47, 48 | eqeltrrd 2826 |
. . . . 5
β’ (((π β§ π β (πΆβπ)) β§ π β (0...π)) β (π₯ β π β¦ (((π Dπ (π»βπ))β(πβπ))βπ₯)) β (πβcnββ)) |
50 | 12, 16, 46, 49 | fprodcncf 45347 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β (π₯ β π β¦ βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯)) β (πβcnββ)) |
51 | 36, 50 | mulcncf 25387 |
. . 3
β’ ((π β§ π β (πΆβπ)) β (π₯ β π β¦ (((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯))) β (πβcnββ)) |
52 | 10, 11, 51 | fsumcncf 45325 |
. 2
β’ (π β (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯))) β (πβcnββ)) |
53 | 9, 52 | eqeltrd 2825 |
1
β’ (π β ((π Dπ πΉ)βπ) β (πβcnββ)) |