Step | Hyp | Ref
| Expression |
1 | | elaa2lem.f |
. . . 4
β’ πΉ = (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ)))) |
3 | | zsscn 12570 |
. . . . 5
β’ β€
β β |
4 | 3 | a1i 11 |
. . . 4
β’ (π β β€ β
β) |
5 | | elaa2lem.g |
. . . . . . . . 9
β’ (π β πΊ β
(Polyββ€)) |
6 | | dgrcl 25971 |
. . . . . . . . 9
β’ (πΊ β (Polyββ€)
β (degβπΊ) β
β0) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ (π β (degβπΊ) β
β0) |
8 | 7 | nn0zd 12588 |
. . . . . . 7
β’ (π β (degβπΊ) β
β€) |
9 | | elaa2lem.m |
. . . . . . . . 9
β’ π = inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) |
10 | | ssrab2 4077 |
. . . . . . . . . 10
β’ {π β β0
β£ ((coeffβπΊ)βπ) β 0} β
β0 |
11 | | nn0uz 12868 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
12 | 10, 11 | sseqtri 4018 |
. . . . . . . . . . . 12
β’ {π β β0
β£ ((coeffβπΊ)βπ) β 0} β
(β€β₯β0) |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
β’ (π β {π β β0 β£
((coeffβπΊ)βπ) β 0} β
(β€β₯β0)) |
14 | | elaa2lem.gn0 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ β
0π) |
15 | 14 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
β’ (π β Β¬ πΊ = 0π) |
16 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’
(degβπΊ) =
(degβπΊ) |
17 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’
(coeffβπΊ) =
(coeffβπΊ) |
18 | 16, 17 | dgreq0 26003 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β (Polyββ€)
β (πΊ =
0π β ((coeffβπΊ)β(degβπΊ)) = 0)) |
19 | 5, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΊ = 0π β
((coeffβπΊ)β(degβπΊ)) = 0)) |
20 | 15, 19 | mtbid 323 |
. . . . . . . . . . . . . . 15
β’ (π β Β¬ ((coeffβπΊ)β(degβπΊ)) = 0) |
21 | 20 | neqned 2947 |
. . . . . . . . . . . . . 14
β’ (π β ((coeffβπΊ)β(degβπΊ)) β 0) |
22 | 7, 21 | jca 512 |
. . . . . . . . . . . . 13
β’ (π β ((degβπΊ) β β0
β§ ((coeffβπΊ)β(degβπΊ)) β 0)) |
23 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π = (degβπΊ) β ((coeffβπΊ)βπ) = ((coeffβπΊ)β(degβπΊ))) |
24 | 23 | neeq1d 3000 |
. . . . . . . . . . . . . 14
β’ (π = (degβπΊ) β (((coeffβπΊ)βπ) β 0 β ((coeffβπΊ)β(degβπΊ)) β 0)) |
25 | 24 | elrab 3683 |
. . . . . . . . . . . . 13
β’
((degβπΊ)
β {π β
β0 β£ ((coeffβπΊ)βπ) β 0} β ((degβπΊ) β β0
β§ ((coeffβπΊ)β(degβπΊ)) β 0)) |
26 | 22, 25 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π β (degβπΊ) β {π β β0 β£
((coeffβπΊ)βπ) β 0}) |
27 | 26 | ne0d 4335 |
. . . . . . . . . . 11
β’ (π β {π β β0 β£
((coeffβπΊ)βπ) β 0} β β
) |
28 | | infssuzcl 12920 |
. . . . . . . . . . 11
β’ (({π β β0
β£ ((coeffβπΊ)βπ) β 0} β
(β€β₯β0) β§ {π β β0 β£
((coeffβπΊ)βπ) β 0} β β
) β inf({π β β0
β£ ((coeffβπΊ)βπ) β 0}, β, < ) β {π β β0
β£ ((coeffβπΊ)βπ) β 0}) |
29 | 13, 27, 28 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) β {π β β0
β£ ((coeffβπΊ)βπ) β 0}) |
30 | 10, 29 | sselid 3980 |
. . . . . . . . 9
β’ (π β inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) β
β0) |
31 | 9, 30 | eqeltrid 2837 |
. . . . . . . 8
β’ (π β π β
β0) |
32 | 31 | nn0zd 12588 |
. . . . . . 7
β’ (π β π β β€) |
33 | 8, 32 | zsubcld 12675 |
. . . . . 6
β’ (π β ((degβπΊ) β π) β β€) |
34 | 9 | a1i 11 |
. . . . . . . 8
β’ (π β π = inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < )) |
35 | | infssuzle 12919 |
. . . . . . . . 9
β’ (({π β β0
β£ ((coeffβπΊ)βπ) β 0} β
(β€β₯β0) β§ (degβπΊ) β {π β β0 β£
((coeffβπΊ)βπ) β 0}) β inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) β€
(degβπΊ)) |
36 | 13, 26, 35 | syl2anc 584 |
. . . . . . . 8
β’ (π β inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) β€
(degβπΊ)) |
37 | 34, 36 | eqbrtrd 5170 |
. . . . . . 7
β’ (π β π β€ (degβπΊ)) |
38 | 7 | nn0red 12537 |
. . . . . . . 8
β’ (π β (degβπΊ) β
β) |
39 | 31 | nn0red 12537 |
. . . . . . . 8
β’ (π β π β β) |
40 | 38, 39 | subge0d 11808 |
. . . . . . 7
β’ (π β (0 β€ ((degβπΊ) β π) β π β€ (degβπΊ))) |
41 | 37, 40 | mpbird 256 |
. . . . . 6
β’ (π β 0 β€ ((degβπΊ) β π)) |
42 | 33, 41 | jca 512 |
. . . . 5
β’ (π β (((degβπΊ) β π) β β€ β§ 0 β€
((degβπΊ) β
π))) |
43 | | elnn0z 12575 |
. . . . 5
β’
(((degβπΊ)
β π) β
β0 β (((degβπΊ) β π) β β€ β§ 0 β€
((degβπΊ) β
π))) |
44 | 42, 43 | sylibr 233 |
. . . 4
β’ (π β ((degβπΊ) β π) β
β0) |
45 | | 0zd 12574 |
. . . . . . . 8
β’ (πΊ β (Polyββ€)
β 0 β β€) |
46 | 17 | coef2 25969 |
. . . . . . . 8
β’ ((πΊ β (Polyββ€)
β§ 0 β β€) β (coeffβπΊ):β0βΆβ€) |
47 | 5, 45, 46 | syl2anc2 585 |
. . . . . . 7
β’ (π β (coeffβπΊ):β0βΆβ€) |
48 | 47 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β0) β
(coeffβπΊ):β0βΆβ€) |
49 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π β β0) β π β
β0) |
50 | 31 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β0) β π β
β0) |
51 | 49, 50 | nn0addcld 12540 |
. . . . . 6
β’ ((π β§ π β β0) β (π + π) β
β0) |
52 | 48, 51 | ffvelcdmd 7087 |
. . . . 5
β’ ((π β§ π β β0) β
((coeffβπΊ)β(π + π)) β β€) |
53 | | elaa2lem.i |
. . . . 5
β’ πΌ = (π β β0 β¦
((coeffβπΊ)β(π + π))) |
54 | 52, 53 | fmptd 7115 |
. . . 4
β’ (π β πΌ:β0βΆβ€) |
55 | | elplyr 25939 |
. . . 4
β’ ((β€
β β β§ ((degβπΊ) β π) β β0 β§ πΌ:β0βΆβ€) β
(π§ β β β¦
Ξ£π β
(0...((degβπΊ) β
π))((πΌβπ) Β· (π§βπ))) β
(Polyββ€)) |
56 | 4, 44, 54, 55 | syl3anc 1371 |
. . 3
β’ (π β (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ))) β
(Polyββ€)) |
57 | 2, 56 | eqeltrd 2833 |
. 2
β’ (π β πΉ β
(Polyββ€)) |
58 | | simpr 485 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β€ ((degβπΊ) β π)) β π β€ ((degβπΊ) β π)) |
59 | 58 | iftrued 4536 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β€ ((degβπΊ) β π)) β if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0) = ((coeffβπΊ)β(π + π))) |
60 | | iffalse 4537 |
. . . . . . . . . . 11
β’ (Β¬
π β€ ((degβπΊ) β π) β if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0) = 0) |
61 | 60 | adantl 482 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0) = 0) |
62 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β Β¬ π β€ ((degβπΊ) β π)) |
63 | 38 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β (degβπΊ) β β) |
64 | 39 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β π β β) |
65 | 63, 64 | resubcld 11646 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β ((degβπΊ) β π) β β) |
66 | | nn0re 12485 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β) |
67 | 66 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β π β β) |
68 | 65, 67 | ltnled 11365 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β (((degβπΊ) β π) < π β Β¬ π β€ ((degβπΊ) β π))) |
69 | 62, 68 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β ((degβπΊ) β π) < π) |
70 | 63, 64, 67 | ltsubaddd 11814 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β (((degβπΊ) β π) < π β (degβπΊ) < (π + π))) |
71 | 69, 70 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β (degβπΊ) < (π + π)) |
72 | | olc 866 |
. . . . . . . . . . . . 13
β’
((degβπΊ) <
(π + π) β (πΊ = 0π β¨
(degβπΊ) < (π + π))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β (πΊ = 0π β¨
(degβπΊ) < (π + π))) |
74 | 5 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β πΊ β
(Polyββ€)) |
75 | 51 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β (π + π) β
β0) |
76 | 16, 17 | dgrlt 26004 |
. . . . . . . . . . . . 13
β’ ((πΊ β (Polyββ€)
β§ (π + π) β β0)
β ((πΊ =
0π β¨ (degβπΊ) < (π + π)) β ((degβπΊ) β€ (π + π) β§ ((coeffβπΊ)β(π + π)) = 0))) |
77 | 74, 75, 76 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β ((πΊ = 0π β¨
(degβπΊ) < (π + π)) β ((degβπΊ) β€ (π + π) β§ ((coeffβπΊ)β(π + π)) = 0))) |
78 | 73, 77 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β ((degβπΊ) β€ (π + π) β§ ((coeffβπΊ)β(π + π)) = 0)) |
79 | 78 | simprd 496 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β ((coeffβπΊ)β(π + π)) = 0) |
80 | 61, 79 | eqtr4d 2775 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ Β¬
π β€ ((degβπΊ) β π)) β if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0) = ((coeffβπΊ)β(π + π))) |
81 | 59, 80 | pm2.61dan 811 |
. . . . . . . 8
β’ ((π β§ π β β0) β if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0) = ((coeffβπΊ)β(π + π))) |
82 | 81 | mpteq2dva 5248 |
. . . . . . 7
β’ (π β (π β β0 β¦ if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0)) = (π β β0 β¦
((coeffβπΊ)β(π + π)))) |
83 | 47, 4 | fssd 6735 |
. . . . . . . . . 10
β’ (π β (coeffβπΊ):β0βΆβ) |
84 | 83 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (0...((degβπΊ) β π))) β (coeffβπΊ):β0βΆβ) |
85 | | elfznn0 13598 |
. . . . . . . . . . 11
β’ (π β (0...((degβπΊ) β π)) β π β β0) |
86 | 85 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...((degβπΊ) β π))) β π β β0) |
87 | 31 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (0...((degβπΊ) β π))) β π β
β0) |
88 | 86, 87 | nn0addcld 12540 |
. . . . . . . . 9
β’ ((π β§ π β (0...((degβπΊ) β π))) β (π + π) β
β0) |
89 | 84, 88 | ffvelcdmd 7087 |
. . . . . . . 8
β’ ((π β§ π β (0...((degβπΊ) β π))) β ((coeffβπΊ)β(π + π)) β β) |
90 | | eqidd 2733 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β
(0...((degβπΊ) β
π)) =
(0...((degβπΊ) β
π))) |
91 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...((degβπΊ) β π))) β π) |
92 | 53 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β πΌ = (π β β0 β¦
((coeffβπΊ)β(π + π)))) |
93 | 92, 52 | fvmpt2d 7011 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β (πΌβπ) = ((coeffβπΊ)β(π + π))) |
94 | 91, 86, 93 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...((degβπΊ) β π))) β (πΌβπ) = ((coeffβπΊ)β(π + π))) |
95 | 94 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π β (0...((degβπΊ) β π))) β (πΌβπ) = ((coeffβπΊ)β(π + π))) |
96 | 95 | oveq1d 7426 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β (0...((degβπΊ) β π))) β ((πΌβπ) Β· (π§βπ)) = (((coeffβπΊ)β(π + π)) Β· (π§βπ))) |
97 | 90, 96 | sumeq12rdv 15657 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ)) = Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π§βπ))) |
98 | 97 | mpteq2dva 5248 |
. . . . . . . . 9
β’ (π β (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π§βπ)))) |
99 | 2, 98 | eqtrd 2772 |
. . . . . . . 8
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π§βπ)))) |
100 | 57, 44, 89, 99 | coeeq2 25980 |
. . . . . . 7
β’ (π β (coeffβπΉ) = (π β β0 β¦ if(π β€ ((degβπΊ) β π), ((coeffβπΊ)β(π + π)), 0))) |
101 | 82, 100, 92 | 3eqtr4d 2782 |
. . . . . 6
β’ (π β (coeffβπΉ) = πΌ) |
102 | 101 | fveq1d 6893 |
. . . . 5
β’ (π β ((coeffβπΉ)β0) = (πΌβ0)) |
103 | | oveq1 7418 |
. . . . . . . . 9
β’ (π = 0 β (π + π) = (0 + π)) |
104 | 103 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π = 0) β (π + π) = (0 + π)) |
105 | 3, 32 | sselid 3980 |
. . . . . . . . . 10
β’ (π β π β β) |
106 | 105 | addlidd 11419 |
. . . . . . . . 9
β’ (π β (0 + π) = π) |
107 | 106 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π = 0) β (0 + π) = π) |
108 | 104, 107 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π = 0) β (π + π) = π) |
109 | 108 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π = 0) β ((coeffβπΊ)β(π + π)) = ((coeffβπΊ)βπ)) |
110 | | 0nn0 12491 |
. . . . . . 7
β’ 0 β
β0 |
111 | 110 | a1i 11 |
. . . . . 6
β’ (π β 0 β
β0) |
112 | 47, 31 | ffvelcdmd 7087 |
. . . . . 6
β’ (π β ((coeffβπΊ)βπ) β β€) |
113 | 92, 109, 111, 112 | fvmptd 7005 |
. . . . 5
β’ (π β (πΌβ0) = ((coeffβπΊ)βπ)) |
114 | | eqidd 2733 |
. . . . 5
β’ (π β ((coeffβπΊ)βπ) = ((coeffβπΊ)βπ)) |
115 | 102, 113,
114 | 3eqtrd 2776 |
. . . 4
β’ (π β ((coeffβπΉ)β0) = ((coeffβπΊ)βπ)) |
116 | 34, 29 | eqeltrd 2833 |
. . . . . 6
β’ (π β π β {π β β0 β£
((coeffβπΊ)βπ) β 0}) |
117 | | fveq2 6891 |
. . . . . . . 8
β’ (π = π β ((coeffβπΊ)βπ) = ((coeffβπΊ)βπ)) |
118 | 117 | neeq1d 3000 |
. . . . . . 7
β’ (π = π β (((coeffβπΊ)βπ) β 0 β ((coeffβπΊ)βπ) β 0)) |
119 | 118 | elrab 3683 |
. . . . . 6
β’ (π β {π β β0 β£
((coeffβπΊ)βπ) β 0} β (π β β0 β§
((coeffβπΊ)βπ) β 0)) |
120 | 116, 119 | sylib 217 |
. . . . 5
β’ (π β (π β β0 β§
((coeffβπΊ)βπ) β 0)) |
121 | 120 | simprd 496 |
. . . 4
β’ (π β ((coeffβπΊ)βπ) β 0) |
122 | 115, 121 | eqnetrd 3008 |
. . 3
β’ (π β ((coeffβπΉ)β0) β
0) |
123 | 5, 45 | syl 17 |
. . . . . . 7
β’ (π β 0 β
β€) |
124 | | aasscn 26055 |
. . . . . . . . . . 11
β’ πΈ
β β |
125 | | elaa2lem.a |
. . . . . . . . . . 11
β’ (π β π΄ β πΈ) |
126 | 124, 125 | sselid 3980 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
127 | 91, 126 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (0...((degβπΊ) β π))) β π΄ β β) |
128 | 127, 86 | expcld 14115 |
. . . . . . . 8
β’ ((π β§ π β (0...((degβπΊ) β π))) β (π΄βπ) β β) |
129 | 89, 128 | mulcld 11238 |
. . . . . . 7
β’ ((π β§ π β (0...((degβπΊ) β π))) β (((coeffβπΊ)β(π + π)) Β· (π΄βπ)) β β) |
130 | | fvoveq1 7434 |
. . . . . . . 8
β’ (π = (π β π) β ((coeffβπΊ)β(π + π)) = ((coeffβπΊ)β((π β π) + π))) |
131 | | oveq2 7419 |
. . . . . . . 8
β’ (π = (π β π) β (π΄βπ) = (π΄β(π β π))) |
132 | 130, 131 | oveq12d 7429 |
. . . . . . 7
β’ (π = (π β π) β (((coeffβπΊ)β(π + π)) Β· (π΄βπ)) = (((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π)))) |
133 | 32, 123, 33, 129, 132 | fsumshft 15730 |
. . . . . 6
β’ (π β Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π΄βπ)) = Ξ£π β ((0 + π)...(((degβπΊ) β π) + π))(((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π)))) |
134 | 3, 8 | sselid 3980 |
. . . . . . . . . 10
β’ (π β (degβπΊ) β
β) |
135 | 134, 105 | npcand 11579 |
. . . . . . . . 9
β’ (π β (((degβπΊ) β π) + π) = (degβπΊ)) |
136 | 106, 135 | oveq12d 7429 |
. . . . . . . 8
β’ (π β ((0 + π)...(((degβπΊ) β π) + π)) = (π...(degβπΊ))) |
137 | 136 | sumeq1d 15651 |
. . . . . . 7
β’ (π β Ξ£π β ((0 + π)...(((degβπΊ) β π) + π))(((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π))) = Ξ£π β (π...(degβπΊ))(((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π)))) |
138 | | elfzelz 13505 |
. . . . . . . . . . . . . 14
β’ (π β (π...(degβπΊ)) β π β β€) |
139 | 138 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(degβπΊ))) β π β β€) |
140 | 3, 139 | sselid 3980 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β π β β) |
141 | 105 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β π β β) |
142 | 140, 141 | npcand 11579 |
. . . . . . . . . . 11
β’ ((π β§ π β (π...(degβπΊ))) β ((π β π) + π) = π) |
143 | 142 | fveq2d 6895 |
. . . . . . . . . 10
β’ ((π β§ π β (π...(degβπΊ))) β ((coeffβπΊ)β((π β π) + π)) = ((coeffβπΊ)βπ)) |
144 | 143 | oveq1d 7426 |
. . . . . . . . 9
β’ ((π β§ π β (π...(degβπΊ))) β (((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π))) = (((coeffβπΊ)βπ) Β· (π΄β(π β π)))) |
145 | 126 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β π΄ β β) |
146 | | elaa2lem.an0 |
. . . . . . . . . . . . 13
β’ (π β π΄ β 0) |
147 | 146 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β π΄ β 0) |
148 | 32 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β π β β€) |
149 | 145, 147,
148, 139 | expsubd 14126 |
. . . . . . . . . . 11
β’ ((π β§ π β (π...(degβπΊ))) β (π΄β(π β π)) = ((π΄βπ) / (π΄βπ))) |
150 | 149 | oveq2d 7427 |
. . . . . . . . . 10
β’ ((π β§ π β (π...(degβπΊ))) β (((coeffβπΊ)βπ) Β· (π΄β(π β π))) = (((coeffβπΊ)βπ) Β· ((π΄βπ) / (π΄βπ)))) |
151 | 83 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(degβπΊ))) β (coeffβπΊ):β0βΆβ) |
152 | | 0red 11221 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π...(degβπΊ))) β 0 β
β) |
153 | 39 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π...(degβπΊ))) β π β β) |
154 | 139 | zred 12670 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π...(degβπΊ))) β π β β) |
155 | 31 | nn0ge0d 12539 |
. . . . . . . . . . . . . . . . 17
β’ (π β 0 β€ π) |
156 | 155 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π...(degβπΊ))) β 0 β€ π) |
157 | | elfzle1 13508 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π...(degβπΊ)) β π β€ π) |
158 | 157 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π...(degβπΊ))) β π β€ π) |
159 | 152, 153,
154, 156, 158 | letrd 11375 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π...(degβπΊ))) β 0 β€ π) |
160 | 139, 159 | jca 512 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π...(degβπΊ))) β (π β β€ β§ 0 β€ π)) |
161 | | elnn0z 12575 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π β β€
β§ 0 β€ π)) |
162 | 160, 161 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(degβπΊ))) β π β β0) |
163 | 151, 162 | ffvelcdmd 7087 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β ((coeffβπΊ)βπ) β β) |
164 | 145, 162 | expcld 14115 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β (π΄βπ) β β) |
165 | 126, 31 | expcld 14115 |
. . . . . . . . . . . . 13
β’ (π β (π΄βπ) β β) |
166 | 165 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β (π΄βπ) β β) |
167 | 145, 147,
148 | expne0d 14121 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(degβπΊ))) β (π΄βπ) β 0) |
168 | 163, 164,
166, 167 | divassd 12029 |
. . . . . . . . . . 11
β’ ((π β§ π β (π...(degβπΊ))) β ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) = (((coeffβπΊ)βπ) Β· ((π΄βπ) / (π΄βπ)))) |
169 | 168 | eqcomd 2738 |
. . . . . . . . . 10
β’ ((π β§ π β (π...(degβπΊ))) β (((coeffβπΊ)βπ) Β· ((π΄βπ) / (π΄βπ))) = ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
170 | 150, 169 | eqtr2d 2773 |
. . . . . . . . 9
β’ ((π β§ π β (π...(degβπΊ))) β ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) = (((coeffβπΊ)βπ) Β· (π΄β(π β π)))) |
171 | 144, 170 | eqtr4d 2775 |
. . . . . . . 8
β’ ((π β§ π β (π...(degβπΊ))) β (((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π))) = ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
172 | 171 | sumeq2dv 15653 |
. . . . . . 7
β’ (π β Ξ£π β (π...(degβπΊ))(((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π))) = Ξ£π β (π...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
173 | 137, 172 | eqtrd 2772 |
. . . . . 6
β’ (π β Ξ£π β ((0 + π)...(((degβπΊ) β π) + π))(((coeffβπΊ)β((π β π) + π)) Β· (π΄β(π β π))) = Ξ£π β (π...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
174 | 31, 11 | eleqtrdi 2843 |
. . . . . . . 8
β’ (π β π β
(β€β₯β0)) |
175 | | fzss1 13544 |
. . . . . . . 8
β’ (π β
(β€β₯β0) β (π...(degβπΊ)) β (0...(degβπΊ))) |
176 | 174, 175 | syl 17 |
. . . . . . 7
β’ (π β (π...(degβπΊ)) β (0...(degβπΊ))) |
177 | 163, 164 | mulcld 11238 |
. . . . . . . 8
β’ ((π β§ π β (π...(degβπΊ))) β (((coeffβπΊ)βπ) Β· (π΄βπ)) β β) |
178 | 177, 166,
167 | divcld 11994 |
. . . . . . 7
β’ ((π β§ π β (π...(degβπΊ))) β ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) β β) |
179 | 32 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β β€) |
180 | 8 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β (degβπΊ) β β€) |
181 | | eldifi 4126 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((0...(degβπΊ)) β (π...(degβπΊ))) β π β (0...(degβπΊ))) |
182 | 181 | elfzelzd 13506 |
. . . . . . . . . . . . . . . 16
β’ (π β ((0...(degβπΊ)) β (π...(degβπΊ))) β π β β€) |
183 | 182 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β β€) |
184 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β Β¬ π < π) |
185 | 39 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β β) |
186 | 183 | zred 12670 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β β) |
187 | 185, 186 | lenltd 11364 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β (π β€ π β Β¬ π < π)) |
188 | 184, 187 | mpbird 256 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β€ π) |
189 | | elfzle2 13509 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(degβπΊ)) β π β€ (degβπΊ)) |
190 | 181, 189 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β ((0...(degβπΊ)) β (π...(degβπΊ))) β π β€ (degβπΊ)) |
191 | 190 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β€ (degβπΊ)) |
192 | 179, 180,
183, 188, 191 | elfzd 13496 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β π β (π...(degβπΊ))) |
193 | | eldifn 4127 |
. . . . . . . . . . . . . . 15
β’ (π β ((0...(degβπΊ)) β (π...(degβπΊ))) β Β¬ π β (π...(degβπΊ))) |
194 | 193 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ π < π) β Β¬ π β (π...(degβπΊ))) |
195 | 192, 194 | condan 816 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β π < π) |
196 | 195 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π < π) |
197 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π = inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < )) |
198 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β {π β β0 β£
((coeffβπΊ)βπ) β 0} β
(β€β₯β0)) |
199 | | elfznn0 13598 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0...(degβπΊ)) β π β β0) |
200 | 181, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((0...(degβπΊ)) β (π...(degβπΊ))) β π β β0) |
201 | 200 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((0...(degβπΊ)) β (π...(degβπΊ))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π β β0) |
202 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
((coeffβπΊ)βπ) = 0 β ((coeffβπΊ)βπ) β 0) |
203 | 202 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((0...(degβπΊ)) β (π...(degβπΊ))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β ((coeffβπΊ)βπ) β 0) |
204 | 201, 203 | jca 512 |
. . . . . . . . . . . . . . . . 17
β’ ((π β ((0...(degβπΊ)) β (π...(degβπΊ))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β (π β β0 β§
((coeffβπΊ)βπ) β 0)) |
205 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((coeffβπΊ)βπ) = ((coeffβπΊ)βπ)) |
206 | 205 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((coeffβπΊ)βπ) β 0 β ((coeffβπΊ)βπ) β 0)) |
207 | 206 | elrab 3683 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π β β0 β£
((coeffβπΊ)βπ) β 0} β (π β β0 β§
((coeffβπΊ)βπ) β 0)) |
208 | 204, 207 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((π β ((0...(degβπΊ)) β (π...(degβπΊ))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π β {π β β0 β£
((coeffβπΊ)βπ) β 0}) |
209 | 208 | adantll 712 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π β {π β β0 β£
((coeffβπΊ)βπ) β 0}) |
210 | | infssuzle 12919 |
. . . . . . . . . . . . . . 15
β’ (({π β β0
β£ ((coeffβπΊ)βπ) β 0} β
(β€β₯β0) β§ π β {π β β0 β£
((coeffβπΊ)βπ) β 0}) β inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) β€ π) |
211 | 198, 209,
210 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β inf({π β β0 β£
((coeffβπΊ)βπ) β 0}, β, < ) β€ π) |
212 | 197, 211 | eqbrtrd 5170 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π β€ π) |
213 | 39 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π β β) |
214 | 182 | zred 12670 |
. . . . . . . . . . . . . . 15
β’ (π β ((0...(degβπΊ)) β (π...(degβπΊ))) β π β β) |
215 | 214 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β π β β) |
216 | 213, 215 | lenltd 11364 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β (π β€ π β Β¬ π < π)) |
217 | 212, 216 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β§ Β¬ ((coeffβπΊ)βπ) = 0) β Β¬ π < π) |
218 | 196, 217 | condan 816 |
. . . . . . . . . . 11
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β ((coeffβπΊ)βπ) = 0) |
219 | 218 | oveq1d 7426 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β (((coeffβπΊ)βπ) Β· (π΄βπ)) = (0 Β· (π΄βπ))) |
220 | 126 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β π΄ β β) |
221 | 200 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β π β β0) |
222 | 220, 221 | expcld 14115 |
. . . . . . . . . . 11
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β (π΄βπ) β β) |
223 | 222 | mul02d 11416 |
. . . . . . . . . 10
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β (0 Β· (π΄βπ)) = 0) |
224 | 219, 223 | eqtrd 2772 |
. . . . . . . . 9
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β (((coeffβπΊ)βπ) Β· (π΄βπ)) = 0) |
225 | 224 | oveq1d 7426 |
. . . . . . . 8
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) = (0 / (π΄βπ))) |
226 | 126, 146,
32 | expne0d 14121 |
. . . . . . . . . 10
β’ (π β (π΄βπ) β 0) |
227 | 165, 226 | div0d 11993 |
. . . . . . . . 9
β’ (π β (0 / (π΄βπ)) = 0) |
228 | 227 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β (0 / (π΄βπ)) = 0) |
229 | 225, 228 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π β ((0...(degβπΊ)) β (π...(degβπΊ)))) β ((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) = 0) |
230 | | fzfid 13942 |
. . . . . . 7
β’ (π β (0...(degβπΊ)) β Fin) |
231 | 176, 178,
229, 230 | fsumss 15675 |
. . . . . 6
β’ (π β Ξ£π β (π...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) = Ξ£π β (0...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
232 | 133, 173,
231 | 3eqtrd 2776 |
. . . . 5
β’ (π β Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π΄βπ)) = Ξ£π β (0...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
233 | 86, 52 | syldan 591 |
. . . . . . . . . 10
β’ ((π β§ π β (0...((degβπΊ) β π))) β ((coeffβπΊ)β(π + π)) β β€) |
234 | 53 | fvmpt2 7009 |
. . . . . . . . . 10
β’ ((π β β0
β§ ((coeffβπΊ)β(π + π)) β β€) β (πΌβπ) = ((coeffβπΊ)β(π + π))) |
235 | 86, 233, 234 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π β (0...((degβπΊ) β π))) β (πΌβπ) = ((coeffβπΊ)β(π + π))) |
236 | 235 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ π§ = π΄) β§ π β (0...((degβπΊ) β π))) β (πΌβπ) = ((coeffβπΊ)β(π + π))) |
237 | | oveq1 7418 |
. . . . . . . . 9
β’ (π§ = π΄ β (π§βπ) = (π΄βπ)) |
238 | 237 | ad2antlr 725 |
. . . . . . . 8
β’ (((π β§ π§ = π΄) β§ π β (0...((degβπΊ) β π))) β (π§βπ) = (π΄βπ)) |
239 | 236, 238 | oveq12d 7429 |
. . . . . . 7
β’ (((π β§ π§ = π΄) β§ π β (0...((degβπΊ) β π))) β ((πΌβπ) Β· (π§βπ)) = (((coeffβπΊ)β(π + π)) Β· (π΄βπ))) |
240 | 239 | sumeq2dv 15653 |
. . . . . 6
β’ ((π β§ π§ = π΄) β Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ)) = Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π΄βπ))) |
241 | | fzfid 13942 |
. . . . . . 7
β’ (π β (0...((degβπΊ) β π)) β Fin) |
242 | 241, 129 | fsumcl 15683 |
. . . . . 6
β’ (π β Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π΄βπ)) β β) |
243 | 2, 240, 126, 242 | fvmptd 7005 |
. . . . 5
β’ (π β (πΉβπ΄) = Ξ£π β (0...((degβπΊ) β π))(((coeffβπΊ)β(π + π)) Β· (π΄βπ))) |
244 | 17, 16 | coeid2 25977 |
. . . . . . . 8
β’ ((πΊ β (Polyββ€)
β§ π΄ β β)
β (πΊβπ΄) = Ξ£π β (0...(degβπΊ))(((coeffβπΊ)βπ) Β· (π΄βπ))) |
245 | 5, 126, 244 | syl2anc 584 |
. . . . . . 7
β’ (π β (πΊβπ΄) = Ξ£π β (0...(degβπΊ))(((coeffβπΊ)βπ) Β· (π΄βπ))) |
246 | 245 | oveq1d 7426 |
. . . . . 6
β’ (π β ((πΊβπ΄) / (π΄βπ)) = (Ξ£π β (0...(degβπΊ))(((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
247 | 83 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΊ))) β (coeffβπΊ):β0βΆβ) |
248 | 199 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΊ))) β π β β0) |
249 | 247, 248 | ffvelcdmd 7087 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΊ))) β ((coeffβπΊ)βπ) β β) |
250 | 126 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΊ))) β π΄ β β) |
251 | 250, 248 | expcld 14115 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΊ))) β (π΄βπ) β β) |
252 | 249, 251 | mulcld 11238 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΊ))) β (((coeffβπΊ)βπ) Β· (π΄βπ)) β β) |
253 | 230, 165,
252, 226 | fsumdivc 15736 |
. . . . . 6
β’ (π β (Ξ£π β (0...(degβπΊ))(((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ)) = Ξ£π β (0...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
254 | 246, 253 | eqtrd 2772 |
. . . . 5
β’ (π β ((πΊβπ΄) / (π΄βπ)) = Ξ£π β (0...(degβπΊ))((((coeffβπΊ)βπ) Β· (π΄βπ)) / (π΄βπ))) |
255 | 232, 243,
254 | 3eqtr4d 2782 |
. . . 4
β’ (π β (πΉβπ΄) = ((πΊβπ΄) / (π΄βπ))) |
256 | | elaa2lem.ga |
. . . . 5
β’ (π β (πΊβπ΄) = 0) |
257 | 256 | oveq1d 7426 |
. . . 4
β’ (π β ((πΊβπ΄) / (π΄βπ)) = (0 / (π΄βπ))) |
258 | 255, 257,
227 | 3eqtrd 2776 |
. . 3
β’ (π β (πΉβπ΄) = 0) |
259 | 122, 258 | jca 512 |
. 2
β’ (π β (((coeffβπΉ)β0) β 0 β§ (πΉβπ΄) = 0)) |
260 | | fveq2 6891 |
. . . . . 6
β’ (π = πΉ β (coeffβπ) = (coeffβπΉ)) |
261 | 260 | fveq1d 6893 |
. . . . 5
β’ (π = πΉ β ((coeffβπ)β0) = ((coeffβπΉ)β0)) |
262 | 261 | neeq1d 3000 |
. . . 4
β’ (π = πΉ β (((coeffβπ)β0) β 0 β ((coeffβπΉ)β0) β
0)) |
263 | | fveq1 6890 |
. . . . 5
β’ (π = πΉ β (πβπ΄) = (πΉβπ΄)) |
264 | 263 | eqeq1d 2734 |
. . . 4
β’ (π = πΉ β ((πβπ΄) = 0 β (πΉβπ΄) = 0)) |
265 | 262, 264 | anbi12d 631 |
. . 3
β’ (π = πΉ β ((((coeffβπ)β0) β 0 β§ (πβπ΄) = 0) β (((coeffβπΉ)β0) β 0 β§ (πΉβπ΄) = 0))) |
266 | 265 | rspcev 3612 |
. 2
β’ ((πΉ β (Polyββ€)
β§ (((coeffβπΉ)β0) β 0 β§ (πΉβπ΄) = 0)) β βπ β
(Polyββ€)(((coeffβπ)β0) β 0 β§ (πβπ΄) = 0)) |
267 | 57, 259, 266 | syl2anc 584 |
1
β’ (π β βπ β
(Polyββ€)(((coeffβπ)β0) β 0 β§ (πβπ΄) = 0)) |