Step | Hyp | Ref
| Expression |
1 | | coemulhi.3 |
. . . . 5
β’ π = (degβπΉ) |
2 | | dgrcl 25982 |
. . . . 5
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
3 | 1, 2 | eqeltrid 2835 |
. . . 4
β’ (πΉ β (Polyβπ) β π β
β0) |
4 | | coemulhi.4 |
. . . . 5
β’ π = (degβπΊ) |
5 | | dgrcl 25982 |
. . . . 5
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
6 | 4, 5 | eqeltrid 2835 |
. . . 4
β’ (πΊ β (Polyβπ) β π β
β0) |
7 | | nn0addcl 12511 |
. . . 4
β’ ((π β β0
β§ π β
β0) β (π + π) β
β0) |
8 | 3, 6, 7 | syl2an 594 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π + π) β
β0) |
9 | | coefv0.1 |
. . . 4
β’ π΄ = (coeffβπΉ) |
10 | | coeadd.2 |
. . . 4
β’ π΅ = (coeffβπΊ) |
11 | 9, 10 | coemul 26001 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ (π + π) β β0) β
((coeffβ(πΉ
βf Β· πΊ))β(π + π)) = Ξ£π β (0...(π + π))((π΄βπ) Β· (π΅β((π + π) β π)))) |
12 | 8, 11 | mpd3an3 1460 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβ(πΉ βf Β· πΊ))β(π + π)) = Ξ£π β (0...(π + π))((π΄βπ) Β· (π΅β((π + π) β π)))) |
13 | 6 | adantl 480 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β
β0) |
14 | 13 | nn0ge0d 12539 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β 0 β€ π) |
15 | 3 | adantr 479 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β
β0) |
16 | 15 | nn0red 12537 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β β) |
17 | 13 | nn0red 12537 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β β) |
18 | 16, 17 | addge01d 11806 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (0 β€ π β π β€ (π + π))) |
19 | 14, 18 | mpbid 231 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β€ (π + π)) |
20 | | nn0uz 12868 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
21 | 15, 20 | eleqtrdi 2841 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β
(β€β₯β0)) |
22 | 8 | nn0zd 12588 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π + π) β β€) |
23 | | elfz5 13497 |
. . . . . 6
β’ ((π β
(β€β₯β0) β§ (π + π) β β€) β (π β (0...(π + π)) β π β€ (π + π))) |
24 | 21, 22, 23 | syl2anc 582 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π β (0...(π + π)) β π β€ (π + π))) |
25 | 19, 24 | mpbird 256 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β (0...(π + π))) |
26 | 25 | snssd 4811 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β {π} β (0...(π + π))) |
27 | | elsni 4644 |
. . . . . 6
β’ (π β {π} β π = π) |
28 | 27 | adantl 480 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β {π}) β π = π) |
29 | | fveq2 6890 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
30 | | oveq2 7419 |
. . . . . . 7
β’ (π = π β ((π + π) β π) = ((π + π) β π)) |
31 | 30 | fveq2d 6894 |
. . . . . 6
β’ (π = π β (π΅β((π + π) β π)) = (π΅β((π + π) β π))) |
32 | 29, 31 | oveq12d 7429 |
. . . . 5
β’ (π = π β ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· (π΅β((π + π) β π)))) |
33 | 28, 32 | syl 17 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β {π}) β ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· (π΅β((π + π) β π)))) |
34 | 16 | recnd 11246 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β β) |
35 | 17 | recnd 11246 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π β β) |
36 | 34, 35 | pncan2d 11577 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((π + π) β π) = π) |
37 | 36 | fveq2d 6894 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π΅β((π + π) β π)) = (π΅βπ)) |
38 | 37 | oveq2d 7427 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· (π΅βπ))) |
39 | 9 | coef3 25981 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
40 | 39 | adantr 479 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π΄:β0βΆβ) |
41 | 40, 15 | ffvelcdmd 7086 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π΄βπ) β β) |
42 | 10 | coef3 25981 |
. . . . . . . . 9
β’ (πΊ β (Polyβπ) β π΅:β0βΆβ) |
43 | 42 | adantl 480 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β π΅:β0βΆβ) |
44 | 43, 13 | ffvelcdmd 7086 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π΅βπ) β β) |
45 | 41, 44 | mulcld 11238 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((π΄βπ) Β· (π΅βπ)) β β) |
46 | 38, 45 | eqeltrd 2831 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((π΄βπ) Β· (π΅β((π + π) β π))) β β) |
47 | 46 | adantr 479 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β {π}) β ((π΄βπ) Β· (π΅β((π + π) β π))) β β) |
48 | 33, 47 | eqeltrd 2831 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β {π}) β ((π΄βπ) Β· (π΅β((π + π) β π))) β β) |
49 | | simpl 481 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β πΉ β (Polyβπ)) |
50 | | eldifi 4125 |
. . . . . . . . . 10
β’ (π β ((0...(π + π)) β {π}) β π β (0...(π + π))) |
51 | | elfznn0 13598 |
. . . . . . . . . 10
β’ (π β (0...(π + π)) β π β β0) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
β’ (π β ((0...(π + π)) β {π}) β π β β0) |
53 | 9, 1 | dgrub 25983 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄βπ) β 0) β π β€ π) |
54 | 53 | 3expia 1119 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
55 | 49, 52, 54 | syl2an 594 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β ((π΄βπ) β 0 β π β€ π)) |
56 | 55 | necon1bd 2956 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (Β¬ π β€ π β (π΄βπ) = 0)) |
57 | 56 | imp 405 |
. . . . . 6
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β (π΄βπ) = 0) |
58 | 57 | oveq1d 7426 |
. . . . 5
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β ((π΄βπ) Β· (π΅β((π + π) β π))) = (0 Β· (π΅β((π + π) β π)))) |
59 | 43 | ad2antrr 722 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β π΅:β0βΆβ) |
60 | 50 | ad2antlr 723 |
. . . . . . . 8
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β π β (0...(π + π))) |
61 | | fznn0sub 13537 |
. . . . . . . 8
β’ (π β (0...(π + π)) β ((π + π) β π) β
β0) |
62 | 60, 61 | syl 17 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β ((π + π) β π) β
β0) |
63 | 59, 62 | ffvelcdmd 7086 |
. . . . . 6
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β (π΅β((π + π) β π)) β β) |
64 | 63 | mul02d 11416 |
. . . . 5
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β (0 Β· (π΅β((π + π) β π))) = 0) |
65 | 58, 64 | eqtrd 2770 |
. . . 4
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β ((π΄βπ) Β· (π΅β((π + π) β π))) = 0) |
66 | 16 | adantr 479 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β π β β) |
67 | 50 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β π β (0...(π + π))) |
68 | 67, 51 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β π β β0) |
69 | 68 | nn0red 12537 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β π β β) |
70 | 17 | adantr 479 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β π β β) |
71 | 66, 69, 70 | leadd1d 11812 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (π β€ π β (π + π) β€ (π + π))) |
72 | 8 | adantr 479 |
. . . . . . . . . . . 12
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (π + π) β
β0) |
73 | 72 | nn0red 12537 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (π + π) β β) |
74 | 73, 69, 70 | lesubadd2d 11817 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (((π + π) β π) β€ π β (π + π) β€ (π + π))) |
75 | 71, 74 | bitr4d 281 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (π β€ π β ((π + π) β π) β€ π)) |
76 | 75 | notbid 317 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (Β¬ π β€ π β Β¬ ((π + π) β π) β€ π)) |
77 | 76 | biimpa 475 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β Β¬ ((π + π) β π) β€ π) |
78 | | simpr 483 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β πΊ β (Polyβπ)) |
79 | 50, 61 | syl 17 |
. . . . . . . . . 10
β’ (π β ((0...(π + π)) β {π}) β ((π + π) β π) β
β0) |
80 | 10, 4 | dgrub 25983 |
. . . . . . . . . . 11
β’ ((πΊ β (Polyβπ) β§ ((π + π) β π) β β0 β§ (π΅β((π + π) β π)) β 0) β ((π + π) β π) β€ π) |
81 | 80 | 3expia 1119 |
. . . . . . . . . 10
β’ ((πΊ β (Polyβπ) β§ ((π + π) β π) β β0) β ((π΅β((π + π) β π)) β 0 β ((π + π) β π) β€ π)) |
82 | 78, 79, 81 | syl2an 594 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β ((π΅β((π + π) β π)) β 0 β ((π + π) β π) β€ π)) |
83 | 82 | necon1bd 2956 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (Β¬ ((π + π) β π) β€ π β (π΅β((π + π) β π)) = 0)) |
84 | 83 | imp 405 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ ((π + π) β π) β€ π) β (π΅β((π + π) β π)) = 0) |
85 | 77, 84 | syldan 589 |
. . . . . 6
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β (π΅β((π + π) β π)) = 0) |
86 | 85 | oveq2d 7427 |
. . . . 5
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· 0)) |
87 | 40 | ad2antrr 722 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β π΄:β0βΆβ) |
88 | 52 | ad2antlr 723 |
. . . . . . 7
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β π β β0) |
89 | 87, 88 | ffvelcdmd 7086 |
. . . . . 6
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β (π΄βπ) β β) |
90 | 89 | mul01d 11417 |
. . . . 5
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β ((π΄βπ) Β· 0) = 0) |
91 | 86, 90 | eqtrd 2770 |
. . . 4
β’ ((((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β§ Β¬ π β€ π) β ((π΄βπ) Β· (π΅β((π + π) β π))) = 0) |
92 | | eldifsni 4792 |
. . . . . . 7
β’ (π β ((0...(π + π)) β {π}) β π β π) |
93 | 92 | adantl 480 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β π β π) |
94 | 69, 66 | letri3d 11360 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (π = π β (π β€ π β§ π β€ π))) |
95 | 94 | necon3abid 2975 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (π β π β Β¬ (π β€ π β§ π β€ π))) |
96 | 93, 95 | mpbid 231 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β Β¬ (π β€ π β§ π β€ π)) |
97 | | ianor 978 |
. . . . 5
β’ (Β¬
(π β€ π β§ π β€ π) β (Β¬ π β€ π β¨ Β¬ π β€ π)) |
98 | 96, 97 | sylib 217 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β (Β¬ π β€ π β¨ Β¬ π β€ π)) |
99 | 65, 91, 98 | mpjaodan 955 |
. . 3
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π β ((0...(π + π)) β {π})) β ((π΄βπ) Β· (π΅β((π + π) β π))) = 0) |
100 | | fzfid 13942 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (0...(π + π)) β Fin) |
101 | 26, 48, 99, 100 | fsumss 15675 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β Ξ£π β {π} ((π΄βπ) Β· (π΅β((π + π) β π))) = Ξ£π β (0...(π + π))((π΄βπ) Β· (π΅β((π + π) β π)))) |
102 | 32 | sumsn 15696 |
. . . 4
β’ ((π β β0
β§ ((π΄βπ) Β· (π΅β((π + π) β π))) β β) β Ξ£π β {π} ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· (π΅β((π + π) β π)))) |
103 | 15, 46, 102 | syl2anc 582 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β Ξ£π β {π} ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· (π΅β((π + π) β π)))) |
104 | 103, 38 | eqtrd 2770 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β Ξ£π β {π} ((π΄βπ) Β· (π΅β((π + π) β π))) = ((π΄βπ) Β· (π΅βπ))) |
105 | 12, 101, 104 | 3eqtr2d 2776 |
1
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβ(πΉ βf Β· πΊ))β(π + π)) = ((π΄βπ) Β· (π΅βπ))) |