Step | Hyp | Ref
| Expression |
1 | | vieta1.5 |
. . . . 5
β’ (π β (β―βπ
) = π) |
2 | | vieta1lem.7 |
. . . . . . 7
β’ (π β (π· + 1) = π) |
3 | | vieta1lem.6 |
. . . . . . . 8
β’ (π β π· β β) |
4 | 3 | peano2nnd 12177 |
. . . . . . 7
β’ (π β (π· + 1) β β) |
5 | 2, 4 | eqeltrrd 2839 |
. . . . . 6
β’ (π β π β β) |
6 | 5 | nnne0d 12210 |
. . . . 5
β’ (π β π β 0) |
7 | 1, 6 | eqnetrd 3012 |
. . . 4
β’ (π β (β―βπ
) β 0) |
8 | | vieta1.4 |
. . . . . . . 8
β’ (π β πΉ β (Polyβπ)) |
9 | | vieta1.2 |
. . . . . . . . . 10
β’ π = (degβπΉ) |
10 | 9, 6 | eqnetrrid 3020 |
. . . . . . . . 9
β’ (π β (degβπΉ) β 0) |
11 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (πΉ = 0π β
(degβπΉ) =
(degβ0π)) |
12 | | dgr0 25639 |
. . . . . . . . . . 11
β’
(degβ0π) = 0 |
13 | 11, 12 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (πΉ = 0π β
(degβπΉ) =
0) |
14 | 13 | necon3i 2977 |
. . . . . . . . 9
β’
((degβπΉ) β
0 β πΉ β
0π) |
15 | 10, 14 | syl 17 |
. . . . . . . 8
β’ (π β πΉ β
0π) |
16 | | vieta1.3 |
. . . . . . . . 9
β’ π
= (β‘πΉ β {0}) |
17 | 16 | fta1 25684 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΉ β 0π) β (π
β Fin β§
(β―βπ
) β€
(degβπΉ))) |
18 | 8, 15, 17 | syl2anc 585 |
. . . . . . 7
β’ (π β (π
β Fin β§ (β―βπ
) β€ (degβπΉ))) |
19 | 18 | simpld 496 |
. . . . . 6
β’ (π β π
β Fin) |
20 | | hasheq0 14270 |
. . . . . 6
β’ (π
β Fin β
((β―βπ
) = 0
β π
=
β
)) |
21 | 19, 20 | syl 17 |
. . . . 5
β’ (π β ((β―βπ
) = 0 β π
= β
)) |
22 | 21 | necon3bid 2989 |
. . . 4
β’ (π β ((β―βπ
) β 0 β π
β β
)) |
23 | 7, 22 | mpbid 231 |
. . 3
β’ (π β π
β β
) |
24 | | n0 4311 |
. . 3
β’ (π
β β
β
βπ§ π§ β π
) |
25 | 23, 24 | sylib 217 |
. 2
β’ (π β βπ§ π§ β π
) |
26 | | incom 4166 |
. . . . 5
β’ ({π§} β© (β‘π β {0})) = ((β‘π β {0}) β© {π§}) |
27 | | vieta1.1 |
. . . . . . . . . . 11
β’ π΄ = (coeffβπΉ) |
28 | | vieta1lem.8 |
. . . . . . . . . . 11
β’ (π β βπ β (Polyββ)((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))))) |
29 | | vieta1lem.9 |
. . . . . . . . . . 11
β’ π = (πΉ quot (Xp
βf β (β Γ {π§}))) |
30 | 27, 9, 16, 8, 1, 3,
2, 28, 29 | vieta1lem1 25686 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (π β (Polyββ) β§ π· = (degβπ))) |
31 | 30 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β π· = (degβπ)) |
32 | 30 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β π β
(Polyββ)) |
33 | | dgrcl 25610 |
. . . . . . . . . . 11
β’ (π β (Polyββ)
β (degβπ) β
β0) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (degβπ) β
β0) |
35 | 34 | nn0red 12481 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β (degβπ) β β) |
36 | 31, 35 | eqeltrd 2838 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β π· β β) |
37 | 36 | ltp1d 12092 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β π· < (π· + 1)) |
38 | 36, 37 | gtned 11297 |
. . . . . . 7
β’ ((π β§ π§ β π
) β (π· + 1) β π·) |
39 | | snssi 4773 |
. . . . . . . . . . 11
β’ (π§ β (β‘π β {0}) β {π§} β (β‘π β {0})) |
40 | | ssequn1 4145 |
. . . . . . . . . . 11
β’ ({π§} β (β‘π β {0}) β ({π§} βͺ (β‘π β {0})) = (β‘π β {0})) |
41 | 39, 40 | sylib 217 |
. . . . . . . . . 10
β’ (π§ β (β‘π β {0}) β ({π§} βͺ (β‘π β {0})) = (β‘π β {0})) |
42 | 41 | fveq2d 6851 |
. . . . . . . . 9
β’ (π§ β (β‘π β {0}) β (β―β({π§} βͺ (β‘π β {0}))) = (β―β(β‘π β {0}))) |
43 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β πΉ β (Polyβπ)) |
44 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β‘πΉ β {0}) β dom πΉ |
45 | 16, 44 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . . . 20
β’ π
β dom πΉ |
46 | | plyf 25575 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
47 | | fdm 6682 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉ:ββΆβ β
dom πΉ =
β) |
48 | 8, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom πΉ = β) |
49 | 45, 48 | sseqtrid 4001 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π
β β) |
50 | 49 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β π§ β β) |
51 | 16 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β π
β π§ β (β‘πΉ β {0})) |
52 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
53 | | fniniseg 7015 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉ Fn β β (π§ β (β‘πΉ β {0}) β (π§ β β β§ (πΉβπ§) = 0))) |
54 | 8, 46, 52, 53 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π§ β (β‘πΉ β {0}) β (π§ β β β§ (πΉβπ§) = 0))) |
55 | 51, 54 | bitrid 283 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π§ β π
β (π§ β β β§ (πΉβπ§) = 0))) |
56 | 55 | simplbda 501 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β (πΉβπ§) = 0) |
57 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(Xp βf β (β Γ
{π§})) =
(Xp βf β (β Γ {π§})) |
58 | 57 | facth 25682 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β (Polyβπ) β§ π§ β β β§ (πΉβπ§) = 0) β πΉ = ((Xp
βf β (β Γ {π§})) βf Β· (πΉ quot (Xp
βf β (β Γ {π§}))))) |
59 | 43, 50, 56, 58 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β πΉ = ((Xp
βf β (β Γ {π§})) βf Β· (πΉ quot (Xp
βf β (β Γ {π§}))))) |
60 | 29 | oveq2i 7373 |
. . . . . . . . . . . . . . . . 17
β’
((Xp βf β (β Γ
{π§})) βf
Β· π) =
((Xp βf β (β Γ {π§})) βf Β·
(πΉ quot
(Xp βf β (β Γ {π§})))) |
61 | 59, 60 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π
) β πΉ = ((Xp
βf β (β Γ {π§})) βf Β· π)) |
62 | 61 | cnveqd 5836 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β β‘πΉ = β‘((Xp βf
β (β Γ {π§})) βf Β· π)) |
63 | 62 | imaeq1d 6017 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (β‘πΉ β {0}) = (β‘((Xp βf
β (β Γ {π§})) βf Β· π) β {0})) |
64 | 16, 63 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β π
= (β‘((Xp βf
β (β Γ {π§})) βf Β· π) β {0})) |
65 | | cnex 11139 |
. . . . . . . . . . . . . 14
β’ β
β V |
66 | 57 | plyremlem 25680 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β β β
((Xp βf β (β Γ {π§})) β (Polyββ)
β§ (degβ(Xp βf β (β
Γ {π§}))) = 1 β§
(β‘(Xp
βf β (β Γ {π§})) β {0}) = {π§})) |
67 | 50, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π
) β ((Xp
βf β (β Γ {π§})) β (Polyββ) β§
(degβ(Xp βf β (β Γ
{π§}))) = 1 β§ (β‘(Xp βf
β (β Γ {π§})) β {0}) = {π§})) |
68 | 67 | simp1d 1143 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β (Xp
βf β (β Γ {π§})) β
(Polyββ)) |
69 | | plyf 25575 |
. . . . . . . . . . . . . . 15
β’
((Xp βf β (β Γ
{π§})) β
(Polyββ) β (Xp βf β
(β Γ {π§})):ββΆβ) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (Xp
βf β (β Γ {π§})):ββΆβ) |
71 | | plyf 25575 |
. . . . . . . . . . . . . . 15
β’ (π β (Polyββ)
β π:ββΆβ) |
72 | 32, 71 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β π:ββΆβ) |
73 | | ofmulrt 25658 |
. . . . . . . . . . . . . 14
β’ ((β
β V β§ (Xp βf β (β
Γ {π§})):ββΆβ β§ π:ββΆβ) β
(β‘((Xp
βf β (β Γ {π§})) βf Β· π) β {0}) = ((β‘(Xp βf
β (β Γ {π§})) β {0}) βͺ (β‘π β {0}))) |
74 | 65, 70, 72, 73 | mp3an2i 1467 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β (β‘((Xp βf
β (β Γ {π§})) βf Β· π) β {0}) = ((β‘(Xp βf
β (β Γ {π§})) β {0}) βͺ (β‘π β {0}))) |
75 | 67 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (β‘(Xp βf
β (β Γ {π§})) β {0}) = {π§}) |
76 | 75 | uneq1d 4127 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β ((β‘(Xp βf
β (β Γ {π§})) β {0}) βͺ (β‘π β {0})) = ({π§} βͺ (β‘π β {0}))) |
77 | 64, 74, 76 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β π
= ({π§} βͺ (β‘π β {0}))) |
78 | 77 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (β―βπ
) = (β―β({π§} βͺ (β‘π β {0})))) |
79 | 1, 2 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’ (π β (β―βπ
) = (π· + 1)) |
80 | 79 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (β―βπ
) = (π· + 1)) |
81 | 78, 80 | eqtr3d 2779 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (β―β({π§} βͺ (β‘π β {0}))) = (π· + 1)) |
82 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β πΉ β
0π) |
83 | 61, 82 | eqnetrrd 3013 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β ((Xp
βf β (β Γ {π§})) βf Β· π) β
0π) |
84 | | plymul0or 25657 |
. . . . . . . . . . . . . . . . . . 19
β’
(((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ π β (Polyββ)) β
(((Xp βf β (β Γ {π§})) βf Β·
π) = 0π
β ((Xp βf β (β Γ
{π§})) =
0π β¨ π = 0π))) |
85 | 68, 32, 84 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β (((Xp
βf β (β Γ {π§})) βf Β· π) = 0π β
((Xp βf β (β Γ {π§})) = 0π β¨
π =
0π))) |
86 | 85 | necon3abid 2981 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β (((Xp
βf β (β Γ {π§})) βf Β· π) β 0π
β Β¬ ((Xp βf β (β
Γ {π§})) =
0π β¨ π = 0π))) |
87 | 83, 86 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π
) β Β¬ ((Xp
βf β (β Γ {π§})) = 0π β¨ π =
0π)) |
88 | | neanior 3038 |
. . . . . . . . . . . . . . . 16
β’
(((Xp βf β (β Γ
{π§})) β
0π β§ π β 0π) β Β¬
((Xp βf β (β Γ {π§})) = 0π β¨
π =
0π)) |
89 | 87, 88 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β ((Xp
βf β (β Γ {π§})) β 0π β§ π β
0π)) |
90 | 89 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β π β
0π) |
91 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (β‘π β {0}) = (β‘π β {0}) |
92 | 91 | fta1 25684 |
. . . . . . . . . . . . . 14
β’ ((π β (Polyββ)
β§ π β
0π) β ((β‘π β {0}) β Fin β§
(β―β(β‘π β {0})) β€ (degβπ))) |
93 | 32, 90, 92 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β ((β‘π β {0}) β Fin β§
(β―β(β‘π β {0})) β€ (degβπ))) |
94 | 93 | simprd 497 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β (β―β(β‘π β {0})) β€ (degβπ)) |
95 | 94, 31 | breqtrrd 5138 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (β―β(β‘π β {0})) β€ π·) |
96 | | snfi 8995 |
. . . . . . . . . . . . . 14
β’ {π§} β Fin |
97 | 93 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (β‘π β {0}) β Fin) |
98 | | hashun2 14290 |
. . . . . . . . . . . . . 14
β’ (({π§} β Fin β§ (β‘π β {0}) β Fin) β
(β―β({π§} βͺ
(β‘π β {0}))) β€ ((β―β{π§}) + (β―β(β‘π β {0})))) |
99 | 96, 97, 98 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β (β―β({π§} βͺ (β‘π β {0}))) β€ ((β―β{π§}) + (β―β(β‘π β {0})))) |
100 | | ax-1cn 11116 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
101 | 3 | nncnd 12176 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β β) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β π· β β) |
103 | | addcom 11348 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ π·
β β) β (1 + π·) = (π· + 1)) |
104 | 100, 102,
103 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (1 + π·) = (π· + 1)) |
105 | 81, 104 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β (β―β({π§} βͺ (β‘π β {0}))) = (1 + π·)) |
106 | | hashsng 14276 |
. . . . . . . . . . . . . . 15
β’ (π§ β π
β (β―β{π§}) = 1) |
107 | 106 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (β―β{π§}) = 1) |
108 | 107 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β ((β―β{π§}) + (β―β(β‘π β {0}))) = (1 + (β―β(β‘π β {0})))) |
109 | 99, 105, 108 | 3brtr3d 5141 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β (1 + π·) β€ (1 + (β―β(β‘π β {0})))) |
110 | | hashcl 14263 |
. . . . . . . . . . . . . . 15
β’ ((β‘π β {0}) β Fin β
(β―β(β‘π β {0})) β
β0) |
111 | 97, 110 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (β―β(β‘π β {0})) β
β0) |
112 | 111 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β (β―β(β‘π β {0})) β
β) |
113 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β 1 β β) |
114 | 36, 112, 113 | leadd2d 11757 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β (π· β€ (β―β(β‘π β {0})) β (1 + π·) β€ (1 + (β―β(β‘π β {0}))))) |
115 | 109, 114 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β π· β€ (β―β(β‘π β {0}))) |
116 | 112, 36 | letri3d 11304 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β ((β―β(β‘π β {0})) = π· β ((β―β(β‘π β {0})) β€ π· β§ π· β€ (β―β(β‘π β {0}))))) |
117 | 95, 115, 116 | mpbir2and 712 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (β―β(β‘π β {0})) = π·) |
118 | 81, 117 | eqeq12d 2753 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β ((β―β({π§} βͺ (β‘π β {0}))) = (β―β(β‘π β {0})) β (π· + 1) = π·)) |
119 | 42, 118 | imbitrid 243 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β (π§ β (β‘π β {0}) β (π· + 1) = π·)) |
120 | 119 | necon3ad 2957 |
. . . . . . 7
β’ ((π β§ π§ β π
) β ((π· + 1) β π· β Β¬ π§ β (β‘π β {0}))) |
121 | 38, 120 | mpd 15 |
. . . . . 6
β’ ((π β§ π§ β π
) β Β¬ π§ β (β‘π β {0})) |
122 | | disjsn 4677 |
. . . . . 6
β’ (((β‘π β {0}) β© {π§}) = β
β Β¬ π§ β (β‘π β {0})) |
123 | 121, 122 | sylibr 233 |
. . . . 5
β’ ((π β§ π§ β π
) β ((β‘π β {0}) β© {π§}) = β
) |
124 | 26, 123 | eqtrid 2789 |
. . . 4
β’ ((π β§ π§ β π
) β ({π§} β© (β‘π β {0})) = β
) |
125 | 19 | adantr 482 |
. . . 4
β’ ((π β§ π§ β π
) β π
β Fin) |
126 | 49 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β π
) β π
β β) |
127 | 126 | sselda 3949 |
. . . 4
β’ (((π β§ π§ β π
) β§ π₯ β π
) β π₯ β β) |
128 | 124, 77, 125, 127 | fsumsplit 15633 |
. . 3
β’ ((π β§ π§ β π
) β Ξ£π₯ β π
π₯ = (Ξ£π₯ β {π§}π₯ + Ξ£π₯ β (β‘π β {0})π₯)) |
129 | | id 22 |
. . . . . . 7
β’ (π₯ = π§ β π₯ = π§) |
130 | 129 | sumsn 15638 |
. . . . . 6
β’ ((π§ β β β§ π§ β β) β
Ξ£π₯ β {π§}π₯ = π§) |
131 | 50, 50, 130 | syl2anc 585 |
. . . . 5
β’ ((π β§ π§ β π
) β Ξ£π₯ β {π§}π₯ = π§) |
132 | 50 | negnegd 11510 |
. . . . 5
β’ ((π β§ π§ β π
) β --π§ = π§) |
133 | 131, 132 | eqtr4d 2780 |
. . . 4
β’ ((π β§ π§ β π
) β Ξ£π₯ β {π§}π₯ = --π§) |
134 | 117, 31 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π§ β π
) β (β―β(β‘π β {0})) = (degβπ)) |
135 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (degβπ) = (degβπ)) |
136 | 135 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = π β (π· = (degβπ) β π· = (degβπ))) |
137 | | cnveq 5834 |
. . . . . . . . . . . 12
β’ (π = π β β‘π = β‘π) |
138 | 137 | imaeq1d 6017 |
. . . . . . . . . . 11
β’ (π = π β (β‘π β {0}) = (β‘π β {0})) |
139 | 138 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β (β―β(β‘π β {0})) = (β―β(β‘π β {0}))) |
140 | 139, 135 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π = π β ((β―β(β‘π β {0})) = (degβπ) β (β―β(β‘π β {0})) = (degβπ))) |
141 | 136, 140 | anbi12d 632 |
. . . . . . . 8
β’ (π = π β ((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β (π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)))) |
142 | 138 | sumeq1d 15593 |
. . . . . . . . 9
β’ (π = π β Ξ£π₯ β (β‘π β {0})π₯ = Ξ£π₯ β (β‘π β {0})π₯) |
143 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (coeffβπ) = (coeffβπ)) |
144 | 135 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π = π β ((degβπ) β 1) = ((degβπ) β 1)) |
145 | 143, 144 | fveq12d 6854 |
. . . . . . . . . . 11
β’ (π = π β ((coeffβπ)β((degβπ) β 1)) = ((coeffβπ)β((degβπ) β 1))) |
146 | 143, 135 | fveq12d 6854 |
. . . . . . . . . . 11
β’ (π = π β ((coeffβπ)β(degβπ)) = ((coeffβπ)β(degβπ))) |
147 | 145, 146 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β (((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))) = (((coeffβπ)β((degβπ) β 1)) /
((coeffβπ)β(degβπ)))) |
148 | 147 | negeqd 11402 |
. . . . . . . . 9
β’ (π = π β -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))) = -(((coeffβπ)β((degβπ) β 1)) /
((coeffβπ)β(degβπ)))) |
149 | 142, 148 | eqeq12d 2753 |
. . . . . . . 8
β’ (π = π β (Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))))) |
150 | 141, 149 | imbi12d 345 |
. . . . . . 7
β’ (π = π β (((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ)))) β ((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ)))))) |
151 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β π
) β βπ β (Polyββ)((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))))) |
152 | 150, 151,
32 | rspcdva 3585 |
. . . . . 6
β’ ((π β§ π§ β π
) β ((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))))) |
153 | 31, 134, 152 | mp2and 698 |
. . . . 5
β’ ((π β§ π§ β π
) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ)))) |
154 | 31 | fvoveq1d 7384 |
. . . . . . 7
β’ ((π β§ π§ β π
) β ((coeffβπ)β(π· β 1)) = ((coeffβπ)β((degβπ) β 1))) |
155 | 61 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (coeffβπΉ) = (coeffβ((Xp
βf β (β Γ {π§})) βf Β· π))) |
156 | 27, 155 | eqtrid 2789 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β π΄ = (coeffβ((Xp
βf β (β Γ {π§})) βf Β· π))) |
157 | 61 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (degβπΉ) = (degβ((Xp
βf β (β Γ {π§})) βf Β· π))) |
158 | 67 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (degβ(Xp
βf β (β Γ {π§}))) = 1) |
159 | | ax-1ne0 11127 |
. . . . . . . . . . . . . . 15
β’ 1 β
0 |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β 1 β 0) |
161 | 158, 160 | eqnetrd 3012 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β (degβ(Xp
βf β (β Γ {π§}))) β 0) |
162 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’
((Xp βf β (β Γ
{π§})) =
0π β (degβ(Xp
βf β (β Γ {π§}))) =
(degβ0π)) |
163 | 162, 12 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’
((Xp βf β (β Γ
{π§})) =
0π β (degβ(Xp
βf β (β Γ {π§}))) = 0) |
164 | 163 | necon3i 2977 |
. . . . . . . . . . . . 13
β’
((degβ(Xp βf β (β
Γ {π§}))) β 0
β (Xp βf β (β Γ
{π§})) β
0π) |
165 | 161, 164 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β (Xp
βf β (β Γ {π§})) β
0π) |
166 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(degβ(Xp βf β (β
Γ {π§}))) =
(degβ(Xp βf β (β Γ
{π§}))) |
167 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(degβπ) =
(degβπ) |
168 | 166, 167 | dgrmul 25647 |
. . . . . . . . . . . 12
β’
((((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ (Xp βf β
(β Γ {π§})) β
0π) β§ (π β (Polyββ) β§ π β 0π))
β (degβ((Xp βf β (β
Γ {π§}))
βf Β· π)) = ((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) |
169 | 68, 165, 32, 90, 168 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (degβ((Xp
βf β (β Γ {π§})) βf Β· π)) =
((degβ(Xp βf β (β Γ
{π§}))) + (degβπ))) |
170 | 157, 169 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (degβπΉ) = ((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) |
171 | 9, 170 | eqtrid 2789 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β π = ((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) |
172 | 156, 171 | fveq12d 6854 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β (π΄βπ) = ((coeffβ((Xp
βf β (β Γ {π§})) βf Β· π))β((degβ(Xp
βf β (β Γ {π§}))) + (degβπ)))) |
173 | | eqid 2737 |
. . . . . . . . . 10
β’
(coeffβ(Xp βf β (β
Γ {π§}))) =
(coeffβ(Xp βf β (β Γ
{π§}))) |
174 | | eqid 2737 |
. . . . . . . . . 10
β’
(coeffβπ) =
(coeffβπ) |
175 | 173, 174,
166, 167 | coemulhi 25631 |
. . . . . . . . 9
β’
(((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ π β (Polyββ)) β
((coeffβ((Xp βf β (β
Γ {π§}))
βf Β· π))β((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) = (((coeffβ(Xp
βf β (β Γ {π§})))β(degβ(Xp
βf β (β Γ {π§})))) Β· ((coeffβπ)β(degβπ)))) |
176 | 68, 32, 175 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β
((coeffβ((Xp βf β (β
Γ {π§}))
βf Β· π))β((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) = (((coeffβ(Xp
βf β (β Γ {π§})))β(degβ(Xp
βf β (β Γ {π§})))) Β· ((coeffβπ)β(degβπ)))) |
177 | 158 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β ((coeffβ(Xp
βf β (β Γ {π§})))β(degβ(Xp
βf β (β Γ {π§})))) = ((coeffβ(Xp
βf β (β Γ {π§})))β1)) |
178 | | ssid 3971 |
. . . . . . . . . . . . . . 15
β’ β
β β |
179 | | plyid 25586 |
. . . . . . . . . . . . . . 15
β’ ((β
β β β§ 1 β β) β Xp β
(Polyββ)) |
180 | 178, 100,
179 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
Xp β (Polyββ) |
181 | | plyconst 25583 |
. . . . . . . . . . . . . . 15
β’ ((β
β β β§ π§
β β) β (β Γ {π§}) β
(Polyββ)) |
182 | 178, 50, 181 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (β Γ {π§}) β
(Polyββ)) |
183 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(coeffβXp) =
(coeffβXp) |
184 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(coeffβ(β Γ {π§})) = (coeffβ(β Γ {π§})) |
185 | 183, 184 | coesub 25634 |
. . . . . . . . . . . . . 14
β’
((Xp β (Polyββ) β§ (β
Γ {π§}) β
(Polyββ)) β (coeffβ(Xp
βf β (β Γ {π§}))) = ((coeffβXp)
βf β (coeffβ(β Γ {π§})))) |
186 | 180, 182,
185 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β (coeffβ(Xp
βf β (β Γ {π§}))) = ((coeffβXp)
βf β (coeffβ(β Γ {π§})))) |
187 | 186 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β ((coeffβ(Xp
βf β (β Γ {π§})))β1) =
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β1)) |
188 | | 1nn0 12436 |
. . . . . . . . . . . . . 14
β’ 1 β
β0 |
189 | 183 | coef3 25609 |
. . . . . . . . . . . . . . . . 17
β’
(Xp β (Polyββ) β
(coeffβXp):β0βΆβ) |
190 | | ffn 6673 |
. . . . . . . . . . . . . . . . 17
β’
((coeffβXp):β0βΆβ
β (coeffβXp) Fn
β0) |
191 | 180, 189,
190 | mp2b 10 |
. . . . . . . . . . . . . . . 16
β’
(coeffβXp) Fn
β0 |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β (coeffβXp)
Fn β0) |
193 | 184 | coef3 25609 |
. . . . . . . . . . . . . . . 16
β’ ((β
Γ {π§}) β
(Polyββ) β (coeffβ(β Γ {π§})):β0βΆβ) |
194 | | ffn 6673 |
. . . . . . . . . . . . . . . 16
β’
((coeffβ(β Γ {π§})):β0βΆβ β
(coeffβ(β Γ {π§})) Fn β0) |
195 | 182, 193,
194 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β (coeffβ(β Γ
{π§})) Fn
β0) |
196 | | nn0ex 12426 |
. . . . . . . . . . . . . . . 16
β’
β0 β V |
197 | 196 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β β0 β
V) |
198 | | inidm 4183 |
. . . . . . . . . . . . . . 15
β’
(β0 β© β0) =
β0 |
199 | | coeidp 25640 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β0 β ((coeffβXp)β1) = if(1
= 1, 1, 0)) |
200 | 199 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π
) β§ 1 β β0) β
((coeffβXp)β1) = if(1 = 1, 1,
0)) |
201 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ 1 =
1 |
202 | 201 | iftruei 4498 |
. . . . . . . . . . . . . . . 16
β’ if(1 = 1,
1, 0) = 1 |
203 | 200, 202 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β π
) β§ 1 β β0) β
((coeffβXp)β1) = 1) |
204 | | 0lt1 11684 |
. . . . . . . . . . . . . . . . . 18
β’ 0 <
1 |
205 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
206 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
207 | 205, 206 | ltnlei 11283 |
. . . . . . . . . . . . . . . . . 18
β’ (0 < 1
β Β¬ 1 β€ 0) |
208 | 204, 207 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’ Β¬ 1
β€ 0 |
209 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β π
) β§ 1 β β0) β
π§ β
β) |
210 | | 0dgr 25622 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β β β
(degβ(β Γ {π§})) = 0) |
211 | 209, 210 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β π
) β§ 1 β β0) β
(degβ(β Γ {π§})) = 0) |
212 | 211 | breq2d 5122 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π
) β§ 1 β β0) β
(1 β€ (degβ(β Γ {π§})) β 1 β€ 0)) |
213 | 208, 212 | mtbiri 327 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π
) β§ 1 β β0) β
Β¬ 1 β€ (degβ(β Γ {π§}))) |
214 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(degβ(β Γ {π§})) = (degβ(β Γ {π§})) |
215 | 184, 214 | dgrub 25611 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β Γ {π§}) β (Polyββ) β§ 1 β
β0 β§ ((coeffβ(β Γ {π§}))β1) β 0) β 1 β€
(degβ(β Γ {π§}))) |
216 | 215 | 3expia 1122 |
. . . . . . . . . . . . . . . . . 18
β’
(((β Γ {π§}) β (Polyββ) β§ 1 β
β0) β (((coeffβ(β Γ {π§}))β1) β 0 β 1 β€
(degβ(β Γ {π§})))) |
217 | 182, 216 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π
) β§ 1 β β0) β
(((coeffβ(β Γ {π§}))β1) β 0 β 1 β€
(degβ(β Γ {π§})))) |
218 | 217 | necon1bd 2962 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π
) β§ 1 β β0) β
(Β¬ 1 β€ (degβ(β Γ {π§})) β ((coeffβ(β Γ
{π§}))β1) =
0)) |
219 | 213, 218 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β π
) β§ 1 β β0) β
((coeffβ(β Γ {π§}))β1) = 0) |
220 | 192, 195,
197, 197, 198, 203, 219 | ofval 7633 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π
) β§ 1 β β0) β
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β1) = (1 β
0)) |
221 | 188, 220 | mpan2 690 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β1) = (1 β
0)) |
222 | | 1m0e1 12281 |
. . . . . . . . . . . . 13
β’ (1
β 0) = 1 |
223 | 221, 222 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β1) = 1) |
224 | 187, 223 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β ((coeffβ(Xp
βf β (β Γ {π§})))β1) = 1) |
225 | 177, 224 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β ((coeffβ(Xp
βf β (β Γ {π§})))β(degβ(Xp
βf β (β Γ {π§})))) = 1) |
226 | 225 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β
(((coeffβ(Xp βf β (β
Γ {π§})))β(degβ(Xp
βf β (β Γ {π§})))) Β· ((coeffβπ)β(degβπ))) = (1 Β·
((coeffβπ)β(degβπ)))) |
227 | 174 | coef3 25609 |
. . . . . . . . . . . 12
β’ (π β (Polyββ)
β (coeffβπ):β0βΆβ) |
228 | 32, 227 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (coeffβπ):β0βΆβ) |
229 | 228, 34 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β ((coeffβπ)β(degβπ)) β β) |
230 | 229 | mulid2d 11180 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β (1 Β· ((coeffβπ)β(degβπ))) = ((coeffβπ)β(degβπ))) |
231 | 226, 230 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β
(((coeffβ(Xp βf β (β
Γ {π§})))β(degβ(Xp
βf β (β Γ {π§})))) Β· ((coeffβπ)β(degβπ))) = ((coeffβπ)β(degβπ))) |
232 | 172, 176,
231 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π§ β π
) β (π΄βπ) = ((coeffβπ)β(degβπ))) |
233 | 154, 232 | oveq12d 7380 |
. . . . . 6
β’ ((π β§ π§ β π
) β (((coeffβπ)β(π· β 1)) / (π΄βπ)) = (((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ)))) |
234 | 233 | negeqd 11402 |
. . . . 5
β’ ((π β§ π§ β π
) β -(((coeffβπ)β(π· β 1)) / (π΄βπ)) = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ)))) |
235 | 153, 234 | eqtr4d 2780 |
. . . 4
β’ ((π β§ π§ β π
) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β(π· β 1)) / (π΄βπ))) |
236 | 133, 235 | oveq12d 7380 |
. . 3
β’ ((π β§ π§ β π
) β (Ξ£π₯ β {π§}π₯ + Ξ£π₯ β (β‘π β {0})π₯) = (--π§ + -(((coeffβπ)β(π· β 1)) / (π΄βπ)))) |
237 | 50 | negcld 11506 |
. . . . 5
β’ ((π β§ π§ β π
) β -π§ β β) |
238 | | nnm1nn0 12461 |
. . . . . . . . 9
β’ (π· β β β (π· β 1) β
β0) |
239 | 3, 238 | syl 17 |
. . . . . . . 8
β’ (π β (π· β 1) β
β0) |
240 | 239 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β π
) β (π· β 1) β
β0) |
241 | 228, 240 | ffvelcdmd 7041 |
. . . . . 6
β’ ((π β§ π§ β π
) β ((coeffβπ)β(π· β 1)) β
β) |
242 | 232, 229 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π§ β π
) β (π΄βπ) β β) |
243 | 9, 27 | dgreq0 25642 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β (πΉ = 0π β (π΄βπ) = 0)) |
244 | 43, 243 | syl 17 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β (πΉ = 0π β (π΄βπ) = 0)) |
245 | 244 | necon3bid 2989 |
. . . . . . 7
β’ ((π β§ π§ β π
) β (πΉ β 0π β (π΄βπ) β 0)) |
246 | 82, 245 | mpbid 231 |
. . . . . 6
β’ ((π β§ π§ β π
) β (π΄βπ) β 0) |
247 | 241, 242,
246 | divcld 11938 |
. . . . 5
β’ ((π β§ π§ β π
) β (((coeffβπ)β(π· β 1)) / (π΄βπ)) β β) |
248 | 237, 247 | negdid 11532 |
. . . 4
β’ ((π β§ π§ β π
) β -(-π§ + (((coeffβπ)β(π· β 1)) / (π΄βπ))) = (--π§ + -(((coeffβπ)β(π· β 1)) / (π΄βπ)))) |
249 | 237, 242 | mulcld 11182 |
. . . . . . 7
β’ ((π β§ π§ β π
) β (-π§ Β· (π΄βπ)) β β) |
250 | 249, 241,
242, 246 | divdird 11976 |
. . . . . 6
β’ ((π β§ π§ β π
) β (((-π§ Β· (π΄βπ)) + ((coeffβπ)β(π· β 1))) / (π΄βπ)) = (((-π§ Β· (π΄βπ)) / (π΄βπ)) + (((coeffβπ)β(π· β 1)) / (π΄βπ)))) |
251 | | nnm1nn0 12461 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β0) |
252 | 5, 251 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β 1) β
β0) |
253 | 252 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β (π β 1) β
β0) |
254 | 173, 174 | coemul 25629 |
. . . . . . . . 9
β’
(((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ π β (Polyββ) β§ (π β 1) β
β0) β ((coeffβ((Xp
βf β (β Γ {π§})) βf Β· π))β(π β 1)) = Ξ£π β (0...(π β
1))(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π)))) |
255 | 68, 32, 253, 254 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β
((coeffβ((Xp βf β (β
Γ {π§}))
βf Β· π))β(π β 1)) = Ξ£π β (0...(π β
1))(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π)))) |
256 | 156 | fveq1d 6849 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β (π΄β(π β 1)) =
((coeffβ((Xp βf β (β
Γ {π§}))
βf Β· π))β(π β 1))) |
257 | | 1e0p1 12667 |
. . . . . . . . . . . 12
β’ 1 = (0 +
1) |
258 | 257 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (0...1) =
(0...(0 + 1)) |
259 | 258 | sumeq1i 15590 |
. . . . . . . . . 10
β’
Ξ£π β
(0...1)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = Ξ£π β (0...(0 +
1))(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) |
260 | | 0nn0 12435 |
. . . . . . . . . . . . 13
β’ 0 β
β0 |
261 | | nn0uz 12812 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
262 | 260, 261 | eleqtri 2836 |
. . . . . . . . . . . 12
β’ 0 β
(β€β₯β0) |
263 | 262 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β 0 β
(β€β₯β0)) |
264 | 258 | eleq2i 2830 |
. . . . . . . . . . . 12
β’ (π β (0...1) β π β (0...(0 +
1))) |
265 | 173 | coef3 25609 |
. . . . . . . . . . . . . . 15
β’
((Xp βf β (β Γ
{π§})) β
(Polyββ) β (coeffβ(Xp
βf β (β Γ {π§}))):β0βΆβ) |
266 | 68, 265 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β (coeffβ(Xp
βf β (β Γ {π§}))):β0βΆβ) |
267 | | elfznn0 13541 |
. . . . . . . . . . . . . 14
β’ (π β (0...1) β π β
β0) |
268 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’
(((coeffβ(Xp βf β
(β Γ {π§}))):β0βΆβ β§
π β
β0) β ((coeffβ(Xp
βf β (β Γ {π§})))βπ) β β) |
269 | 266, 267,
268 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π
) β§ π β (0...1)) β
((coeffβ(Xp βf β (β
Γ {π§})))βπ) β
β) |
270 | 2 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π· + 1) β 1) = (π β 1)) |
271 | | pncan 11414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β β β§ 1 β
β) β ((π· + 1)
β 1) = π·) |
272 | 101, 100,
271 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π· + 1) β 1) = π·) |
273 | 270, 272 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β 1) = π·) |
274 | 273 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β (π β 1) = π·) |
275 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π
) β π· β β) |
276 | 274, 275 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β (π β 1) β β) |
277 | | nnuz 12813 |
. . . . . . . . . . . . . . . . 17
β’ β =
(β€β₯β1) |
278 | 276, 277 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π
) β (π β 1) β
(β€β₯β1)) |
279 | | fzss2 13488 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β
(β€β₯β1) β (0...1) β (0...(π β 1))) |
280 | 278, 279 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β (0...1) β (0...(π β 1))) |
281 | 280 | sselda 3949 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π
) β§ π β (0...1)) β π β (0...(π β 1))) |
282 | | fznn0sub 13480 |
. . . . . . . . . . . . . . 15
β’ (π β (0...(π β 1)) β ((π β 1) β π) β
β0) |
283 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . 15
β’
(((coeffβπ):β0βΆβ β§
((π β 1) β
π) β
β0) β ((coeffβπ)β((π β 1) β π)) β β) |
284 | 228, 282,
283 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π
) β§ π β (0...(π β 1))) β ((coeffβπ)β((π β 1) β π)) β β) |
285 | 281, 284 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π
) β§ π β (0...1)) β ((coeffβπ)β((π β 1) β π)) β β) |
286 | 269, 285 | mulcld 11182 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π
) β§ π β (0...1)) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) β β) |
287 | 264, 286 | sylan2br 596 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π
) β§ π β (0...(0 + 1))) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) β β) |
288 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = (0 + 1) β π = (0 + 1)) |
289 | 288, 257 | eqtr4di 2795 |
. . . . . . . . . . . . 13
β’ (π = (0 + 1) β π = 1) |
290 | 289 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = (0 + 1) β
((coeffβ(Xp βf β (β
Γ {π§})))βπ) =
((coeffβ(Xp βf β (β
Γ {π§})))β1)) |
291 | 289 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = (0 + 1) β ((π β 1) β π) = ((π β 1) β 1)) |
292 | 291 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = (0 + 1) β
((coeffβπ)β((π β 1) β π)) = ((coeffβπ)β((π β 1) β 1))) |
293 | 290, 292 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = (0 + 1) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (((coeffβ(Xp
βf β (β Γ {π§})))β1) Β· ((coeffβπ)β((π β 1) β 1)))) |
294 | 263, 287,
293 | fsump1 15648 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β Ξ£π β (0...(0 +
1))(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (Ξ£π β
(0...0)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) + (((coeffβ(Xp
βf β (β Γ {π§})))β1) Β· ((coeffβπ)β((π β 1) β 1))))) |
295 | 259, 294 | eqtrid 2789 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β Ξ£π β
(0...1)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (Ξ£π β
(0...0)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) + (((coeffβ(Xp
βf β (β Γ {π§})))β1) Β· ((coeffβπ)β((π β 1) β 1))))) |
296 | | eldifn 4092 |
. . . . . . . . . . . . . 14
β’ (π β ((0...(π β 1)) β (0...1)) β Β¬
π β
(0...1)) |
297 | 296 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β Β¬
π β
(0...1)) |
298 | | eldifi 4091 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((0...(π β 1)) β (0...1)) β π β (0...(π β 1))) |
299 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(π β 1)) β π β β0) |
300 | 298, 299 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β ((0...(π β 1)) β (0...1)) β π β
β0) |
301 | 173, 166 | dgrub 25611 |
. . . . . . . . . . . . . . . . 17
β’
(((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ π β β0 β§
((coeffβ(Xp βf β (β
Γ {π§})))βπ) β 0) β π β€
(degβ(Xp βf β (β Γ
{π§})))) |
302 | 301 | 3expia 1122 |
. . . . . . . . . . . . . . . 16
β’
(((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ π β β0) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) β 0 β π β€
(degβ(Xp βf β (β Γ
{π§}))))) |
303 | 68, 300, 302 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) β 0 β π β€
(degβ(Xp βf β (β Γ
{π§}))))) |
304 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...(π β 1)) β π β
(β€β₯β0)) |
305 | 298, 304 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((0...(π β 1)) β (0...1)) β π β
(β€β₯β0)) |
306 | 305 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β π β
(β€β₯β0)) |
307 | | 1z 12540 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β€ |
308 | | elfz5 13440 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β0) β§ 1 β β€) β (π β (0...1) β π β€ 1)) |
309 | 306, 307,
308 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β (π β (0...1) β π β€ 1)) |
310 | 158 | breq2d 5122 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β (π β€ (degβ(Xp
βf β (β Γ {π§}))) β π β€ 1)) |
311 | 310 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β (π β€
(degβ(Xp βf β (β Γ
{π§}))) β π β€ 1)) |
312 | 309, 311 | bitr4d 282 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β (π β (0...1) β π β€
(degβ(Xp βf β (β Γ
{π§}))))) |
313 | 303, 312 | sylibrd 259 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) β 0 β π β
(0...1))) |
314 | 313 | necon1bd 2962 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β (Β¬
π β (0...1) β
((coeffβ(Xp βf β (β
Γ {π§})))βπ) = 0)) |
315 | 297, 314 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β
((coeffβ(Xp βf β (β
Γ {π§})))βπ) = 0) |
316 | 315 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (0 Β· ((coeffβπ)β((π β 1) β π)))) |
317 | 298, 284 | sylan2 594 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β
((coeffβπ)β((π β 1) β π)) β β) |
318 | 317 | mul02d 11360 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β (0
Β· ((coeffβπ)β((π β 1) β π))) = 0) |
319 | 316, 318 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π§ β π
) β§ π β ((0...(π β 1)) β (0...1))) β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = 0) |
320 | | fzfid 13885 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (0...(π β 1)) β Fin) |
321 | 280, 286,
319, 320 | fsumss 15617 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β Ξ£π β
(0...1)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = Ξ£π β (0...(π β
1))(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π)))) |
322 | | 0z 12517 |
. . . . . . . . . . . 12
β’ 0 β
β€ |
323 | 186 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β ((coeffβ(Xp
βf β (β Γ {π§})))β0) =
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β0)) |
324 | | coeidp 25640 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 β
β0 β ((coeffβXp)β0) = if(0
= 1, 1, 0)) |
325 | 159 | nesymi 3002 |
. . . . . . . . . . . . . . . . . . . . 21
β’ Β¬ 0
= 1 |
326 | 325 | iffalsei 4501 |
. . . . . . . . . . . . . . . . . . . 20
β’ if(0 = 1,
1, 0) = 0 |
327 | 324, 326 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
β’ (0 β
β0 β ((coeffβXp)β0) =
0) |
328 | 327 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β π
) β§ 0 β β0) β
((coeffβXp)β0) = 0) |
329 | 184 | coefv0 25625 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β
Γ {π§}) β
(Polyββ) β ((β Γ {π§})β0) = ((coeffβ(β Γ
{π§}))β0)) |
330 | 182, 329 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β π
) β ((β Γ {π§})β0) =
((coeffβ(β Γ {π§}))β0)) |
331 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
β |
332 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π§ β V |
333 | 332 | fvconst2 7158 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β
β β ((β Γ {π§})β0) = π§) |
334 | 331, 333 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β
Γ {π§})β0) =
π§ |
335 | 330, 334 | eqtr3di 2792 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β π
) β ((coeffβ(β Γ
{π§}))β0) = π§) |
336 | 335 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β π
) β§ 0 β β0) β
((coeffβ(β Γ {π§}))β0) = π§) |
337 | 192, 195,
197, 197, 198, 328, 336 | ofval 7633 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π
) β§ 0 β β0) β
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β0) = (0 β π§)) |
338 | 260, 337 | mpan2 690 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π
) β
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β0) = (0 β π§)) |
339 | | df-neg 11395 |
. . . . . . . . . . . . . . . 16
β’ -π§ = (0 β π§) |
340 | 338, 339 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β
(((coeffβXp) βf β
(coeffβ(β Γ {π§})))β0) = -π§) |
341 | 323, 340 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β ((coeffβ(Xp
βf β (β Γ {π§})))β0) = -π§) |
342 | 274 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β ((π β 1) β 0) = (π· β 0)) |
343 | 102 | subid1d 11508 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π
) β (π· β 0) = π·) |
344 | 342, 343,
31 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π
) β ((π β 1) β 0) = (degβπ)) |
345 | 344 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π
) β ((coeffβπ)β((π β 1) β 0)) =
((coeffβπ)β(degβπ))) |
346 | 345, 232 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π
) β ((coeffβπ)β((π β 1) β 0)) = (π΄βπ)) |
347 | 341, 346 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π
) β
(((coeffβ(Xp βf β (β
Γ {π§})))β0)
Β· ((coeffβπ)β((π β 1) β 0))) = (-π§ Β· (π΄βπ))) |
348 | 347, 249 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β
(((coeffβ(Xp βf β (β
Γ {π§})))β0)
Β· ((coeffβπ)β((π β 1) β 0))) β
β) |
349 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 0 β
((coeffβ(Xp βf β (β
Γ {π§})))βπ) =
((coeffβ(Xp βf β (β
Γ {π§})))β0)) |
350 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β ((π β 1) β π) = ((π β 1) β 0)) |
351 | 350 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = 0 β ((coeffβπ)β((π β 1) β π)) = ((coeffβπ)β((π β 1) β 0))) |
352 | 349, 351 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π = 0 β
(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (((coeffβ(Xp
βf β (β Γ {π§})))β0) Β· ((coeffβπ)β((π β 1) β 0)))) |
353 | 352 | fsum1 15639 |
. . . . . . . . . . . 12
β’ ((0
β β€ β§ (((coeffβ(Xp βf
β (β Γ {π§})))β0) Β· ((coeffβπ)β((π β 1) β 0))) β β)
β Ξ£π β
(0...0)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (((coeffβ(Xp
βf β (β Γ {π§})))β0) Β· ((coeffβπ)β((π β 1) β 0)))) |
354 | 322, 348,
353 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β Ξ£π β
(0...0)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (((coeffβ(Xp
βf β (β Γ {π§})))β0) Β· ((coeffβπ)β((π β 1) β 0)))) |
355 | 354, 347 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β Ξ£π β
(0...0)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) = (-π§ Β· (π΄βπ))) |
356 | 274 | fvoveq1d 7384 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π
) β ((coeffβπ)β((π β 1) β 1)) =
((coeffβπ)β(π· β 1))) |
357 | 224, 356 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β
(((coeffβ(Xp βf β (β
Γ {π§})))β1)
Β· ((coeffβπ)β((π β 1) β 1))) = (1 Β·
((coeffβπ)β(π· β 1)))) |
358 | 241 | mulid2d 11180 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π
) β (1 Β· ((coeffβπ)β(π· β 1))) = ((coeffβπ)β(π· β 1))) |
359 | 357, 358 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β
(((coeffβ(Xp βf β (β
Γ {π§})))β1)
Β· ((coeffβπ)β((π β 1) β 1))) =
((coeffβπ)β(π· β 1))) |
360 | 355, 359 | oveq12d 7380 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β (Ξ£π β
(0...0)(((coeffβ(Xp βf β
(β Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π))) + (((coeffβ(Xp
βf β (β Γ {π§})))β1) Β· ((coeffβπ)β((π β 1) β 1)))) = ((-π§ Β· (π΄βπ)) + ((coeffβπ)β(π· β 1)))) |
361 | 295, 321,
360 | 3eqtr3rd 2786 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β ((-π§ Β· (π΄βπ)) + ((coeffβπ)β(π· β 1))) = Ξ£π β (0...(π β
1))(((coeffβ(Xp βf β (β
Γ {π§})))βπ) Β· ((coeffβπ)β((π β 1) β π)))) |
362 | 255, 256,
361 | 3eqtr4rd 2788 |
. . . . . . 7
β’ ((π β§ π§ β π
) β ((-π§ Β· (π΄βπ)) + ((coeffβπ)β(π· β 1))) = (π΄β(π β 1))) |
363 | 362 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π§ β π
) β (((-π§ Β· (π΄βπ)) + ((coeffβπ)β(π· β 1))) / (π΄βπ)) = ((π΄β(π β 1)) / (π΄βπ))) |
364 | 237, 242,
246 | divcan4d 11944 |
. . . . . . 7
β’ ((π β§ π§ β π
) β ((-π§ Β· (π΄βπ)) / (π΄βπ)) = -π§) |
365 | 364 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π§ β π
) β (((-π§ Β· (π΄βπ)) / (π΄βπ)) + (((coeffβπ)β(π· β 1)) / (π΄βπ))) = (-π§ + (((coeffβπ)β(π· β 1)) / (π΄βπ)))) |
366 | 250, 363,
365 | 3eqtr3rd 2786 |
. . . . 5
β’ ((π β§ π§ β π
) β (-π§ + (((coeffβπ)β(π· β 1)) / (π΄βπ))) = ((π΄β(π β 1)) / (π΄βπ))) |
367 | 366 | negeqd 11402 |
. . . 4
β’ ((π β§ π§ β π
) β -(-π§ + (((coeffβπ)β(π· β 1)) / (π΄βπ))) = -((π΄β(π β 1)) / (π΄βπ))) |
368 | 248, 367 | eqtr3d 2779 |
. . 3
β’ ((π β§ π§ β π
) β (--π§ + -(((coeffβπ)β(π· β 1)) / (π΄βπ))) = -((π΄β(π β 1)) / (π΄βπ))) |
369 | 128, 236,
368 | 3eqtrd 2781 |
. 2
β’ ((π β§ π§ β π
) β Ξ£π₯ β π
π₯ = -((π΄β(π β 1)) / (π΄βπ))) |
370 | 25, 369 | exlimddv 1939 |
1
β’ (π β Ξ£π₯ β π
π₯ = -((π΄β(π β 1)) / (π΄βπ))) |