Step | Hyp | Ref
| Expression |
1 | | plyf 25712 |
. . . . 5
β’ (πΉ β (Polyββ)
β πΉ:ββΆβ) |
2 | 1 | ffnd 6719 |
. . . 4
β’ (πΉ β (Polyββ)
β πΉ Fn
β) |
3 | | ovex 7442 |
. . . . . 6
β’ (π₯βπ·) β V |
4 | 3 | rgenw 3066 |
. . . . 5
β’
βπ₯ β
β+ (π₯βπ·) β V |
5 | | signsplypnf.g |
. . . . . 6
β’ πΊ = (π₯ β β+ β¦ (π₯βπ·)) |
6 | 5 | fnmpt 6691 |
. . . . 5
β’
(βπ₯ β
β+ (π₯βπ·) β V β πΊ Fn β+) |
7 | 4, 6 | mp1i 13 |
. . . 4
β’ (πΉ β (Polyββ)
β πΊ Fn
β+) |
8 | | cnex 11191 |
. . . . 5
β’ β
β V |
9 | 8 | a1i 11 |
. . . 4
β’ (πΉ β (Polyββ)
β β β V) |
10 | | reex 11201 |
. . . . . 6
β’ β
β V |
11 | | rpssre 12981 |
. . . . . 6
β’
β+ β β |
12 | 10, 11 | ssexi 5323 |
. . . . 5
β’
β+ β V |
13 | 12 | a1i 11 |
. . . 4
β’ (πΉ β (Polyββ)
β β+ β V) |
14 | | ax-resscn 11167 |
. . . . . 6
β’ β
β β |
15 | 11, 14 | sstri 3992 |
. . . . 5
β’
β+ β β |
16 | | sseqin2 4216 |
. . . . 5
β’
(β+ β β β (β β©
β+) = β+) |
17 | 15, 16 | mpbi 229 |
. . . 4
β’ (β
β© β+) = β+ |
18 | | signsply0.c |
. . . . 5
β’ πΆ = (coeffβπΉ) |
19 | | signsply0.d |
. . . . 5
β’ π· = (degβπΉ) |
20 | 18, 19 | coeid2 25753 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ π₯ β β)
β (πΉβπ₯) = Ξ£π β (0...π·)((πΆβπ) Β· (π₯βπ))) |
21 | 5 | fvmpt2 7010 |
. . . . . 6
β’ ((π₯ β β+
β§ (π₯βπ·) β V) β (πΊβπ₯) = (π₯βπ·)) |
22 | 3, 21 | mpan2 690 |
. . . . 5
β’ (π₯ β β+
β (πΊβπ₯) = (π₯βπ·)) |
23 | 22 | adantl 483 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (πΊβπ₯) = (π₯βπ·)) |
24 | 2, 7, 9, 13, 17, 20, 23 | offval 7679 |
. . 3
β’ (πΉ β (Polyββ)
β (πΉ
βf / πΊ) =
(π₯ β
β+ β¦ (Ξ£π β (0...π·)((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)))) |
25 | | fzfid 13938 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (0...π·) β Fin) |
26 | 15 | a1i 11 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β β+ β β) |
27 | 26 | sselda 3983 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β π₯ β β) |
28 | | dgrcl 25747 |
. . . . . . . . 9
β’ (πΉ β (Polyββ)
β (degβπΉ) β
β0) |
29 | 19, 28 | eqeltrid 2838 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β π· β
β0) |
30 | 29 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β π· β
β0) |
31 | 27, 30 | expcld 14111 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (π₯βπ·) β β) |
32 | 18 | coef3 25746 |
. . . . . . . . 9
β’ (πΉ β (Polyββ)
β πΆ:β0βΆβ) |
33 | 32 | ad2antrr 725 |
. . . . . . . 8
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β πΆ:β0βΆβ) |
34 | | elfznn0 13594 |
. . . . . . . . 9
β’ (π β (0...π·) β π β β0) |
35 | 34 | adantl 483 |
. . . . . . . 8
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β π β β0) |
36 | 33, 35 | ffvelcdmd 7088 |
. . . . . . 7
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β (πΆβπ) β β) |
37 | 27 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β π₯ β β) |
38 | 37, 35 | expcld 14111 |
. . . . . . 7
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β (π₯βπ) β β) |
39 | 36, 38 | mulcld 11234 |
. . . . . 6
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β ((πΆβπ) Β· (π₯βπ)) β β) |
40 | | rpne0 12990 |
. . . . . . . 8
β’ (π₯ β β+
β π₯ β
0) |
41 | 40 | adantl 483 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β π₯ β 0) |
42 | 29 | nn0zd 12584 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β π· β
β€) |
43 | 42 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β π· β β€) |
44 | 27, 41, 43 | expne0d 14117 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (π₯βπ·) β 0) |
45 | 25, 31, 39, 44 | fsumdivc 15732 |
. . . . 5
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (Ξ£π β (0...π·)((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = Ξ£π β (0...π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) |
46 | | fzosn 13703 |
. . . . . . . . 9
β’ (π· β β€ β (π·..^(π· + 1)) = {π·}) |
47 | 46 | ineq2d 4213 |
. . . . . . . 8
β’ (π· β β€ β
((0..^π·) β© (π·..^(π· + 1))) = ((0..^π·) β© {π·})) |
48 | | fzodisj 13666 |
. . . . . . . 8
β’
((0..^π·) β©
(π·..^(π· + 1))) = β
|
49 | 47, 48 | eqtr3di 2788 |
. . . . . . 7
β’ (π· β β€ β
((0..^π·) β© {π·}) = β
) |
50 | 43, 49 | syl 17 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β ((0..^π·) β© {π·}) = β
) |
51 | | fzval3 13701 |
. . . . . . . . 9
β’ (π· β β€ β
(0...π·) = (0..^(π· + 1))) |
52 | 42, 51 | syl 17 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β (0...π·) =
(0..^(π· +
1))) |
53 | | nn0uz 12864 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
54 | 29, 53 | eleqtrdi 2844 |
. . . . . . . . 9
β’ (πΉ β (Polyββ)
β π· β
(β€β₯β0)) |
55 | | fzosplitsn 13740 |
. . . . . . . . 9
β’ (π· β
(β€β₯β0) β (0..^(π· + 1)) = ((0..^π·) βͺ {π·})) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β (0..^(π· + 1)) =
((0..^π·) βͺ {π·})) |
57 | 52, 56 | eqtrd 2773 |
. . . . . . 7
β’ (πΉ β (Polyββ)
β (0...π·) =
((0..^π·) βͺ {π·})) |
58 | 57 | adantr 482 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (0...π·) = ((0..^π·) βͺ {π·})) |
59 | 31 | adantr 482 |
. . . . . . 7
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β (π₯βπ·) β β) |
60 | 41 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β π₯ β 0) |
61 | 43 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β π· β β€) |
62 | 37, 60, 61 | expne0d 14117 |
. . . . . . 7
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β (π₯βπ·) β 0) |
63 | 39, 59, 62 | divcld 11990 |
. . . . . 6
β’ (((πΉ β (Polyββ)
β§ π₯ β
β+) β§ π β (0...π·)) β (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) β β) |
64 | 50, 58, 25, 63 | fsumsplit 15687 |
. . . . 5
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β Ξ£π β (0...π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = (Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) + Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)))) |
65 | 45, 64 | eqtrd 2773 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (Ξ£π β (0...π·)((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = (Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) + Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)))) |
66 | 65 | mpteq2dva 5249 |
. . 3
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ (Ξ£π β (0...π·)((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) = (π₯ β β+ β¦
(Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) + Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))))) |
67 | 24, 66 | eqtrd 2773 |
. 2
β’ (πΉ β (Polyββ)
β (πΉ
βf / πΊ) =
(π₯ β
β+ β¦ (Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) + Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))))) |
68 | | sumex 15634 |
. . . . 5
β’
Ξ£π β
(0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) β V |
69 | 68 | a1i 11 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) β V) |
70 | | sumex 15634 |
. . . . 5
β’
Ξ£π β
{π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) β V |
71 | 70 | a1i 11 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) β V) |
72 | 11 | a1i 11 |
. . . . . 6
β’ (πΉ β (Polyββ)
β β+ β β) |
73 | | fzofi 13939 |
. . . . . . 7
β’
(0..^π·) β
Fin |
74 | 73 | a1i 11 |
. . . . . 6
β’ (πΉ β (Polyββ)
β (0..^π·) β
Fin) |
75 | | ovexd 7444 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ (π₯ β
β+ β§ π
β (0..^π·))) β
(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) β V) |
76 | 32 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β πΆ:β0βΆβ) |
77 | | elfzonn0 13677 |
. . . . . . . . . . 11
β’ (π β (0..^π·) β π β β0) |
78 | 77 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π β
β0) |
79 | 76, 78 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (πΆβπ) β β) |
80 | 27 | adantlr 714 |
. . . . . . . . . 10
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π₯ β
β) |
81 | 80, 78 | expcld 14111 |
. . . . . . . . 9
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯βπ) β β) |
82 | 31 | adantlr 714 |
. . . . . . . . 9
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯βπ·) β β) |
83 | 40 | adantl 483 |
. . . . . . . . . 10
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π₯ β 0) |
84 | 43 | adantlr 714 |
. . . . . . . . . 10
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π· β
β€) |
85 | 80, 83, 84 | expne0d 14117 |
. . . . . . . . 9
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯βπ·) β 0) |
86 | 79, 81, 82, 85 | divassd 12025 |
. . . . . . . 8
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = ((πΆβπ) Β· ((π₯βπ) / (π₯βπ·)))) |
87 | 86 | mpteq2dva 5249 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) = (π₯ β β+ β¦ ((πΆβπ) Β· ((π₯βπ) / (π₯βπ·))))) |
88 | | fvexd 6907 |
. . . . . . . . 9
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (πΆβπ) β V) |
89 | | ovexd 7444 |
. . . . . . . . 9
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β ((π₯βπ) / (π₯βπ·)) β V) |
90 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β πΆ:β0βΆβ) |
91 | 77 | adantl 483 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β π β β0) |
92 | 90, 91 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (πΆβπ) β β) |
93 | | rlimconst 15488 |
. . . . . . . . . 10
β’
((β+ β β β§ (πΆβπ) β β) β (π₯ β β+ β¦ (πΆβπ)) βπ (πΆβπ)) |
94 | 11, 92, 93 | sylancr 588 |
. . . . . . . . 9
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ (πΆβπ)) βπ (πΆβπ)) |
95 | 78 | nn0zd 12584 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π β
β€) |
96 | 84, 95 | zsubcld 12671 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π· β π) β β€) |
97 | 80, 83, 96 | cxpexpzd 26219 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯βπ(π· β π)) = (π₯β(π· β π))) |
98 | 97 | oveq2d 7425 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (1 /
(π₯βπ(π· β π))) = (1 / (π₯β(π· β π)))) |
99 | 80, 83, 96 | expnegd 14118 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯β-(π· β π)) = (1 / (π₯β(π· β π)))) |
100 | 84 | zcnd 12667 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π· β
β) |
101 | 78 | nn0cnd 12534 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β π β
β) |
102 | 100, 101 | negsubdi2d 11587 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β -(π· β π) = (π β π·)) |
103 | 102 | oveq2d 7425 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯β-(π· β π)) = (π₯β(π β π·))) |
104 | 98, 99, 103 | 3eqtr2d 2779 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (1 /
(π₯βπ(π· β π))) = (π₯β(π β π·))) |
105 | 80, 83, 84, 95 | expsubd 14122 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (π₯β(π β π·)) = ((π₯βπ) / (π₯βπ·))) |
106 | 104, 105 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyββ)
β§ π β (0..^π·)) β§ π₯ β β+) β (1 /
(π₯βπ(π· β π))) = ((π₯βπ) / (π₯βπ·))) |
107 | 106 | mpteq2dva 5249 |
. . . . . . . . . 10
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ (1 /
(π₯βπ(π· β π)))) = (π₯ β β+ β¦ ((π₯βπ) / (π₯βπ·)))) |
108 | 91 | nn0red 12533 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β π β β) |
109 | 29 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β π· β
β0) |
110 | 109 | nn0red 12533 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β π· β β) |
111 | | elfzolt2 13641 |
. . . . . . . . . . . . 13
β’ (π β (0..^π·) β π < π·) |
112 | 111 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β π < π·) |
113 | | difrp 13012 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π· β β) β (π < π· β (π· β π) β
β+)) |
114 | 113 | biimpa 478 |
. . . . . . . . . . . 12
β’ (((π β β β§ π· β β) β§ π < π·) β (π· β π) β
β+) |
115 | 108, 110,
112, 114 | syl21anc 837 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π· β π) β
β+) |
116 | | cxplim 26476 |
. . . . . . . . . . 11
β’ ((π· β π) β β+ β (π₯ β β+
β¦ (1 / (π₯βπ(π· β π)))) βπ
0) |
117 | 115, 116 | syl 17 |
. . . . . . . . . 10
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ (1 /
(π₯βπ(π· β π)))) βπ
0) |
118 | 107, 117 | eqbrtrrd 5173 |
. . . . . . . . 9
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ ((π₯βπ) / (π₯βπ·))) βπ
0) |
119 | 88, 89, 94, 118 | rlimmul 15590 |
. . . . . . . 8
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ ((πΆβπ) Β· ((π₯βπ) / (π₯βπ·)))) βπ ((πΆβπ) Β· 0)) |
120 | 92 | mul01d 11413 |
. . . . . . . 8
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β ((πΆβπ) Β· 0) = 0) |
121 | 119, 120 | breqtrd 5175 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ ((πΆβπ) Β· ((π₯βπ) / (π₯βπ·)))) βπ
0) |
122 | 87, 121 | eqbrtrd 5171 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π β (0..^π·)) β (π₯ β β+ β¦ (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) βπ
0) |
123 | 72, 74, 75, 122 | fsumrlim 15757 |
. . . . 5
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) βπ Ξ£π β (0..^π·)0) |
124 | 74 | olcd 873 |
. . . . . 6
β’ (πΉ β (Polyββ)
β ((0..^π·) β
(β€β₯β0) β¨ (0..^π·) β Fin)) |
125 | | sumz 15668 |
. . . . . 6
β’
(((0..^π·) β
(β€β₯β0) β¨ (0..^π·) β Fin) β Ξ£π β (0..^π·)0 = 0) |
126 | 124, 125 | syl 17 |
. . . . 5
β’ (πΉ β (Polyββ)
β Ξ£π β
(0..^π·)0 =
0) |
127 | 123, 126 | breqtrd 5175 |
. . . 4
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) βπ
0) |
128 | 32, 29 | ffvelcdmd 7088 |
. . . . . . . . . . 11
β’ (πΉ β (Polyββ)
β (πΆβπ·) β
β) |
129 | 128 | adantr 482 |
. . . . . . . . . 10
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (πΆβπ·) β β) |
130 | 129, 31 | mulcld 11234 |
. . . . . . . . 9
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β ((πΆβπ·) Β· (π₯βπ·)) β β) |
131 | 130, 31, 44 | divcld 11990 |
. . . . . . . 8
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (((πΆβπ·) Β· (π₯βπ·)) / (π₯βπ·)) β β) |
132 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = π· β (πΆβπ) = (πΆβπ·)) |
133 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π = π· β (π₯βπ) = (π₯βπ·)) |
134 | 132, 133 | oveq12d 7427 |
. . . . . . . . . 10
β’ (π = π· β ((πΆβπ) Β· (π₯βπ)) = ((πΆβπ·) Β· (π₯βπ·))) |
135 | 134 | oveq1d 7424 |
. . . . . . . . 9
β’ (π = π· β (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = (((πΆβπ·) Β· (π₯βπ·)) / (π₯βπ·))) |
136 | 135 | sumsn 15692 |
. . . . . . . 8
β’ ((π· β β0
β§ (((πΆβπ·) Β· (π₯βπ·)) / (π₯βπ·)) β β) β Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = (((πΆβπ·) Β· (π₯βπ·)) / (π₯βπ·))) |
137 | 30, 131, 136 | syl2anc 585 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = (((πΆβπ·) Β· (π₯βπ·)) / (π₯βπ·))) |
138 | 129, 31, 44 | divcan4d 11996 |
. . . . . . 7
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β (((πΆβπ·) Β· (π₯βπ·)) / (π₯βπ·)) = (πΆβπ·)) |
139 | 137, 138 | eqtrd 2773 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ π₯ β
β+) β Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) = (πΆβπ·)) |
140 | 139 | mpteq2dva 5249 |
. . . . 5
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) = (π₯ β β+ β¦ (πΆβπ·))) |
141 | | rlimconst 15488 |
. . . . . 6
β’
((β+ β β β§ (πΆβπ·) β β) β (π₯ β β+ β¦ (πΆβπ·)) βπ (πΆβπ·)) |
142 | 11, 128, 141 | sylancr 588 |
. . . . 5
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ (πΆβπ·)) βπ (πΆβπ·)) |
143 | 140, 142 | eqbrtrd 5171 |
. . . 4
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·))) βπ (πΆβπ·)) |
144 | 69, 71, 127, 143 | rlimadd 15587 |
. . 3
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ (Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) + Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)))) βπ (0 + (πΆβπ·))) |
145 | 128 | addlidd 11415 |
. . . 4
β’ (πΉ β (Polyββ)
β (0 + (πΆβπ·)) = (πΆβπ·)) |
146 | | signsply0.b |
. . . 4
β’ π΅ = (πΆβπ·) |
147 | 145, 146 | eqtr4di 2791 |
. . 3
β’ (πΉ β (Polyββ)
β (0 + (πΆβπ·)) = π΅) |
148 | 144, 147 | breqtrd 5175 |
. 2
β’ (πΉ β (Polyββ)
β (π₯ β
β+ β¦ (Ξ£π β (0..^π·)(((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)) + Ξ£π β {π·} (((πΆβπ) Β· (π₯βπ)) / (π₯βπ·)))) βπ π΅) |
149 | 67, 148 | eqbrtrd 5171 |
1
β’ (πΉ β (Polyββ)
β (πΉ
βf / πΊ)
βπ π΅) |