Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(coeffβ(π§
β β β¦ (πΉβ(π§ + π)))) = (coeffβ(π§ β β β¦ (πΉβ(π§ + π)))) |
2 | | eqid 2733 |
. . . 4
β’
(degβ(π§ β
β β¦ (πΉβ(π§ + π)))) = (degβ(π§ β β β¦ (πΉβ(π§ + π)))) |
3 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π§ β β) β π§ β β) |
4 | | ftalem7.5 |
. . . . . . . 8
β’ (π β π β β) |
5 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β β) β π β β) |
6 | 3, 5 | addcld 11233 |
. . . . . 6
β’ ((π β§ π§ β β) β (π§ + π) β β) |
7 | | cnex 11191 |
. . . . . . . . 9
β’ β
β V |
8 | 7 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
9 | 4 | negcld 11558 |
. . . . . . . . 9
β’ (π β -π β β) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π§ β β) β -π β β) |
11 | | df-idp 25703 |
. . . . . . . . . 10
β’
Xp = ( I βΎ β) |
12 | | mptresid 6051 |
. . . . . . . . . 10
β’ ( I
βΎ β) = (π§
β β β¦ π§) |
13 | 11, 12 | eqtri 2761 |
. . . . . . . . 9
β’
Xp = (π§ β β β¦ π§) |
14 | 13 | a1i 11 |
. . . . . . . 8
β’ (π β Xp =
(π§ β β β¦
π§)) |
15 | | fconstmpt 5739 |
. . . . . . . . 9
β’ (β
Γ {-π}) = (π§ β β β¦ -π) |
16 | 15 | a1i 11 |
. . . . . . . 8
β’ (π β (β Γ {-π}) = (π§ β β β¦ -π)) |
17 | 8, 3, 10, 14, 16 | offval2 7690 |
. . . . . . 7
β’ (π β (Xp
βf β (β Γ {-π})) = (π§ β β β¦ (π§ β -π))) |
18 | | id 22 |
. . . . . . . . 9
β’ (π§ β β β π§ β
β) |
19 | | subneg 11509 |
. . . . . . . . 9
β’ ((π§ β β β§ π β β) β (π§ β -π) = (π§ + π)) |
20 | 18, 4, 19 | syl2anr 598 |
. . . . . . . 8
β’ ((π β§ π§ β β) β (π§ β -π) = (π§ + π)) |
21 | 20 | mpteq2dva 5249 |
. . . . . . 7
β’ (π β (π§ β β β¦ (π§ β -π)) = (π§ β β β¦ (π§ + π))) |
22 | 17, 21 | eqtrd 2773 |
. . . . . 6
β’ (π β (Xp
βf β (β Γ {-π})) = (π§ β β β¦ (π§ + π))) |
23 | | ftalem.3 |
. . . . . . . 8
β’ (π β πΉ β (Polyβπ)) |
24 | | plyf 25712 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
25 | 23, 24 | syl 17 |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
26 | 25 | feqmptd 6961 |
. . . . . 6
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
27 | | fveq2 6892 |
. . . . . 6
β’ (π¦ = (π§ + π) β (πΉβπ¦) = (πΉβ(π§ + π))) |
28 | 6, 22, 26, 27 | fmptco 7127 |
. . . . 5
β’ (π β (πΉ β (Xp
βf β (β Γ {-π}))) = (π§ β β β¦ (πΉβ(π§ + π)))) |
29 | | plyssc 25714 |
. . . . . . 7
β’
(Polyβπ)
β (Polyββ) |
30 | 29, 23 | sselid 3981 |
. . . . . 6
β’ (π β πΉ β
(Polyββ)) |
31 | | eqid 2733 |
. . . . . . . . 9
β’
(Xp βf β (β Γ
{-π})) =
(Xp βf β (β Γ {-π})) |
32 | 31 | plyremlem 25817 |
. . . . . . . 8
β’ (-π β β β
((Xp βf β (β Γ {-π})) β (Polyββ)
β§ (degβ(Xp βf β (β
Γ {-π}))) = 1 β§
(β‘(Xp
βf β (β Γ {-π})) β {0}) = {-π})) |
33 | 9, 32 | syl 17 |
. . . . . . 7
β’ (π β ((Xp
βf β (β Γ {-π})) β (Polyββ) β§
(degβ(Xp βf β (β Γ
{-π}))) = 1 β§ (β‘(Xp βf
β (β Γ {-π})) β {0}) = {-π})) |
34 | 33 | simp1d 1143 |
. . . . . 6
β’ (π β (Xp
βf β (β Γ {-π})) β
(Polyββ)) |
35 | | addcl 11192 |
. . . . . . 7
β’ ((π§ β β β§ π€ β β) β (π§ + π€) β β) |
36 | 35 | adantl 483 |
. . . . . 6
β’ ((π β§ (π§ β β β§ π€ β β)) β (π§ + π€) β β) |
37 | | mulcl 11194 |
. . . . . . 7
β’ ((π§ β β β§ π€ β β) β (π§ Β· π€) β β) |
38 | 37 | adantl 483 |
. . . . . 6
β’ ((π β§ (π§ β β β§ π€ β β)) β (π§ Β· π€) β β) |
39 | 30, 34, 36, 38 | plyco 25755 |
. . . . 5
β’ (π β (πΉ β (Xp
βf β (β Γ {-π}))) β
(Polyββ)) |
40 | 28, 39 | eqeltrrd 2835 |
. . . 4
β’ (π β (π§ β β β¦ (πΉβ(π§ + π))) β
(Polyββ)) |
41 | 28 | fveq2d 6896 |
. . . . 5
β’ (π β (degβ(πΉ β (Xp
βf β (β Γ {-π})))) = (degβ(π§ β β β¦ (πΉβ(π§ + π))))) |
42 | | ftalem.2 |
. . . . . . 7
β’ π = (degβπΉ) |
43 | | eqid 2733 |
. . . . . . 7
β’
(degβ(Xp βf β (β
Γ {-π}))) =
(degβ(Xp βf β (β Γ
{-π}))) |
44 | 42, 43, 30, 34 | dgrco 25789 |
. . . . . 6
β’ (π β (degβ(πΉ β (Xp
βf β (β Γ {-π})))) = (π Β· (degβ(Xp
βf β (β Γ {-π}))))) |
45 | | ftalem.4 |
. . . . . . 7
β’ (π β π β β) |
46 | 33 | simp2d 1144 |
. . . . . . . 8
β’ (π β
(degβ(Xp βf β (β Γ
{-π}))) =
1) |
47 | | 1nn 12223 |
. . . . . . . 8
β’ 1 β
β |
48 | 46, 47 | eqeltrdi 2842 |
. . . . . . 7
β’ (π β
(degβ(Xp βf β (β Γ
{-π}))) β
β) |
49 | 45, 48 | nnmulcld 12265 |
. . . . . 6
β’ (π β (π Β· (degβ(Xp
βf β (β Γ {-π})))) β β) |
50 | 44, 49 | eqeltrd 2834 |
. . . . 5
β’ (π β (degβ(πΉ β (Xp
βf β (β Γ {-π})))) β β) |
51 | 41, 50 | eqeltrrd 2835 |
. . . 4
β’ (π β (degβ(π§ β β β¦ (πΉβ(π§ + π)))) β β) |
52 | | 0cn 11206 |
. . . . . . 7
β’ 0 β
β |
53 | | fvoveq1 7432 |
. . . . . . . 8
β’ (π§ = 0 β (πΉβ(π§ + π)) = (πΉβ(0 + π))) |
54 | | eqid 2733 |
. . . . . . . 8
β’ (π§ β β β¦ (πΉβ(π§ + π))) = (π§ β β β¦ (πΉβ(π§ + π))) |
55 | | fvex 6905 |
. . . . . . . 8
β’ (πΉβ(0 + π)) β V |
56 | 53, 54, 55 | fvmpt 6999 |
. . . . . . 7
β’ (0 β
β β ((π§ β
β β¦ (πΉβ(π§ + π)))β0) = (πΉβ(0 + π))) |
57 | 52, 56 | ax-mp 5 |
. . . . . 6
β’ ((π§ β β β¦ (πΉβ(π§ + π)))β0) = (πΉβ(0 + π)) |
58 | 4 | addlidd 11415 |
. . . . . . 7
β’ (π β (0 + π) = π) |
59 | 58 | fveq2d 6896 |
. . . . . 6
β’ (π β (πΉβ(0 + π)) = (πΉβπ)) |
60 | 57, 59 | eqtrid 2785 |
. . . . 5
β’ (π β ((π§ β β β¦ (πΉβ(π§ + π)))β0) = (πΉβπ)) |
61 | | ftalem7.6 |
. . . . 5
β’ (π β (πΉβπ) β 0) |
62 | 60, 61 | eqnetrd 3009 |
. . . 4
β’ (π β ((π§ β β β¦ (πΉβ(π§ + π)))β0) β 0) |
63 | 1, 2, 40, 51, 62 | ftalem6 26582 |
. . 3
β’ (π β βπ¦ β β (absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) < (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0))) |
64 | | id 22 |
. . . . . 6
β’ (π¦ β β β π¦ β
β) |
65 | | addcl 11192 |
. . . . . 6
β’ ((π¦ β β β§ π β β) β (π¦ + π) β β) |
66 | 64, 4, 65 | syl2anr 598 |
. . . . 5
β’ ((π β§ π¦ β β) β (π¦ + π) β β) |
67 | | fvoveq1 7432 |
. . . . . . . . . . 11
β’ (π§ = π¦ β (πΉβ(π§ + π)) = (πΉβ(π¦ + π))) |
68 | | fvex 6905 |
. . . . . . . . . . 11
β’ (πΉβ(π¦ + π)) β V |
69 | 67, 54, 68 | fvmpt 6999 |
. . . . . . . . . 10
β’ (π¦ β β β ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦) = (πΉβ(π¦ + π))) |
70 | 69 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦) = (πΉβ(π¦ + π))) |
71 | 70 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) = (absβ(πΉβ(π¦ + π)))) |
72 | 60 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β ((π§ β β β¦ (πΉβ(π§ + π)))β0) = (πΉβπ)) |
73 | 72 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0)) = (absβ(πΉβπ))) |
74 | 71, 73 | breq12d 5162 |
. . . . . . 7
β’ ((π β§ π¦ β β) β ((absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) < (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0)) β (absβ(πΉβ(π¦ + π))) < (absβ(πΉβπ)))) |
75 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β πΉ:ββΆβ) |
76 | 75, 66 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (πΉβ(π¦ + π)) β β) |
77 | 76 | abscld 15383 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (absβ(πΉβ(π¦ + π))) β β) |
78 | 25, 4 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ (π β (πΉβπ) β β) |
79 | 78 | abscld 15383 |
. . . . . . . . 9
β’ (π β (absβ(πΉβπ)) β β) |
80 | 79 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (absβ(πΉβπ)) β β) |
81 | 77, 80 | ltnled 11361 |
. . . . . . 7
β’ ((π β§ π¦ β β) β ((absβ(πΉβ(π¦ + π))) < (absβ(πΉβπ)) β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβ(π¦ + π))))) |
82 | 74, 81 | bitrd 279 |
. . . . . 6
β’ ((π β§ π¦ β β) β ((absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) < (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0)) β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβ(π¦ + π))))) |
83 | 82 | biimpd 228 |
. . . . 5
β’ ((π β§ π¦ β β) β ((absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) < (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0)) β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβ(π¦ + π))))) |
84 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π₯ = (π¦ + π) β (absβ(πΉβπ₯)) = (absβ(πΉβ(π¦ + π)))) |
85 | 84 | breq2d 5161 |
. . . . . . 7
β’ (π₯ = (π¦ + π) β ((absβ(πΉβπ)) β€ (absβ(πΉβπ₯)) β (absβ(πΉβπ)) β€ (absβ(πΉβ(π¦ + π))))) |
86 | 85 | notbid 318 |
. . . . . 6
β’ (π₯ = (π¦ + π) β (Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβπ₯)) β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβ(π¦ + π))))) |
87 | 86 | rspcev 3613 |
. . . . 5
β’ (((π¦ + π) β β β§ Β¬
(absβ(πΉβπ)) β€ (absβ(πΉβ(π¦ + π)))) β βπ₯ β β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβπ₯))) |
88 | 66, 83, 87 | syl6an 683 |
. . . 4
β’ ((π β§ π¦ β β) β ((absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) < (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0)) β βπ₯ β β Β¬
(absβ(πΉβπ)) β€ (absβ(πΉβπ₯)))) |
89 | 88 | rexlimdva 3156 |
. . 3
β’ (π β (βπ¦ β β (absβ((π§ β β β¦ (πΉβ(π§ + π)))βπ¦)) < (absβ((π§ β β β¦ (πΉβ(π§ + π)))β0)) β βπ₯ β β Β¬
(absβ(πΉβπ)) β€ (absβ(πΉβπ₯)))) |
90 | 63, 89 | mpd 15 |
. 2
β’ (π β βπ₯ β β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβπ₯))) |
91 | | rexnal 3101 |
. 2
β’
(βπ₯ β
β Β¬ (absβ(πΉβπ)) β€ (absβ(πΉβπ₯)) β Β¬ βπ₯ β β (absβ(πΉβπ)) β€ (absβ(πΉβπ₯))) |
92 | 90, 91 | sylib 217 |
1
β’ (π β Β¬ βπ₯ β β
(absβ(πΉβπ)) β€ (absβ(πΉβπ₯))) |