Step | Hyp | Ref
| Expression |
1 | | etransclem47.k |
. . . . 5
β’ πΎ = (πΏ / (!β(π β 1))) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β πΎ = (πΏ / (!β(π β 1)))) |
3 | | etransclem47.q |
. . . . 5
β’ (π β π β ((Polyββ€) β
{0π})) |
4 | | etransclem47.qe0 |
. . . . 5
β’ (π β (πβe) = 0) |
5 | | etransclem47.a |
. . . . 5
β’ π΄ = (coeffβπ) |
6 | | etransclem47.m |
. . . . 5
β’ π = (degβπ) |
7 | | ssid 4005 |
. . . . . 6
β’ β
β β |
8 | 7 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
9 | | reelprrecn 11202 |
. . . . . 6
β’ β
β {β, β} |
10 | 9 | a1i 11 |
. . . . 5
β’ (π β β β {β,
β}) |
11 | | reopn 43999 |
. . . . . . 7
β’ β
β (topGenβran (,)) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
13 | 12 | tgioo2 24319 |
. . . . . . 7
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
14 | 11, 13 | eleqtri 2832 |
. . . . . 6
β’ β
β ((TopOpenββfld) βΎt
β) |
15 | 14 | a1i 11 |
. . . . 5
β’ (π β β β
((TopOpenββfld) βΎt
β)) |
16 | | etransclem47.p |
. . . . . 6
β’ (π β π β β) |
17 | | prmnn 16611 |
. . . . . 6
β’ (π β β β π β
β) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (π β π β β) |
19 | | etransclem47.f |
. . . . 5
β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
20 | | etransclem47.l |
. . . . 5
β’ πΏ = Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) |
21 | | eqid 2733 |
. . . . 5
β’ ((π Β· π) + (π β 1)) = ((π Β· π) + (π β 1)) |
22 | | fveq2 6892 |
. . . . . . 7
β’ (π¦ = π₯ β (((β Dπ
πΉ)βπ)βπ¦) = (((β Dπ πΉ)βπ)βπ₯)) |
23 | 22 | sumeq2sdv 15650 |
. . . . . 6
β’ (π¦ = π₯ β Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦) = Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ₯)) |
24 | 23 | cbvmptv 5262 |
. . . . 5
β’ (π¦ β β β¦
Ξ£π β
(0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦)) = (π₯ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ₯)) |
25 | | negeq 11452 |
. . . . . . . . 9
β’ (π§ = π₯ β -π§ = -π₯) |
26 | 25 | oveq2d 7425 |
. . . . . . . 8
β’ (π§ = π₯ β (eβπ-π§) =
(eβπ-π₯)) |
27 | | fveq2 6892 |
. . . . . . . 8
β’ (π§ = π₯ β ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ§) = ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ₯)) |
28 | 26, 27 | oveq12d 7427 |
. . . . . . 7
β’ (π§ = π₯ β ((eβπ-π§) Β· ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ§)) = ((eβπ-π₯) Β· ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ₯))) |
29 | 28 | negeqd 11454 |
. . . . . 6
β’ (π§ = π₯ β -((eβπ-π§) Β· ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ§)) = -((eβπ-π₯) Β· ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ₯))) |
30 | 29 | cbvmptv 5262 |
. . . . 5
β’ (π§ β (0[,]π) β¦
-((eβπ-π§) Β· ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ§))) = (π₯ β (0[,]π) β¦
-((eβπ-π₯) Β· ((π¦ β β β¦ Ξ£π β (0...((π Β· π) + (π β 1)))(((β
Dπ πΉ)βπ)βπ¦))βπ₯))) |
31 | 3, 4, 5, 6, 8, 10,
15, 18, 19, 20, 21, 24, 30 | etransclem46 44996 |
. . . 4
β’ (π β (πΏ / (!β(π β 1))) = (-Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
32 | | fzfid 13938 |
. . . . . . . 8
β’ (π β (0...π) β Fin) |
33 | | fzfid 13938 |
. . . . . . . 8
β’ (π β (0...((π Β· π) + (π β 1))) β Fin) |
34 | | xpfi 9317 |
. . . . . . . 8
β’
(((0...π) β Fin
β§ (0...((π Β·
π) + (π β 1))) β Fin) β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β Fin) |
35 | 32, 33, 34 | syl2anc 585 |
. . . . . . 7
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β Fin) |
36 | 3 | eldifad 3961 |
. . . . . . . . . . . 12
β’ (π β π β
(Polyββ€)) |
37 | | 0zd 12570 |
. . . . . . . . . . . 12
β’ (π β 0 β
β€) |
38 | 5 | coef2 25745 |
. . . . . . . . . . . 12
β’ ((π β (Polyββ€)
β§ 0 β β€) β π΄:β0βΆβ€) |
39 | 36, 37, 38 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π΄:β0βΆβ€) |
40 | 39 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β π΄:β0βΆβ€) |
41 | | xp1st 8007 |
. . . . . . . . . . . 12
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (1st
βπ) β (0...π)) |
42 | | elfznn0 13594 |
. . . . . . . . . . . 12
β’
((1st βπ) β (0...π) β (1st βπ) β
β0) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (1st
βπ) β
β0) |
44 | 43 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (1st
βπ) β
β0) |
45 | 40, 44 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (π΄β(1st βπ)) β
β€) |
46 | 45 | zcnd 12667 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (π΄β(1st βπ)) β
β) |
47 | 9 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β β β
{β, β}) |
48 | 14 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β β β
((TopOpenββfld) βΎt
β)) |
49 | 18 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β π β β) |
50 | | dgrcl 25747 |
. . . . . . . . . . . . 13
β’ (π β (Polyββ€)
β (degβπ) β
β0) |
51 | 36, 50 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (degβπ) β
β0) |
52 | 6, 51 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
53 | 52 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β π β
β0) |
54 | | xp2nd 8008 |
. . . . . . . . . . . 12
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (2nd
βπ) β
(0...((π Β· π) + (π β 1)))) |
55 | | elfznn0 13594 |
. . . . . . . . . . . 12
β’
((2nd βπ) β (0...((π Β· π) + (π β 1))) β (2nd
βπ) β
β0) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (2nd
βπ) β
β0) |
57 | 56 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (2nd
βπ) β
β0) |
58 | 47, 48, 49, 53, 19, 57 | etransclem33 44983 |
. . . . . . . . 9
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β ((β
Dπ πΉ)β(2nd βπ)):ββΆβ) |
59 | 44 | nn0red 12533 |
. . . . . . . . 9
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (1st
βπ) β
β) |
60 | 58, 59 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ)) β
β) |
61 | 46, 60 | mulcld 11234 |
. . . . . . 7
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β ((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β) |
62 | 35, 61 | fsumcl 15679 |
. . . . . 6
β’ (π β Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β) |
63 | | nnm1nn0 12513 |
. . . . . . . . 9
β’ (π β β β (π β 1) β
β0) |
64 | 18, 63 | syl 17 |
. . . . . . . 8
β’ (π β (π β 1) β
β0) |
65 | 64 | faccld 14244 |
. . . . . . 7
β’ (π β (!β(π β 1)) β
β) |
66 | 65 | nncnd 12228 |
. . . . . 6
β’ (π β (!β(π β 1)) β
β) |
67 | 65 | nnne0d 12262 |
. . . . . 6
β’ (π β (!β(π β 1)) β
0) |
68 | 62, 66, 67 | divnegd 12003 |
. . . . 5
β’ (π β -(Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))) =
(-Ξ£π β
((0...π) Γ
(0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
69 | 68 | eqcomd 2739 |
. . . 4
β’ (π β (-Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))) =
-(Ξ£π β
((0...π) Γ
(0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
70 | 2, 31, 69 | 3eqtrd 2777 |
. . 3
β’ (π β πΎ = -(Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
71 | | eqid 2733 |
. . . . 5
β’
(Ξ£π β
((0...π) Γ
(0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))) =
(Ξ£π β
((0...π) Γ
(0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1))) |
72 | 18, 52, 19, 39, 71 | etransclem45 44995 |
. . . 4
β’ (π β (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β β€) |
73 | 72 | znegcld 12668 |
. . 3
β’ (π β -(Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β β€) |
74 | 70, 73 | eqeltrd 2834 |
. 2
β’ (π β πΎ β β€) |
75 | 1, 31 | eqtrid 2785 |
. . 3
β’ (π β πΎ = (-Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
76 | 62, 66, 67 | divcld 11990 |
. . . . 5
β’ (π β (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β β) |
77 | | etransclem47.a0 |
. . . . . 6
β’ (π β (π΄β0) β 0) |
78 | | etransclem47.ap |
. . . . . 6
β’ (π β (absβ(π΄β0)) < π) |
79 | | etransclem47.mp |
. . . . . 6
β’ (π β (!βπ) < π) |
80 | 39, 77, 52, 16, 78, 79, 19, 71 | etransclem44 44994 |
. . . . 5
β’ (π β (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β 0) |
81 | 76, 80 | negne0d 11569 |
. . . 4
β’ (π β -(Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β 0) |
82 | 69, 81 | eqnetrd 3009 |
. . 3
β’ (π β (-Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β 0) |
83 | 75, 82 | eqnetrd 3009 |
. 2
β’ (π β πΎ β 0) |
84 | | eldifsni 4794 |
. . . . . 6
β’ (π β ((Polyββ€)
β {0π}) β π β
0π) |
85 | 3, 84 | syl 17 |
. . . . 5
β’ (π β π β
0π) |
86 | | ere 16032 |
. . . . . . 7
β’ e β
β |
87 | 86 | recni 11228 |
. . . . . 6
β’ e β
β |
88 | 87 | a1i 11 |
. . . . 5
β’ (π β e β
β) |
89 | | dgrnznn 25761 |
. . . . 5
β’ (((π β (Polyββ€)
β§ π β
0π) β§ (e β β β§ (πβe) = 0)) β (degβπ) β
β) |
90 | 36, 85, 88, 4, 89 | syl22anc 838 |
. . . 4
β’ (π β (degβπ) β
β) |
91 | 6, 90 | eqeltrid 2838 |
. . 3
β’ (π β π β β) |
92 | | etransclem47.9 |
. . 3
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1)))) < 1) |
93 | 39, 20, 1, 18, 91, 19, 92 | etransclem23 44973 |
. 2
β’ (π β (absβπΎ) < 1) |
94 | | neeq1 3004 |
. . . 4
β’ (π = πΎ β (π β 0 β πΎ β 0)) |
95 | | fveq2 6892 |
. . . . 5
β’ (π = πΎ β (absβπ) = (absβπΎ)) |
96 | 95 | breq1d 5159 |
. . . 4
β’ (π = πΎ β ((absβπ) < 1 β (absβπΎ) < 1)) |
97 | 94, 96 | anbi12d 632 |
. . 3
β’ (π = πΎ β ((π β 0 β§ (absβπ) < 1) β (πΎ β 0 β§ (absβπΎ) < 1))) |
98 | 97 | rspcev 3613 |
. 2
β’ ((πΎ β β€ β§ (πΎ β 0 β§ (absβπΎ) < 1)) β βπ β β€ (π β 0 β§ (absβπ) < 1)) |
99 | 74, 83, 93, 98 | syl12anc 836 |
1
β’ (π β βπ β β€ (π β 0 β§ (absβπ) < 1)) |