Step | Hyp | Ref
| Expression |
1 | | dgreq0.2 |
. . . . . 6
⊢ 𝐴 = (coeff‘𝐹) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝐹 = 0𝑝 →
(coeff‘𝐹) =
(coeff‘0𝑝)) |
3 | 1, 2 | syl5eq 2668 |
. . . . 5
⊢ (𝐹 = 0𝑝 →
𝐴 =
(coeff‘0𝑝)) |
4 | | coe0 24012 |
. . . . 5
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
5 | 3, 4 | syl6eq 2672 |
. . . 4
⊢ (𝐹 = 0𝑝 →
𝐴 = (ℕ0
× {0})) |
6 | | dgreq0.1 |
. . . . . 6
⊢ 𝑁 = (deg‘𝐹) |
7 | | fveq2 6191 |
. . . . . 6
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
8 | 6, 7 | syl5eq 2668 |
. . . . 5
⊢ (𝐹 = 0𝑝 →
𝑁 =
(deg‘0𝑝)) |
9 | | dgr0 24018 |
. . . . 5
⊢
(deg‘0𝑝) = 0 |
10 | 8, 9 | syl6eq 2672 |
. . . 4
⊢ (𝐹 = 0𝑝 →
𝑁 = 0) |
11 | 5, 10 | fveq12d 6197 |
. . 3
⊢ (𝐹 = 0𝑝 →
(𝐴‘𝑁) = ((ℕ0 ×
{0})‘0)) |
12 | | 0nn0 11307 |
. . . 4
⊢ 0 ∈
ℕ0 |
13 | | fvconst2g 6467 |
. . . 4
⊢ ((0
∈ ℕ0 ∧ 0 ∈ ℕ0) →
((ℕ0 × {0})‘0) = 0) |
14 | 12, 12, 13 | mp2an 708 |
. . 3
⊢
((ℕ0 × {0})‘0) = 0 |
15 | 11, 14 | syl6eq 2672 |
. 2
⊢ (𝐹 = 0𝑝 →
(𝐴‘𝑁) = 0) |
16 | 1 | coefv0 24004 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0)) |
17 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐹‘0) = (𝐴‘0)) |
18 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
19 | 18 | nnred 11035 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
20 | 19 | ltm1d 10956 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) < 𝑁) |
21 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝐹 ∈ (Poly‘𝑆)) |
22 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
23 | 22 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℕ0) |
24 | 1, 6 | dgrub 23990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑁) |
25 | 24 | 3expia 1267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
26 | 25 | ad2ant2rl 785 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
27 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝐴‘𝑁) = 0) |
28 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = 𝑘 → (𝐴‘𝑁) = (𝐴‘𝑘)) |
29 | 28 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = 𝑘 → ((𝐴‘𝑁) = 0 ↔ (𝐴‘𝑘) = 0)) |
30 | 27, 29 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝑁 = 𝑘 → (𝐴‘𝑘) = 0)) |
31 | 30 | necon3d 2815 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → 𝑁 ≠ 𝑘)) |
32 | 26, 31 | jcad 555 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → (𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘))) |
33 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
34 | 33 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑘 ∈
ℝ) |
35 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
36 | 35 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑁 ∈
ℝ) |
37 | 34, 36 | ltlend 10182 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝑘 < 𝑁 ↔ (𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘))) |
38 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
39 | 38 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑘 ∈
ℤ) |
40 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
41 | 40 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑁 ∈
ℤ) |
42 | | zltlem1 11430 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ 𝑘 ≤ (𝑁 − 1))) |
43 | 39, 41, 42 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝑘 < 𝑁 ↔ 𝑘 ≤ (𝑁 − 1))) |
44 | 37, 43 | bitr3d 270 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘) ↔ 𝑘 ≤ (𝑁 − 1))) |
45 | 32, 44 | sylibd 229 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))) |
46 | 45 | expr 643 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑘 ∈ ℕ0 → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))) |
47 | 46 | ralrimiv 2965 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))) |
48 | 1 | coef3 23988 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
49 | 48 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝐴:ℕ0⟶ℂ) |
50 | | plyco0 23948 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0} ↔
∀𝑘 ∈
ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))) |
51 | 23, 49, 50 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ((𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0} ↔
∀𝑘 ∈
ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))) |
52 | 47, 51 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0}) |
53 | 1, 6 | dgrlb 23992 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑁 − 1) ∈ ℕ0 ∧
(𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0}) → 𝑁 ≤ (𝑁 − 1)) |
54 | 21, 23, 52, 53 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ (𝑁 − 1)) |
55 | 35 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
56 | | peano2rem 10348 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℝ) |
58 | 55, 57 | lenltd 10183 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 ≤ (𝑁 − 1) ↔ ¬ (𝑁 − 1) < 𝑁)) |
59 | 54, 58 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ¬ (𝑁 − 1) < 𝑁) |
60 | 20, 59 | pm2.65da 600 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → ¬ 𝑁 ∈ ℕ) |
61 | | dgrcl 23989 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
62 | 6, 61 | syl5eqel 2705 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
63 | 62 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝑁 ∈
ℕ0) |
64 | | elnn0 11294 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
65 | 63, 64 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
66 | 65 | ord 392 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (¬ 𝑁 ∈ ℕ → 𝑁 = 0)) |
67 | 60, 66 | mpd 15 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝑁 = 0) |
68 | 67 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐴‘𝑁) = (𝐴‘0)) |
69 | | simpr 477 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐴‘𝑁) = 0) |
70 | 17, 68, 69 | 3eqtr2d 2662 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐹‘0) = 0) |
71 | 70 | sneqd 4189 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → {(𝐹‘0)} = {0}) |
72 | 71 | xpeq2d 5139 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (ℂ × {(𝐹‘0)}) = (ℂ ×
{0})) |
73 | 6, 67 | syl5eqr 2670 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (deg‘𝐹) = 0) |
74 | | 0dgrb 24002 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) |
75 | 74 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) |
76 | 73, 75 | mpbid 222 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝐹 = (ℂ × {(𝐹‘0)})) |
77 | | df-0p 23437 |
. . . . 5
⊢
0𝑝 = (ℂ × {0}) |
78 | 77 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 0𝑝 =
(ℂ × {0})) |
79 | 72, 76, 78 | 3eqtr4d 2666 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝐹 = 0𝑝) |
80 | 79 | ex 450 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ((𝐴‘𝑁) = 0 → 𝐹 = 0𝑝)) |
81 | 15, 80 | impbid2 216 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |