Step | Hyp | Ref
| Expression |
1 | | etransclem37.c |
. . . 4
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
2 | | etransclem37.n |
. . . 4
β’ (π β π β
β0) |
3 | 1, 2 | etransclem16 44565 |
. . 3
β’ (π β (πΆβπ) β Fin) |
4 | | etransclem37.p |
. . . . . 6
β’ (π β π β β) |
5 | | nnm1nn0 12461 |
. . . . . 6
β’ (π β β β (π β 1) β
β0) |
6 | 4, 5 | syl 17 |
. . . . 5
β’ (π β (π β 1) β
β0) |
7 | 6 | faccld 14191 |
. . . 4
β’ (π β (!β(π β 1)) β
β) |
8 | 7 | nnzd 12533 |
. . 3
β’ (π β (!β(π β 1)) β
β€) |
9 | 1, 2 | etransclem12 44561 |
. . . . . . . . . . . 12
β’ (π β (πΆβπ) = {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
10 | 9 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π β (π β (πΆβπ) β π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π})) |
11 | 10 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ π β (πΆβπ)) β π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
12 | | rabid 3430 |
. . . . . . . . . . . 12
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β (π β ((0...π) βm (0...π)) β§ Ξ£π β (0...π)(πβπ) = π)) |
13 | 12 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β (π β ((0...π) βm (0...π)) β§ Ξ£π β (0...π)(πβπ) = π)) |
14 | 13 | simprd 497 |
. . . . . . . . . 10
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β Ξ£π β (0...π)(πβπ) = π) |
15 | 11, 14 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (πΆβπ)) β Ξ£π β (0...π)(πβπ) = π) |
16 | 15 | eqcomd 2743 |
. . . . . . . 8
β’ ((π β§ π β (πΆβπ)) β π = Ξ£π β (0...π)(πβπ)) |
17 | 16 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π β (πΆβπ)) β (!βπ) = (!βΞ£π β (0...π)(πβπ))) |
18 | 17 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β ((!βπ) / βπ β (0...π)(!β(πβπ))) = ((!βΞ£π β (0...π)(πβπ)) / βπ β (0...π)(!β(πβπ)))) |
19 | | nfcv 2908 |
. . . . . . 7
β’
β²ππ |
20 | | fzfid 13885 |
. . . . . . 7
β’ ((π β§ π β (πΆβπ)) β (0...π) β Fin) |
21 | | nn0ex 12426 |
. . . . . . . . . . 11
β’
β0 β V |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β β0 β
V) |
23 | | fzssnn0 43625 |
. . . . . . . . . 10
β’
(0...π) β
β0 |
24 | | mapss 8834 |
. . . . . . . . . 10
β’
((β0 β V β§ (0...π) β β0) β
((0...π) βm
(0...π)) β
(β0 βm (0...π))) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . . 9
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β ((0...π) βm (0...π)) β (β0
βm (0...π))) |
26 | 13 | simpld 496 |
. . . . . . . . 9
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β π β ((0...π) βm (0...π))) |
27 | 25, 26 | sseldd 3950 |
. . . . . . . 8
β’ (π β {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π} β π β (β0
βm (0...π))) |
28 | 11, 27 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (πΆβπ)) β π β (β0
βm (0...π))) |
29 | 19, 20, 28 | mccl 43913 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β ((!βΞ£π β (0...π)(πβπ)) / βπ β (0...π)(!β(πβπ))) β β) |
30 | 18, 29 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β ((!βπ) / βπ β (0...π)(!β(πβπ))) β β) |
31 | 30 | nnzd 12533 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β ((!βπ) / βπ β (0...π)(!β(πβπ))) β β€) |
32 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β π β β) |
33 | | etransclem37.m |
. . . . . . 7
β’ (π β π β
β0) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β π β
β0) |
35 | | elmapi 8794 |
. . . . . . 7
β’ (π β ((0...π) βm (0...π)) β π:(0...π)βΆ(0...π)) |
36 | 11, 26, 35 | 3syl 18 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β π:(0...π)βΆ(0...π)) |
37 | | etransclem37.9 |
. . . . . . . 8
β’ (π β π½ β (0...π)) |
38 | 37 | elfzelzd 13449 |
. . . . . . 7
β’ (π β π½ β β€) |
39 | 38 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β π½ β β€) |
40 | 32, 34, 36, 39 | etransclem10 44559 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) β
β€) |
41 | | fzfid 13885 |
. . . . . 6
β’ ((π β§ π β (πΆβπ)) β (1...π) β Fin) |
42 | 32 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (1...π)) β π β β) |
43 | 36 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (1...π)) β π:(0...π)βΆ(0...π)) |
44 | | 0z 12517 |
. . . . . . . . . . 11
β’ 0 β
β€ |
45 | | fzp1ss 13499 |
. . . . . . . . . . 11
β’ (0 β
β€ β ((0 + 1)...π) β (0...π)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . 10
β’ ((0 +
1)...π) β (0...π) |
47 | 46 | sseli 3945 |
. . . . . . . . 9
β’ (π β ((0 + 1)...π) β π β (0...π)) |
48 | | 1e0p1 12667 |
. . . . . . . . . 10
β’ 1 = (0 +
1) |
49 | 48 | oveq1i 7372 |
. . . . . . . . 9
β’
(1...π) = ((0 +
1)...π) |
50 | 47, 49 | eleq2s 2856 |
. . . . . . . 8
β’ (π β (1...π) β π β (0...π)) |
51 | 50 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (1...π)) β π β (0...π)) |
52 | 39 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (πΆβπ)) β§ π β (1...π)) β π½ β β€) |
53 | 42, 43, 51, 52 | etransclem3 44552 |
. . . . . 6
β’ (((π β§ π β (πΆβπ)) β§ π β (1...π)) β if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))) β β€) |
54 | 41, 53 | fprodzcl 15844 |
. . . . 5
β’ ((π β§ π β (πΆβπ)) β βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))) β β€) |
55 | 40, 54 | zmulcld 12620 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))) β β€) |
56 | 31, 55 | zmulcld 12620 |
. . 3
β’ ((π β§ π β (πΆβπ)) β (((!βπ) / βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))))) β β€) |
57 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β π β
β0) |
58 | | etransclem11 44560 |
. . . . 5
β’ (π β β0
β¦ {π β
((0...π) βm
(0...π)) β£
Ξ£π β (0...π)(πβπ) = π}) = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
59 | 1, 58 | eqtri 2765 |
. . . 4
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
60 | | simpr 486 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β π β (πΆβπ)) |
61 | 37 | adantr 482 |
. . . 4
β’ ((π β§ π β (πΆβπ)) β π½ β (0...π)) |
62 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
63 | 62 | fveq2d 6851 |
. . . . . . 7
β’ (π = π β (!β(πβπ)) = (!β(πβπ))) |
64 | 63 | cbvprodv 15806 |
. . . . . 6
β’
βπ β
(0...π)(!β(πβπ)) = βπ β (0...π)(!β(πβπ)) |
65 | 64 | oveq2i 7373 |
. . . . 5
β’
((!βπ) /
βπ β (0...π)(!β(πβπ))) = ((!βπ) / βπ β (0...π)(!β(πβπ))) |
66 | 62 | breq2d 5122 |
. . . . . . . 8
β’ (π = π β (π < (πβπ) β π < (πβπ))) |
67 | 62 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (π β (πβπ)) = (π β (πβπ))) |
68 | 67 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β (!β(π β (πβπ))) = (!β(π β (πβπ)))) |
69 | 68 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π β ((!βπ) / (!β(π β (πβπ)))) = ((!βπ) / (!β(π β (πβπ))))) |
70 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (π½ β π) = (π½ β π)) |
71 | 70, 67 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β ((π½ β π)β(π β (πβπ))) = ((π½ β π)β(π β (πβπ)))) |
72 | 69, 71 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π β (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))) = (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))) |
73 | 66, 72 | ifbieq2d 4517 |
. . . . . . 7
β’ (π = π β if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))) = if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))) |
74 | 73 | cbvprodv 15806 |
. . . . . 6
β’
βπ β
(1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))) = βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))) |
75 | 74 | oveq2i 7373 |
. . . . 5
β’
(if((π β 1)
< (πβ0), 0,
(((!β(π β 1)) /
(!β((π β 1)
β (πβ0))))
Β· (π½β((π β 1) β (πβ0))))) Β·
βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))) = (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))) |
76 | 65, 75 | oveq12i 7374 |
. . . 4
β’
(((!βπ) /
βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))))) = (((!βπ) / βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ))))))) |
77 | 32, 34, 57, 59, 60, 61, 76 | etransclem28 44577 |
. . 3
β’ ((π β§ π β (πΆβπ)) β (!β(π β 1)) β₯ (((!βπ) / βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))))) |
78 | 3, 8, 56, 77 | fsumdvds 16197 |
. 2
β’ (π β (!β(π β 1)) β₯
Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))))) |
79 | | etransclem37.s |
. . 3
β’ (π β π β {β, β}) |
80 | | etransclem37.x |
. . 3
β’ (π β π β
((TopOpenββfld) βΎt π)) |
81 | | etransclem37.f |
. . 3
β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
82 | | etransclem37.h |
. . 3
β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
83 | | etransclem37.j |
. . 3
β’ (π β π½ β π) |
84 | 79, 80, 4, 33, 81, 2, 82, 1, 83 | etransclem31 44580 |
. 2
β’ (π β (((π Dπ πΉ)βπ)βπ½) = Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (π½β((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π½ β π)β(π β (πβπ)))))))) |
85 | 78, 84 | breqtrrd 5138 |
1
β’ (π β (!β(π β 1)) β₯ (((π Dπ πΉ)βπ)βπ½)) |