Step | Hyp | Ref
| Expression |
1 | | dgrle.1 |
. 2
β’ (π β πΉ β (Polyβπ)) |
2 | | dgrle.2 |
. 2
β’ (π β π β
β0) |
3 | | simpll 766 |
. . . . 5
β’ (((π β§ π β β0) β§ π β€ π) β π) |
4 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β€ π) β π β€ π) |
5 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π β€ π) β π β β0) |
6 | | nn0uz 12864 |
. . . . . . . 8
β’
β0 = (β€β₯β0) |
7 | 5, 6 | eleqtrdi 2844 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β€ π) β π β
(β€β₯β0)) |
8 | 2 | nn0zd 12584 |
. . . . . . . 8
β’ (π β π β β€) |
9 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β€ π) β π β β€) |
10 | | elfz5 13493 |
. . . . . . 7
β’ ((π β
(β€β₯β0) β§ π β β€) β (π β (0...π) β π β€ π)) |
11 | 7, 9, 10 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β€ π) β (π β (0...π) β π β€ π)) |
12 | 4, 11 | mpbird 257 |
. . . . 5
β’ (((π β§ π β β0) β§ π β€ π) β π β (0...π)) |
13 | | dgrle.3 |
. . . . 5
β’ ((π β§ π β (0...π)) β π΄ β β) |
14 | 3, 12, 13 | syl2anc 585 |
. . . 4
β’ (((π β§ π β β0) β§ π β€ π) β π΄ β β) |
15 | | 0cnd 11207 |
. . . 4
β’ (((π β§ π β β0) β§ Β¬
π β€ π) β 0 β β) |
16 | 14, 15 | ifclda 4564 |
. . 3
β’ ((π β§ π β β0) β if(π β€ π, π΄, 0) β β) |
17 | 16 | fmpttd 7115 |
. 2
β’ (π β (π β β0 β¦ if(π β€ π, π΄,
0)):β0βΆβ) |
18 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β0) β π β
β0) |
19 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β0
β¦ if(π β€ π, π΄, 0)) = (π β β0 β¦ if(π β€ π, π΄, 0)) |
20 | 19 | fvmpt2 7010 |
. . . . . . . 8
β’ ((π β β0
β§ if(π β€ π, π΄, 0) β β) β ((π β β0
β¦ if(π β€ π, π΄, 0))βπ) = if(π β€ π, π΄, 0)) |
21 | 18, 16, 20 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β0
β¦ if(π β€ π, π΄, 0))βπ) = if(π β€ π, π΄, 0)) |
22 | 21 | neeq1d 3001 |
. . . . . 6
β’ ((π β§ π β β0) β (((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β if(π β€ π, π΄, 0) β 0)) |
23 | | iffalse 4538 |
. . . . . . 7
β’ (Β¬
π β€ π β if(π β€ π, π΄, 0) = 0) |
24 | 23 | necon1ai 2969 |
. . . . . 6
β’ (if(π β€ π, π΄, 0) β 0 β π β€ π) |
25 | 22, 24 | syl6bi 253 |
. . . . 5
β’ ((π β§ π β β0) β (((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π)) |
26 | 25 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β β0 (((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π)) |
27 | | nfv 1918 |
. . . . 5
β’
β²π(((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π) |
28 | | nffvmpt1 6903 |
. . . . . . 7
β’
β²π((π β β0 β¦ if(π β€ π, π΄, 0))βπ) |
29 | | nfcv 2904 |
. . . . . . 7
β’
β²π0 |
30 | 28, 29 | nfne 3044 |
. . . . . 6
β’
β²π((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 |
31 | | nfv 1918 |
. . . . . 6
β’
β²π π β€ π |
32 | 30, 31 | nfim 1900 |
. . . . 5
β’
β²π(((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π) |
33 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β ((π β β0 β¦ if(π β€ π, π΄, 0))βπ) = ((π β β0 β¦ if(π β€ π, π΄, 0))βπ)) |
34 | 33 | neeq1d 3001 |
. . . . . 6
β’ (π = π β (((π β β0 β¦ if(π β€ π, π΄, 0))βπ) β 0 β ((π β β0 β¦ if(π β€ π, π΄, 0))βπ) β 0)) |
35 | | breq1 5152 |
. . . . . 6
β’ (π = π β (π β€ π β π β€ π)) |
36 | 34, 35 | imbi12d 345 |
. . . . 5
β’ (π = π β ((((π β β0 β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π) β (((π β β0 β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π))) |
37 | 27, 32, 36 | cbvralw 3304 |
. . . 4
β’
(βπ β
β0 (((π
β β0 β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π) β βπ β β0 (((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π)) |
38 | 26, 37 | sylib 217 |
. . 3
β’ (π β βπ β β0 (((π β β0
β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π)) |
39 | | plyco0 25706 |
. . . 4
β’ ((π β β0
β§ (π β
β0 β¦ if(π β€ π, π΄, 0)):β0βΆβ)
β (((π β
β0 β¦ if(π β€ π, π΄, 0)) β
(β€β₯β(π + 1))) = {0} β βπ β β0
(((π β
β0 β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π))) |
40 | 2, 17, 39 | syl2anc 585 |
. . 3
β’ (π β (((π β β0 β¦ if(π β€ π, π΄, 0)) β
(β€β₯β(π + 1))) = {0} β βπ β β0
(((π β
β0 β¦ if(π β€ π, π΄, 0))βπ) β 0 β π β€ π))) |
41 | 38, 40 | mpbird 257 |
. 2
β’ (π β ((π β β0 β¦ if(π β€ π, π΄, 0)) β
(β€β₯β(π + 1))) = {0}) |
42 | | dgrle.4 |
. . 3
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...π)(π΄ Β· (π§βπ)))) |
43 | | nfcv 2904 |
. . . . . 6
β’
β²π(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) |
44 | | nfcv 2904 |
. . . . . . 7
β’
β²π
Β· |
45 | | nfcv 2904 |
. . . . . . 7
β’
β²π(π§βπ) |
46 | 28, 44, 45 | nfov 7439 |
. . . . . 6
β’
β²π(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) |
47 | | oveq2 7417 |
. . . . . . 7
β’ (π = π β (π§βπ) = (π§βπ)) |
48 | 33, 47 | oveq12d 7427 |
. . . . . 6
β’ (π = π β (((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) = (((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ))) |
49 | 43, 46, 48 | cbvsumi 15643 |
. . . . 5
β’
Ξ£π β
(0...π)(((π β β0
β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) = Ξ£π β (0...π)(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) |
50 | | elfznn0 13594 |
. . . . . . . . . 10
β’ (π β (0...π) β π β β0) |
51 | 50 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β (0...π)) β π β β0) |
52 | | elfzle2 13505 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β€ π) |
53 | 52 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β (0...π)) β π β€ π) |
54 | 53 | iftrued 4537 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β (0...π)) β if(π β€ π, π΄, 0) = π΄) |
55 | 13 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β (0...π)) β π΄ β β) |
56 | 54, 55 | eqeltrd 2834 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β (0...π)) β if(π β€ π, π΄, 0) β β) |
57 | 51, 56, 20 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π β (0...π)) β ((π β β0 β¦ if(π β€ π, π΄, 0))βπ) = if(π β€ π, π΄, 0)) |
58 | 57, 54 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π β (0...π)) β ((π β β0 β¦ if(π β€ π, π΄, 0))βπ) = π΄) |
59 | 58 | oveq1d 7424 |
. . . . . 6
β’ (((π β§ π§ β β) β§ π β (0...π)) β (((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) = (π΄ Β· (π§βπ))) |
60 | 59 | sumeq2dv 15649 |
. . . . 5
β’ ((π β§ π§ β β) β Ξ£π β (0...π)(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) = Ξ£π β (0...π)(π΄ Β· (π§βπ))) |
61 | 49, 60 | eqtr3id 2787 |
. . . 4
β’ ((π β§ π§ β β) β Ξ£π β (0...π)(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)) = Ξ£π β (0...π)(π΄ Β· (π§βπ))) |
62 | 61 | mpteq2dva 5249 |
. . 3
β’ (π β (π§ β β β¦ Ξ£π β (0...π)(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)(π΄ Β· (π§βπ)))) |
63 | 42, 62 | eqtr4d 2776 |
. 2
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...π)(((π β β0 β¦ if(π β€ π, π΄, 0))βπ) Β· (π§βπ)))) |
64 | 1, 2, 17, 41, 63 | coeeq 25741 |
1
β’ (π β (coeffβπΉ) = (π β β0 β¦ if(π β€ π, π΄, 0))) |