Step | Hyp | Ref
| Expression |
1 | | vieta1.5 |
. 2
โข (๐ โ (โฏโ๐
) = ๐) |
2 | | fveq2 6846 |
. . . . . . 7
โข (๐ = ๐น โ (degโ๐) = (degโ๐น)) |
3 | 2 | eqeq2d 2744 |
. . . . . 6
โข (๐ = ๐น โ (๐ = (degโ๐) โ ๐ = (degโ๐น))) |
4 | | cnveq 5833 |
. . . . . . . . . 10
โข (๐ = ๐น โ โก๐ = โก๐น) |
5 | 4 | imaeq1d 6016 |
. . . . . . . . 9
โข (๐ = ๐น โ (โก๐ โ {0}) = (โก๐น โ {0})) |
6 | | vieta1.3 |
. . . . . . . . 9
โข ๐
= (โก๐น โ {0}) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ = ๐น โ (โก๐ โ {0}) = ๐
) |
8 | 7 | fveq2d 6850 |
. . . . . . 7
โข (๐ = ๐น โ (โฏโ(โก๐ โ {0})) = (โฏโ๐
)) |
9 | | vieta1.2 |
. . . . . . . 8
โข ๐ = (degโ๐น) |
10 | 2, 9 | eqtr4di 2791 |
. . . . . . 7
โข (๐ = ๐น โ (degโ๐) = ๐) |
11 | 8, 10 | eqeq12d 2749 |
. . . . . 6
โข (๐ = ๐น โ ((โฏโ(โก๐ โ {0})) = (degโ๐) โ (โฏโ๐
) = ๐)) |
12 | 3, 11 | anbi12d 632 |
. . . . 5
โข (๐ = ๐น โ ((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ (๐ = (degโ๐น) โง (โฏโ๐
) = ๐))) |
13 | 9 | biantrur 532 |
. . . . 5
โข
((โฏโ๐
) =
๐ โ (๐ = (degโ๐น) โง (โฏโ๐
) = ๐)) |
14 | 12, 13 | bitr4di 289 |
. . . 4
โข (๐ = ๐น โ ((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ (โฏโ๐
) = ๐)) |
15 | 7 | sumeq1d 15594 |
. . . . 5
โข (๐ = ๐น โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = ฮฃ๐ฅ โ ๐
๐ฅ) |
16 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = ๐น โ (coeffโ๐) = (coeffโ๐น)) |
17 | | vieta1.1 |
. . . . . . . . 9
โข ๐ด = (coeffโ๐น) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ = ๐น โ (coeffโ๐) = ๐ด) |
19 | 10 | oveq1d 7376 |
. . . . . . . 8
โข (๐ = ๐น โ ((degโ๐) โ 1) = (๐ โ 1)) |
20 | 18, 19 | fveq12d 6853 |
. . . . . . 7
โข (๐ = ๐น โ ((coeffโ๐)โ((degโ๐) โ 1)) = (๐ดโ(๐ โ 1))) |
21 | 18, 10 | fveq12d 6853 |
. . . . . . 7
โข (๐ = ๐น โ ((coeffโ๐)โ(degโ๐)) = (๐ดโ๐)) |
22 | 20, 21 | oveq12d 7379 |
. . . . . 6
โข (๐ = ๐น โ (((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) = ((๐ดโ(๐ โ 1)) / (๐ดโ๐))) |
23 | 22 | negeqd 11403 |
. . . . 5
โข (๐ = ๐น โ -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) = -((๐ดโ(๐ โ 1)) / (๐ดโ๐))) |
24 | 15, 23 | eqeq12d 2749 |
. . . 4
โข (๐ = ๐น โ (ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) โ ฮฃ๐ฅ โ ๐
๐ฅ = -((๐ดโ(๐ โ 1)) / (๐ดโ๐)))) |
25 | 14, 24 | imbi12d 345 |
. . 3
โข (๐ = ๐น โ (((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ
((โฏโ๐
) = ๐ โ ฮฃ๐ฅ โ ๐
๐ฅ = -((๐ดโ(๐ โ 1)) / (๐ดโ๐))))) |
26 | | vieta1.6 |
. . . 4
โข (๐ โ ๐ โ โ) |
27 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ฆ = 1 โ (๐ฆ = (degโ๐) โ 1 = (degโ๐))) |
28 | 27 | anbi1d 631 |
. . . . . . 7
โข (๐ฆ = 1 โ ((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ (1 = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)))) |
29 | 28 | imbi1d 342 |
. . . . . 6
โข (๐ฆ = 1 โ (((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ ((1 =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
30 | 29 | ralbidv 3171 |
. . . . 5
โข (๐ฆ = 1 โ (โ๐ โ
(Polyโโ)((๐ฆ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ (Polyโโ)((1
= (degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
31 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ฆ = ๐ โ (๐ฆ = (degโ๐) โ ๐ = (degโ๐))) |
32 | 31 | anbi1d 631 |
. . . . . . 7
โข (๐ฆ = ๐ โ ((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ (๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)))) |
33 | 32 | imbi1d 342 |
. . . . . 6
โข (๐ฆ = ๐ โ (((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ ((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
34 | 33 | ralbidv 3171 |
. . . . 5
โข (๐ฆ = ๐ โ (โ๐ โ (Polyโโ)((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
35 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ฆ = (๐ + 1) โ (๐ฆ = (degโ๐) โ (๐ + 1) = (degโ๐))) |
36 | 35 | anbi1d 631 |
. . . . . . 7
โข (๐ฆ = (๐ + 1) โ ((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)))) |
37 | 36 | imbi1d 342 |
. . . . . 6
โข (๐ฆ = (๐ + 1) โ (((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ (((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
38 | 37 | ralbidv 3171 |
. . . . 5
โข (๐ฆ = (๐ + 1) โ (โ๐ โ (Polyโโ)((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)(((๐ +
1) = (degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
39 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ฆ = ๐ โ (๐ฆ = (degโ๐) โ ๐ = (degโ๐))) |
40 | 39 | anbi1d 631 |
. . . . . . 7
โข (๐ฆ = ๐ โ ((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ (๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)))) |
41 | 40 | imbi1d 342 |
. . . . . 6
โข (๐ฆ = ๐ โ (((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ ((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
42 | 41 | ralbidv 3171 |
. . . . 5
โข (๐ฆ = ๐ โ (โ๐ โ (Polyโโ)((๐ฆ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
43 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข
(coeffโ๐) =
(coeffโ๐) |
44 | 43 | coef3 25616 |
. . . . . . . . . . . . . 14
โข (๐ โ (Polyโโ)
โ (coeffโ๐):โ0โถโ) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (coeffโ๐):โ0โถโ) |
46 | | 0nn0 12436 |
. . . . . . . . . . . . 13
โข 0 โ
โ0 |
47 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
โข
(((coeffโ๐):โ0โถโ โง 0
โ โ0) โ ((coeffโ๐)โ0) โ โ) |
48 | 45, 46, 47 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((coeffโ๐)โ0) โ โ) |
49 | | 1nn0 12437 |
. . . . . . . . . . . . 13
โข 1 โ
โ0 |
50 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
โข
(((coeffโ๐):โ0โถโ โง 1
โ โ0) โ ((coeffโ๐)โ1) โ โ) |
51 | 45, 49, 50 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((coeffโ๐)โ1) โ โ) |
52 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ 1 = (degโ๐)) |
53 | 52 | fveq2d 6850 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((coeffโ๐)โ1) = ((coeffโ๐)โ(degโ๐))) |
54 | | ax-1ne0 11128 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
0 |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ 1 โ 0) |
56 | 52, 55 | eqnetrrd 3009 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (degโ๐) โ
0) |
57 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 0๐ โ
(degโ๐) =
(degโ0๐)) |
58 | | dgr0 25646 |
. . . . . . . . . . . . . . . . 17
โข
(degโ0๐) = 0 |
59 | 57, 58 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
โข (๐ = 0๐ โ
(degโ๐) =
0) |
60 | 59 | necon3i 2973 |
. . . . . . . . . . . . . . 15
โข
((degโ๐) โ
0 โ ๐ โ
0๐) |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ๐ โ
0๐) |
62 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(degโ๐) =
(degโ๐) |
63 | 62, 43 | dgreq0 25649 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (Polyโโ)
โ (๐ =
0๐ โ ((coeffโ๐)โ(degโ๐)) = 0)) |
64 | 63 | necon3bid 2985 |
. . . . . . . . . . . . . . 15
โข (๐ โ (Polyโโ)
โ (๐ โ
0๐ โ ((coeffโ๐)โ(degโ๐)) โ 0)) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (๐ โ
0๐ โ ((coeffโ๐)โ(degโ๐)) โ 0)) |
66 | 61, 65 | mpbid 231 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((coeffโ๐)โ(degโ๐)) โ 0) |
67 | 53, 66 | eqnetrd 3008 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((coeffโ๐)โ1) โ 0) |
68 | 48, 51, 67 | divcld 11939 |
. . . . . . . . . . 11
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ) |
69 | 68 | negcld 11507 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ -(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ) |
70 | | id 22 |
. . . . . . . . . . 11
โข (๐ฅ = -(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ ๐ฅ = -(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) |
71 | 70 | sumsn 15639 |
. . . . . . . . . 10
โข
((-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ โง
-(((coeffโ๐)โ0)
/ ((coeffโ๐)โ1)) โ โ) โ
ฮฃ๐ฅ โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}๐ฅ = -(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) |
72 | 69, 69, 71 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ฮฃ๐ฅ โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}๐ฅ = -(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) |
73 | 72 | adantrr 716 |
. . . . . . . 8
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
ฮฃ๐ฅ โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}๐ฅ = -(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) |
74 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข (โก๐ โ {0}) = (โก๐ โ {0}) |
75 | 74 | fta1 25691 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง ๐ โ
0๐) โ ((โก๐ โ {0}) โ Fin โง
(โฏโ(โก๐ โ {0})) โค (degโ๐))) |
76 | 61, 75 | syldan 592 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((โก๐ โ {0}) โ Fin โง
(โฏโ(โก๐ โ {0})) โค (degโ๐))) |
77 | 76 | simpld 496 |
. . . . . . . . . . 11
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (โก๐ โ {0}) โ Fin) |
78 | 77 | adantrr 716 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
(โก๐ โ {0}) โ Fin) |
79 | 43, 62 | coeid2 25623 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (Polyโโ)
โง -(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ) โ (๐โ-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) = ฮฃ๐ โ (0...(degโ๐))(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐))) |
80 | 69, 79 | syldan 592 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (๐โ-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) = ฮฃ๐ โ (0...(degโ๐))(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐))) |
81 | 52 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (0...1) = (0...(degโ๐))) |
82 | 81 | sumeq1d 15594 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ฮฃ๐ โ
(0...1)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = ฮฃ๐ โ (0...(degโ๐))(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐))) |
83 | | nn0uz 12813 |
. . . . . . . . . . . . . . . 16
โข
โ0 = (โคโฅโ0) |
84 | | 1e0p1 12668 |
. . . . . . . . . . . . . . . 16
โข 1 = (0 +
1) |
85 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ ((coeffโ๐)โ๐) = ((coeffโ๐)โ1)) |
86 | | oveq2 7369 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐) = (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1)) |
87 | 85, 86 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = (((coeffโ๐)โ1) ยท
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1))) |
88 | 45 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โง ๐ โ
โ0) โ ((coeffโ๐)โ๐) โ โ) |
89 | | expcl 13994 |
. . . . . . . . . . . . . . . . . 18
โข
((-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ โง ๐ โ โ0)
โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐) โ โ) |
90 | 69, 89 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โง ๐ โ
โ0) โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐) โ โ) |
91 | 88, 90 | mulcld 11183 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โง ๐ โ
โ0) โ (((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) โ
โ) |
92 | | 0z 12518 |
. . . . . . . . . . . . . . . . . . 19
โข 0 โ
โค |
93 | 69 | exp0d 14054 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0) = 1) |
94 | 93 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0)) =
(((coeffโ๐)โ0)
ยท 1)) |
95 | 48 | mulid1d 11180 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) ยท 1) = ((coeffโ๐)โ0)) |
96 | 94, 95 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0)) =
((coeffโ๐)โ0)) |
97 | 96, 48 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0)) โ
โ) |
98 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = 0 โ ((coeffโ๐)โ๐) = ((coeffโ๐)โ0)) |
99 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = 0 โ
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐) = (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0)) |
100 | 98, 99 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = 0 โ (((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = (((coeffโ๐)โ0) ยท
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0))) |
101 | 100 | fsum1 15640 |
. . . . . . . . . . . . . . . . . . 19
โข ((0
โ โค โง (((coeffโ๐)โ0) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0)) โ
โ) โ ฮฃ๐
โ (0...0)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = (((coeffโ๐)โ0) ยท
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0))) |
102 | 92, 97, 101 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ฮฃ๐ โ
(0...0)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = (((coeffโ๐)โ0) ยท
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ0))) |
103 | 102, 96 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ฮฃ๐ โ
(0...0)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = ((coeffโ๐)โ0)) |
104 | 103, 46 | jctil 521 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (0 โ โ0 โง ฮฃ๐ โ (0...0)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = ((coeffโ๐)โ0))) |
105 | 69 | exp1d 14055 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1) = -(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) |
106 | 105 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ1) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1)) =
(((coeffโ๐)โ1)
ยท -(((coeffโ๐)โ0) / ((coeffโ๐)โ1)))) |
107 | 51, 68 | mulneg2d 11617 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ1) ยท -(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) =
-(((coeffโ๐)โ1)
ยท (((coeffโ๐)โ0) / ((coeffโ๐)โ1)))) |
108 | 48, 51, 67 | divcan2d 11941 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ1) ยท (((coeffโ๐)โ0) / ((coeffโ๐)โ1))) =
((coeffโ๐)โ0)) |
109 | 108 | negeqd 11403 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ -(((coeffโ๐)โ1) ยท (((coeffโ๐)โ0) / ((coeffโ๐)โ1))) =
-((coeffโ๐)โ0)) |
110 | 106, 107,
109 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ1) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1)) =
-((coeffโ๐)โ0)) |
111 | 110 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) + (((coeffโ๐)โ1) ยท
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1))) = (((coeffโ๐)โ0) +
-((coeffโ๐)โ0))) |
112 | 48 | negidd 11510 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) + -((coeffโ๐)โ0)) =
0) |
113 | 111, 112 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) + (((coeffโ๐)โ1) ยท
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ1))) = 0) |
114 | 83, 84, 87, 91, 104, 113 | fsump1i 15662 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (1 โ โ0 โง ฮฃ๐ โ (0...1)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = 0)) |
115 | 114 | simprd 497 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ฮฃ๐ โ
(0...1)(((coeffโ๐)โ๐) ยท (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))โ๐)) = 0) |
116 | 80, 82, 115 | 3eqtr2d 2779 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (๐โ-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) = 0) |
117 | | plyf 25582 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (Polyโโ)
โ ๐:โโถโ) |
118 | 117 | ffnd 6673 |
. . . . . . . . . . . . . . 15
โข (๐ โ (Polyโโ)
โ ๐ Fn
โ) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ๐ Fn
โ) |
120 | | fniniseg 7014 |
. . . . . . . . . . . . . 14
โข (๐ Fn โ โ
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ (โก๐ โ {0}) โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ โง
(๐โ-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) = 0))) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ (โก๐ โ {0}) โ (-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ โง
(๐โ-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))) = 0))) |
122 | 69, 116, 121 | mpbir2and 712 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ -(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ (โก๐ โ {0})) |
123 | 122 | snssd 4773 |
. . . . . . . . . . 11
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ {-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0})) |
124 | 123 | adantrr 716 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0})) |
125 | | hashsng 14278 |
. . . . . . . . . . . . . . 15
โข
(-(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) โ โ โ
(โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = 1) |
126 | 69, 125 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = 1) |
127 | 126, 52 | eqtrd 2773 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = (degโ๐)) |
128 | 127 | adantrr 716 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
(โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = (degโ๐)) |
129 | | simprr 772 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
(โฏโ(โก๐ โ {0})) = (degโ๐)) |
130 | 128, 129 | eqtr4d 2776 |
. . . . . . . . . . 11
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
(โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = (โฏโ(โก๐ โ {0}))) |
131 | | snfi 8994 |
. . . . . . . . . . . . 13
โข
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ Fin |
132 | | hashen 14256 |
. . . . . . . . . . . . 13
โข
(({-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ Fin โง (โก๐ โ {0}) โ Fin) โ
((โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = (โฏโ(โก๐ โ {0})) โ {-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0}))) |
133 | 131, 77, 132 | sylancr 588 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = (โฏโ(โก๐ โ {0})) โ {-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0}))) |
134 | 133 | adantrr 716 |
. . . . . . . . . . 11
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
((โฏโ{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}) = (โฏโ(โก๐ โ {0})) โ {-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0}))) |
135 | 130, 134 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0})) |
136 | | fisseneq 9207 |
. . . . . . . . . 10
โข (((โก๐ โ {0}) โ Fin โง
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0}) โง {-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} โ (โก๐ โ {0})) โ {-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} = (โก๐ โ {0})) |
137 | 78, 124, 135, 136 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))} = (โก๐ โ {0})) |
138 | 137 | sumeq1d 15594 |
. . . . . . . 8
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
ฮฃ๐ฅ โ
{-(((coeffโ๐)โ0) / ((coeffโ๐)โ1))}๐ฅ = ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ) |
139 | | 1m1e0 12233 |
. . . . . . . . . . . . 13
โข (1
โ 1) = 0 |
140 | 52 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (1 โ 1) = ((degโ๐) โ 1)) |
141 | 139, 140 | eqtr3id 2787 |
. . . . . . . . . . . 12
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ 0 = ((degโ๐)
โ 1)) |
142 | 141 | fveq2d 6850 |
. . . . . . . . . . 11
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ ((coeffโ๐)โ0) = ((coeffโ๐)โ((degโ๐) โ 1))) |
143 | 142, 53 | oveq12d 7379 |
. . . . . . . . . 10
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ (((coeffโ๐)โ0) / ((coeffโ๐)โ1)) = (((coeffโ๐)โ((degโ๐) โ 1)) /
((coeffโ๐)โ(degโ๐)))) |
144 | 143 | negeqd 11403 |
. . . . . . . . 9
โข ((๐ โ (Polyโโ)
โง 1 = (degโ๐))
โ -(((coeffโ๐)โ0) / ((coeffโ๐)โ1)) = -(((coeffโ๐)โ((degโ๐) โ 1)) /
((coeffโ๐)โ(degโ๐)))) |
145 | 144 | adantrr 716 |
. . . . . . . 8
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
-(((coeffโ๐)โ0)
/ ((coeffโ๐)โ1)) = -(((coeffโ๐)โ((degโ๐) โ 1)) /
((coeffโ๐)โ(degโ๐)))) |
146 | 73, 138, 145 | 3eqtr3d 2781 |
. . . . . . 7
โข ((๐ โ (Polyโโ)
โง (1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐))) โ
ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) |
147 | 146 | ex 414 |
. . . . . 6
โข (๐ โ (Polyโโ)
โ ((1 = (degโ๐)
โง (โฏโ(โก๐ โ {0})) =
(degโ๐)) โ
ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
148 | 147 | rgen 3063 |
. . . . 5
โข
โ๐ โ
(Polyโโ)((1 = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) |
149 | | id 22 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ฅ โ ๐ฆ = ๐ฅ) |
150 | 149 | cbvsumv 15589 |
. . . . . . . . . . 11
โข
ฮฃ๐ฆ โ
(โก๐ โ {0})๐ฆ = ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ |
151 | 150 | eqeq1i 2738 |
. . . . . . . . . 10
โข
(ฮฃ๐ฆ โ
(โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) |
152 | 151 | imbi2i 336 |
. . . . . . . . 9
โข (((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ ((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
153 | 152 | ralbii 3093 |
. . . . . . . 8
โข
(โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
154 | | eqid 2733 |
. . . . . . . . . 10
โข
(coeffโ๐) =
(coeffโ๐) |
155 | | eqid 2733 |
. . . . . . . . . 10
โข
(degโ๐) =
(degโ๐) |
156 | | eqid 2733 |
. . . . . . . . . 10
โข (โก๐ โ {0}) = (โก๐ โ {0}) |
157 | | simp1r 1199 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ ๐ โ
(Polyโโ)) |
158 | | simp3r 1203 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ (โฏโ(โก๐ โ {0})) = (degโ๐)) |
159 | | simp1l 1198 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ ๐ โ โ) |
160 | | simp3l 1202 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ (๐ + 1) = (degโ๐)) |
161 | | simp2 1138 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
162 | 161, 153 | sylib 217 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
163 | | eqid 2733 |
. . . . . . . . . 10
โข (๐ quot (Xp
โf โ (โ ร {๐ง}))) = (๐ quot (Xp
โf โ (โ ร {๐ง}))) |
164 | 154, 155,
156, 157, 158, 159, 160, 162, 163 | vieta1lem2 25694 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ (Polyโโ))
โง โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โง ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐))) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) |
165 | 164 | 3exp 1120 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (Polyโโ))
โ (โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฆ โ (โก๐ โ {0})๐ฆ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ (((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
166 | 153, 165 | biimtrrid 242 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (Polyโโ))
โ (โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ (((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
167 | 166 | ralrimdva 3148 |
. . . . . 6
โข (๐ โ โ โ
(โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)(((๐ +
1) = (degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
168 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ = ๐ โ (degโ๐) = (degโ๐)) |
169 | 168 | eqeq2d 2744 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ + 1) = (degโ๐) โ (๐ + 1) = (degโ๐))) |
170 | | cnveq 5833 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ โก๐ = โก๐) |
171 | 170 | imaeq1d 6016 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (โก๐ โ {0}) = (โก๐ โ {0})) |
172 | 171 | fveq2d 6850 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โฏโ(โก๐ โ {0})) = (โฏโ(โก๐ โ {0}))) |
173 | 172, 168 | eqeq12d 2749 |
. . . . . . . . 9
โข (๐ = ๐ โ ((โฏโ(โก๐ โ {0})) = (degโ๐) โ (โฏโ(โก๐ โ {0})) = (degโ๐))) |
174 | 169, 173 | anbi12d 632 |
. . . . . . . 8
โข (๐ = ๐ โ (((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)))) |
175 | 171 | sumeq1d 15594 |
. . . . . . . . 9
โข (๐ = ๐ โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ) |
176 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (coeffโ๐) = (coeffโ๐)) |
177 | 168 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((degโ๐) โ 1) = ((degโ๐) โ 1)) |
178 | 176, 177 | fveq12d 6853 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((coeffโ๐)โ((degโ๐) โ 1)) = ((coeffโ๐)โ((degโ๐) โ 1))) |
179 | 176, 168 | fveq12d 6853 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((coeffโ๐)โ(degโ๐)) = ((coeffโ๐)โ(degโ๐))) |
180 | 178, 179 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) = (((coeffโ๐)โ((degโ๐) โ 1)) /
((coeffโ๐)โ(degโ๐)))) |
181 | 180 | negeqd 11403 |
. . . . . . . . 9
โข (๐ = ๐ โ -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) = -(((coeffโ๐)โ((degโ๐) โ 1)) /
((coeffโ๐)โ(degโ๐)))) |
182 | 175, 181 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ = ๐ โ (ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
183 | 174, 182 | imbi12d 345 |
. . . . . . 7
โข (๐ = ๐ โ ((((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ (((๐ + 1) = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
184 | 183 | cbvralvw 3224 |
. . . . . 6
โข
(โ๐ โ
(Polyโโ)(((๐ +
1) = (degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)(((๐ +
1) = (degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
185 | 167, 184 | syl6ib 251 |
. . . . 5
โข (๐ โ โ โ
(โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))) โ โ๐ โ
(Polyโโ)(((๐ +
1) = (degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐)))))) |
186 | 30, 34, 38, 42, 148, 185 | nnind 12179 |
. . . 4
โข (๐ โ โ โ
โ๐ โ
(Polyโโ)((๐ =
(degโ๐) โง
(โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
187 | 26, 186 | syl 17 |
. . 3
โข (๐ โ โ๐ โ (Polyโโ)((๐ = (degโ๐) โง (โฏโ(โก๐ โ {0})) = (degโ๐)) โ ฮฃ๐ฅ โ (โก๐ โ {0})๐ฅ = -(((coeffโ๐)โ((degโ๐) โ 1)) / ((coeffโ๐)โ(degโ๐))))) |
188 | | plyssc 25584 |
. . . 4
โข
(Polyโ๐)
โ (Polyโโ) |
189 | | vieta1.4 |
. . . 4
โข (๐ โ ๐น โ (Polyโ๐)) |
190 | 188, 189 | sselid 3946 |
. . 3
โข (๐ โ ๐น โ
(Polyโโ)) |
191 | 25, 187, 190 | rspcdva 3584 |
. 2
โข (๐ โ ((โฏโ๐
) = ๐ โ ฮฃ๐ฅ โ ๐
๐ฅ = -((๐ดโ(๐ โ 1)) / (๐ดโ๐)))) |
192 | 1, 191 | mpd 15 |
1
โข (๐ โ ฮฃ๐ฅ โ ๐
๐ฅ = -((๐ดโ(๐ โ 1)) / (๐ดโ๐))) |