Step | Hyp | Ref
| Expression |
1 | | vieta1lem.9 |
. . 3
β’ π = (πΉ quot (Xp
βf β (β Γ {π§}))) |
2 | | plyssc 25577 |
. . . . 5
β’
(Polyβπ)
β (Polyββ) |
3 | | vieta1.4 |
. . . . . 6
β’ (π β πΉ β (Polyβπ)) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β π
) β πΉ β (Polyβπ)) |
5 | 2, 4 | sselid 3947 |
. . . 4
β’ ((π β§ π§ β π
) β πΉ β
(Polyββ)) |
6 | | vieta1.3 |
. . . . . . . . 9
β’ π
= (β‘πΉ β {0}) |
7 | | cnvimass 6038 |
. . . . . . . . 9
β’ (β‘πΉ β {0}) β dom πΉ |
8 | 6, 7 | eqsstri 3983 |
. . . . . . . 8
β’ π
β dom πΉ |
9 | | plyf 25575 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
10 | 3, 9 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
11 | 8, 10 | fssdm 6693 |
. . . . . . 7
β’ (π β π
β β) |
12 | 11 | sselda 3949 |
. . . . . 6
β’ ((π β§ π§ β π
) β π§ β β) |
13 | | eqid 2737 |
. . . . . . 7
β’
(Xp βf β (β Γ
{π§})) =
(Xp βf β (β Γ {π§})) |
14 | 13 | plyremlem 25680 |
. . . . . 6
β’ (π§ β β β
((Xp βf β (β Γ {π§})) β (Polyββ)
β§ (degβ(Xp βf β (β
Γ {π§}))) = 1 β§
(β‘(Xp
βf β (β Γ {π§})) β {0}) = {π§})) |
15 | 12, 14 | syl 17 |
. . . . 5
β’ ((π β§ π§ β π
) β ((Xp
βf β (β Γ {π§})) β (Polyββ) β§
(degβ(Xp βf β (β Γ
{π§}))) = 1 β§ (β‘(Xp βf
β (β Γ {π§})) β {0}) = {π§})) |
16 | 15 | simp1d 1143 |
. . . 4
β’ ((π β§ π§ β π
) β (Xp
βf β (β Γ {π§})) β
(Polyββ)) |
17 | 15 | simp2d 1144 |
. . . . . 6
β’ ((π β§ π§ β π
) β (degβ(Xp
βf β (β Γ {π§}))) = 1) |
18 | | ax-1ne0 11127 |
. . . . . . 7
β’ 1 β
0 |
19 | 18 | a1i 11 |
. . . . . 6
β’ ((π β§ π§ β π
) β 1 β 0) |
20 | 17, 19 | eqnetrd 3012 |
. . . . 5
β’ ((π β§ π§ β π
) β (degβ(Xp
βf β (β Γ {π§}))) β 0) |
21 | | fveq2 6847 |
. . . . . . 7
β’
((Xp βf β (β Γ
{π§})) =
0π β (degβ(Xp
βf β (β Γ {π§}))) =
(degβ0π)) |
22 | | dgr0 25639 |
. . . . . . 7
β’
(degβ0π) = 0 |
23 | 21, 22 | eqtrdi 2793 |
. . . . . 6
β’
((Xp βf β (β Γ
{π§})) =
0π β (degβ(Xp
βf β (β Γ {π§}))) = 0) |
24 | 23 | necon3i 2977 |
. . . . 5
β’
((degβ(Xp βf β (β
Γ {π§}))) β 0
β (Xp βf β (β Γ
{π§})) β
0π) |
25 | 20, 24 | syl 17 |
. . . 4
β’ ((π β§ π§ β π
) β (Xp
βf β (β Γ {π§})) β
0π) |
26 | | quotcl2 25678 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ (Xp βf β (β Γ {π§})) β (Polyββ)
β§ (Xp βf β (β Γ {π§})) β 0π)
β (πΉ quot
(Xp βf β (β Γ {π§}))) β
(Polyββ)) |
27 | 5, 16, 25, 26 | syl3anc 1372 |
. . 3
β’ ((π β§ π§ β π
) β (πΉ quot (Xp
βf β (β Γ {π§}))) β
(Polyββ)) |
28 | 1, 27 | eqeltrid 2842 |
. 2
β’ ((π β§ π§ β π
) β π β
(Polyββ)) |
29 | | 1cnd 11157 |
. . 3
β’ ((π β§ π§ β π
) β 1 β β) |
30 | | vieta1lem.6 |
. . . . 5
β’ (π β π· β β) |
31 | 30 | nncnd 12176 |
. . . 4
β’ (π β π· β β) |
32 | 31 | adantr 482 |
. . 3
β’ ((π β§ π§ β π
) β π· β β) |
33 | | dgrcl 25610 |
. . . . 5
β’ (π β (Polyββ)
β (degβπ) β
β0) |
34 | 28, 33 | syl 17 |
. . . 4
β’ ((π β§ π§ β π
) β (degβπ) β
β0) |
35 | 34 | nn0cnd 12482 |
. . 3
β’ ((π β§ π§ β π
) β (degβπ) β β) |
36 | | ax-1cn 11116 |
. . . . 5
β’ 1 β
β |
37 | | addcom 11348 |
. . . . 5
β’ ((1
β β β§ π·
β β) β (1 + π·) = (π· + 1)) |
38 | 36, 32, 37 | sylancr 588 |
. . . 4
β’ ((π β§ π§ β π
) β (1 + π·) = (π· + 1)) |
39 | | vieta1lem.7 |
. . . . . . 7
β’ (π β (π· + 1) = π) |
40 | | vieta1.2 |
. . . . . . 7
β’ π = (degβπΉ) |
41 | 39, 40 | eqtrdi 2793 |
. . . . . 6
β’ (π β (π· + 1) = (degβπΉ)) |
42 | 41 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β π
) β (π· + 1) = (degβπΉ)) |
43 | 6 | eleq2i 2830 |
. . . . . . . . . 10
β’ (π§ β π
β π§ β (β‘πΉ β {0})) |
44 | 10 | ffnd 6674 |
. . . . . . . . . . 11
β’ (π β πΉ Fn β) |
45 | | fniniseg 7015 |
. . . . . . . . . . 11
β’ (πΉ Fn β β (π§ β (β‘πΉ β {0}) β (π§ β β β§ (πΉβπ§) = 0))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
β’ (π β (π§ β (β‘πΉ β {0}) β (π§ β β β§ (πΉβπ§) = 0))) |
47 | 43, 46 | bitrid 283 |
. . . . . . . . 9
β’ (π β (π§ β π
β (π§ β β β§ (πΉβπ§) = 0))) |
48 | 47 | simplbda 501 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β (πΉβπ§) = 0) |
49 | 13 | facth 25682 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ π§ β β β§ (πΉβπ§) = 0) β πΉ = ((Xp
βf β (β Γ {π§})) βf Β· (πΉ quot (Xp
βf β (β Γ {π§}))))) |
50 | 4, 12, 48, 49 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π§ β π
) β πΉ = ((Xp
βf β (β Γ {π§})) βf Β· (πΉ quot (Xp
βf β (β Γ {π§}))))) |
51 | 1 | oveq2i 7373 |
. . . . . . 7
β’
((Xp βf β (β Γ
{π§})) βf
Β· π) =
((Xp βf β (β Γ {π§})) βf Β·
(πΉ quot
(Xp βf β (β Γ {π§})))) |
52 | 50, 51 | eqtr4di 2795 |
. . . . . 6
β’ ((π β§ π§ β π
) β πΉ = ((Xp
βf β (β Γ {π§})) βf Β· π)) |
53 | 52 | fveq2d 6851 |
. . . . 5
β’ ((π β§ π§ β π
) β (degβπΉ) = (degβ((Xp
βf β (β Γ {π§})) βf Β· π))) |
54 | 30 | peano2nnd 12177 |
. . . . . . . . . . . . . . 15
β’ (π β (π· + 1) β β) |
55 | 39, 54 | eqeltrrd 2839 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
56 | 55 | nnne0d 12210 |
. . . . . . . . . . . . 13
β’ (π β π β 0) |
57 | 40, 56 | eqnetrrid 3020 |
. . . . . . . . . . . 12
β’ (π β (degβπΉ) β 0) |
58 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (πΉ = 0π β
(degβπΉ) =
(degβ0π)) |
59 | 58, 22 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (πΉ = 0π β
(degβπΉ) =
0) |
60 | 59 | necon3i 2977 |
. . . . . . . . . . . 12
β’
((degβπΉ) β
0 β πΉ β
0π) |
61 | 57, 60 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ β
0π) |
62 | 61 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β πΉ β
0π) |
63 | 52, 62 | eqnetrrd 3013 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β ((Xp
βf β (β Γ {π§})) βf Β· π) β
0π) |
64 | | plymul0or 25657 |
. . . . . . . . . . 11
β’
(((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ π β (Polyββ)) β
(((Xp βf β (β Γ {π§})) βf Β·
π) = 0π
β ((Xp βf β (β Γ
{π§})) =
0π β¨ π = 0π))) |
65 | 16, 28, 64 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π§ β π
) β (((Xp
βf β (β Γ {π§})) βf Β· π) = 0π β
((Xp βf β (β Γ {π§})) = 0π β¨
π =
0π))) |
66 | 65 | necon3abid 2981 |
. . . . . . . . 9
β’ ((π β§ π§ β π
) β (((Xp
βf β (β Γ {π§})) βf Β· π) β 0π
β Β¬ ((Xp βf β (β
Γ {π§})) =
0π β¨ π = 0π))) |
67 | 63, 66 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π§ β π
) β Β¬ ((Xp
βf β (β Γ {π§})) = 0π β¨ π =
0π)) |
68 | | neanior 3038 |
. . . . . . . 8
β’
(((Xp βf β (β Γ
{π§})) β
0π β§ π β 0π) β Β¬
((Xp βf β (β Γ {π§})) = 0π β¨
π =
0π)) |
69 | 67, 68 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π§ β π
) β ((Xp
βf β (β Γ {π§})) β 0π β§ π β
0π)) |
70 | 69 | simprd 497 |
. . . . . 6
β’ ((π β§ π§ β π
) β π β
0π) |
71 | | eqid 2737 |
. . . . . . 7
β’
(degβ(Xp βf β (β
Γ {π§}))) =
(degβ(Xp βf β (β Γ
{π§}))) |
72 | | eqid 2737 |
. . . . . . 7
β’
(degβπ) =
(degβπ) |
73 | 71, 72 | dgrmul 25647 |
. . . . . 6
β’
((((Xp βf β (β Γ
{π§})) β
(Polyββ) β§ (Xp βf β
(β Γ {π§})) β
0π) β§ (π β (Polyββ) β§ π β 0π))
β (degβ((Xp βf β (β
Γ {π§}))
βf Β· π)) = ((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) |
74 | 16, 25, 28, 70, 73 | syl22anc 838 |
. . . . 5
β’ ((π β§ π§ β π
) β (degβ((Xp
βf β (β Γ {π§})) βf Β· π)) =
((degβ(Xp βf β (β Γ
{π§}))) + (degβπ))) |
75 | 42, 53, 74 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ π§ β π
) β (π· + 1) = ((degβ(Xp
βf β (β Γ {π§}))) + (degβπ))) |
76 | 17 | oveq1d 7377 |
. . . 4
β’ ((π β§ π§ β π
) β ((degβ(Xp
βf β (β Γ {π§}))) + (degβπ)) = (1 + (degβπ))) |
77 | 38, 75, 76 | 3eqtrd 2781 |
. . 3
β’ ((π β§ π§ β π
) β (1 + π·) = (1 + (degβπ))) |
78 | 29, 32, 35, 77 | addcanad 11367 |
. 2
β’ ((π β§ π§ β π
) β π· = (degβπ)) |
79 | 28, 78 | jca 513 |
1
β’ ((π β§ π§ β π
) β (π β (Polyββ) β§ π· = (degβπ))) |