Step | Hyp | Ref
| Expression |
1 | | ssid 4003 |
. . . 4
β’ β
β β |
2 | | coe1term.1 |
. . . . 5
β’ πΉ = (π§ β β β¦ (π΄ Β· (π§βπ))) |
3 | 2 | ply1term 25709 |
. . . 4
β’ ((β
β β β§ π΄
β β β§ π
β β0) β πΉ β
(Polyββ)) |
4 | 1, 3 | mp3an1 1448 |
. . 3
β’ ((π΄ β β β§ π β β0)
β πΉ β
(Polyββ)) |
5 | | simpr 485 |
. . 3
β’ ((π΄ β β β§ π β β0)
β π β
β0) |
6 | | simpl 483 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β π΄ β
β) |
7 | | 0cn 11202 |
. . . . . 6
β’ 0 β
β |
8 | | ifcl 4572 |
. . . . . 6
β’ ((π΄ β β β§ 0 β
β) β if(π =
π, π΄, 0) β β) |
9 | 6, 7, 8 | sylancl 586 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β if(π = π, π΄, 0) β β) |
10 | 9 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β if(π = π, π΄, 0) β β) |
11 | 10 | fmpttd 7111 |
. . 3
β’ ((π΄ β β β§ π β β0)
β (π β
β0 β¦ if(π = π, π΄,
0)):β0βΆβ) |
12 | | eqid 2732 |
. . . . . . . 8
β’ (π β β0
β¦ if(π = π, π΄, 0)) = (π β β0 β¦ if(π = π, π΄, 0)) |
13 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π = π β (π = π β π = π)) |
14 | 13 | ifbid 4550 |
. . . . . . . 8
β’ (π = π β if(π = π, π΄, 0) = if(π = π, π΄, 0)) |
15 | | simpr 485 |
. . . . . . . 8
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β π β β0) |
16 | | ifcl 4572 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 0 β
β) β if(π =
π, π΄, 0) β β) |
17 | 6, 7, 16 | sylancl 586 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β if(π = π, π΄, 0) β β) |
18 | 17 | adantr 481 |
. . . . . . . 8
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β if(π = π, π΄, 0) β β) |
19 | 12, 14, 15, 18 | fvmptd3 7018 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β ((π β β0 β¦ if(π = π, π΄, 0))βπ) = if(π = π, π΄, 0)) |
20 | 19 | neeq1d 3000 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β (((π β β0 β¦ if(π = π, π΄, 0))βπ) β 0 β if(π = π, π΄, 0) β 0)) |
21 | | nn0re 12477 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
22 | 21 | leidd 11776 |
. . . . . . . 8
β’ (π β β0
β π β€ π) |
23 | 22 | ad2antlr 725 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β π β€ π) |
24 | | iffalse 4536 |
. . . . . . . . 9
β’ (Β¬
π = π β if(π = π, π΄, 0) = 0) |
25 | 24 | necon1ai 2968 |
. . . . . . . 8
β’ (if(π = π, π΄, 0) β 0 β π = π) |
26 | 25 | breq1d 5157 |
. . . . . . 7
β’ (if(π = π, π΄, 0) β 0 β (π β€ π β π β€ π)) |
27 | 23, 26 | syl5ibrcom 246 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β (if(π = π, π΄, 0) β 0 β π β€ π)) |
28 | 20, 27 | sylbid 239 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β (((π β β0 β¦ if(π = π, π΄, 0))βπ) β 0 β π β€ π)) |
29 | 28 | ralrimiva 3146 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β βπ β
β0 (((π
β β0 β¦ if(π = π, π΄, 0))βπ) β 0 β π β€ π)) |
30 | | plyco0 25697 |
. . . . 5
β’ ((π β β0
β§ (π β
β0 β¦ if(π = π, π΄, 0)):β0βΆβ)
β (((π β
β0 β¦ if(π = π, π΄, 0)) β
(β€β₯β(π + 1))) = {0} β βπ β β0
(((π β
β0 β¦ if(π = π, π΄, 0))βπ) β 0 β π β€ π))) |
31 | 5, 11, 30 | syl2anc 584 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β (((π β
β0 β¦ if(π = π, π΄, 0)) β
(β€β₯β(π + 1))) = {0} β βπ β β0
(((π β
β0 β¦ if(π = π, π΄, 0))βπ) β 0 β π β€ π))) |
32 | 29, 31 | mpbird 256 |
. . 3
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ if(π = π, π΄, 0)) β
(β€β₯β(π + 1))) = {0}) |
33 | 2 | ply1termlem 25708 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β πΉ = (π§ β β β¦
Ξ£π β (0...π)(if(π = π, π΄, 0) Β· (π§βπ)))) |
34 | | elfznn0 13590 |
. . . . . . 7
β’ (π β (0...π) β π β β0) |
35 | 19 | oveq1d 7420 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β
β0) β (((π β β0 β¦ if(π = π, π΄, 0))βπ) Β· (π§βπ)) = (if(π = π, π΄, 0) Β· (π§βπ))) |
36 | 34, 35 | sylan2 593 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β (((π β β0 β¦ if(π = π, π΄, 0))βπ) Β· (π§βπ)) = (if(π = π, π΄, 0) Β· (π§βπ))) |
37 | 36 | sumeq2dv 15645 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β Ξ£π β
(0...π)(((π β β0
β¦ if(π = π, π΄, 0))βπ) Β· (π§βπ)) = Ξ£π β (0...π)(if(π = π, π΄, 0) Β· (π§βπ))) |
38 | 37 | mpteq2dv 5249 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β (π§ β β
β¦ Ξ£π β
(0...π)(((π β β0
β¦ if(π = π, π΄, 0))βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)(if(π = π, π΄, 0) Β· (π§βπ)))) |
39 | 33, 38 | eqtr4d 2775 |
. . 3
β’ ((π΄ β β β§ π β β0)
β πΉ = (π§ β β β¦
Ξ£π β (0...π)(((π β β0 β¦ if(π = π, π΄, 0))βπ) Β· (π§βπ)))) |
40 | 4, 5, 11, 32, 39 | coeeq 25732 |
. 2
β’ ((π΄ β β β§ π β β0)
β (coeffβπΉ) =
(π β
β0 β¦ if(π = π, π΄, 0))) |
41 | 4 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
πΉ β
(Polyββ)) |
42 | 5 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
π β
β0) |
43 | 11 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
(π β
β0 β¦ if(π = π, π΄,
0)):β0βΆβ) |
44 | 32 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
((π β
β0 β¦ if(π = π, π΄, 0)) β
(β€β₯β(π + 1))) = {0}) |
45 | 39 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
πΉ = (π§ β β β¦ Ξ£π β (0...π)(((π β β0 β¦ if(π = π, π΄, 0))βπ) Β· (π§βπ)))) |
46 | | iftrue 4533 |
. . . . . . . 8
β’ (π = π β if(π = π, π΄, 0) = π΄) |
47 | 46, 12 | fvmptg 6993 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β)
β ((π β
β0 β¦ if(π = π, π΄, 0))βπ) = π΄) |
48 | 47 | ancoms 459 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ if(π = π, π΄, 0))βπ) = π΄) |
49 | 48 | neeq1d 3000 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β (((π β
β0 β¦ if(π = π, π΄, 0))βπ) β 0 β π΄ β 0)) |
50 | 49 | biimpar 478 |
. . . 4
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
((π β
β0 β¦ if(π = π, π΄, 0))βπ) β 0) |
51 | 41, 42, 43, 44, 45, 50 | dgreq 25749 |
. . 3
β’ (((π΄ β β β§ π β β0)
β§ π΄ β 0) β
(degβπΉ) = π) |
52 | 51 | ex 413 |
. 2
β’ ((π΄ β β β§ π β β0)
β (π΄ β 0 β
(degβπΉ) = π)) |
53 | 40, 52 | jca 512 |
1
β’ ((π΄ β β β§ π β β0)
β ((coeffβπΉ) =
(π β
β0 β¦ if(π = π, π΄, 0)) β§ (π΄ β 0 β (degβπΉ) = π))) |