Step | Hyp | Ref
| Expression |
1 | | dgreq0.2 |
. . . . . 6
⊢ 𝐴 = (coeff‘𝐹) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝐹 = 0𝑝 →
(coeff‘𝐹) =
(coeff‘0𝑝)) |
3 | 1, 2 | syl5eq 2656 |
. . . . 5
⊢ (𝐹 = 0𝑝 →
𝐴 =
(coeff‘0𝑝)) |
4 | | coe0 23816 |
. . . . 5
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
5 | 3, 4 | syl6eq 2660 |
. . . 4
⊢ (𝐹 = 0𝑝 →
𝐴 = (ℕ0
× {0})) |
6 | | dgreq0.1 |
. . . . . 6
⊢ 𝑁 = (deg‘𝐹) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
8 | 6, 7 | syl5eq 2656 |
. . . . 5
⊢ (𝐹 = 0𝑝 →
𝑁 =
(deg‘0𝑝)) |
9 | | dgr0 23822 |
. . . . 5
⊢
(deg‘0𝑝) = 0 |
10 | 8, 9 | syl6eq 2660 |
. . . 4
⊢ (𝐹 = 0𝑝 →
𝑁 = 0) |
11 | 5, 10 | fveq12d 6109 |
. . 3
⊢ (𝐹 = 0𝑝 →
(𝐴‘𝑁) = ((ℕ0 ×
{0})‘0)) |
12 | | 0nn0 11184 |
. . . 4
⊢ 0 ∈
ℕ0 |
13 | | fvconst2g 6372 |
. . . 4
⊢ ((0
∈ ℕ0 ∧ 0 ∈ ℕ0) →
((ℕ0 × {0})‘0) = 0) |
14 | 12, 12, 13 | mp2an 704 |
. . 3
⊢
((ℕ0 × {0})‘0) = 0 |
15 | 11, 14 | syl6eq 2660 |
. 2
⊢ (𝐹 = 0𝑝 →
(𝐴‘𝑁) = 0) |
16 | 1 | coefv0 23808 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0)) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐹‘0) = (𝐴‘0)) |
18 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
19 | 18 | nnred 10912 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
20 | 19 | ltm1d 10835 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) < 𝑁) |
21 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝐹 ∈ (Poly‘𝑆)) |
22 | | nnm1nn0 11211 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℕ0) |
24 | 1, 6 | dgrub 23794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ℕ0 ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑁) |
25 | 24 | 3expia 1259 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
26 | 25 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
27 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝐴‘𝑁) = 0) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = 𝑘 → (𝐴‘𝑁) = (𝐴‘𝑘)) |
29 | 28 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = 𝑘 → ((𝐴‘𝑁) = 0 ↔ (𝐴‘𝑘) = 0)) |
30 | 27, 29 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝑁 = 𝑘 → (𝐴‘𝑘) = 0)) |
31 | 30 | necon3d 2803 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → 𝑁 ≠ 𝑘)) |
32 | 26, 31 | jcad 554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → (𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘))) |
33 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
34 | 33 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑘 ∈
ℝ) |
35 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
36 | 35 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑁 ∈
ℝ) |
37 | 34, 36 | ltlend 10061 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝑘 < 𝑁 ↔ (𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘))) |
38 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
39 | 38 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑘 ∈
ℤ) |
40 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
41 | 40 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → 𝑁 ∈
ℤ) |
42 | | zltlem1 11307 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ 𝑘 ≤ (𝑁 − 1))) |
43 | 39, 41, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → (𝑘 < 𝑁 ↔ 𝑘 ≤ (𝑁 − 1))) |
44 | 37, 43 | bitr3d 269 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘) ↔ 𝑘 ≤ (𝑁 − 1))) |
45 | 32, 44 | sylibd 228 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))) |
46 | 45 | expr 641 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑘 ∈ ℕ0 → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))) |
47 | 46 | ralrimiv 2948 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))) |
48 | 1 | coef3 23792 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝐴:ℕ0⟶ℂ) |
50 | | plyco0 23752 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0} ↔
∀𝑘 ∈
ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))) |
51 | 23, 49, 50 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ((𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0} ↔
∀𝑘 ∈
ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))) |
52 | 47, 51 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0}) |
53 | 1, 6 | dgrlb 23796 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑁 − 1) ∈ ℕ0 ∧
(𝐴 “
(ℤ≥‘((𝑁 − 1) + 1))) = {0}) → 𝑁 ≤ (𝑁 − 1)) |
54 | 21, 23, 52, 53 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ (𝑁 − 1)) |
55 | 35 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
56 | | peano2rem 10227 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℝ) |
58 | 55, 57 | lenltd 10062 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 ≤ (𝑁 − 1) ↔ ¬ (𝑁 − 1) < 𝑁)) |
59 | 54, 58 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ¬ (𝑁 − 1) < 𝑁) |
60 | 20, 59 | pm2.65da 598 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → ¬ 𝑁 ∈ ℕ) |
61 | | dgrcl 23793 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
62 | 6, 61 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
63 | 62 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝑁 ∈
ℕ0) |
64 | | elnn0 11171 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
65 | 63, 64 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
66 | 65 | ord 391 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (¬ 𝑁 ∈ ℕ → 𝑁 = 0)) |
67 | 60, 66 | mpd 15 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝑁 = 0) |
68 | 67 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐴‘𝑁) = (𝐴‘0)) |
69 | | simpr 476 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐴‘𝑁) = 0) |
70 | 17, 68, 69 | 3eqtr2d 2650 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐹‘0) = 0) |
71 | 70 | sneqd 4137 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → {(𝐹‘0)} = {0}) |
72 | 71 | xpeq2d 5063 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (ℂ × {(𝐹‘0)}) = (ℂ ×
{0})) |
73 | 6, 67 | syl5eqr 2658 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (deg‘𝐹) = 0) |
74 | | 0dgrb 23806 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) |
75 | 74 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) |
76 | 73, 75 | mpbid 221 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝐹 = (ℂ × {(𝐹‘0)})) |
77 | | df-0p 23243 |
. . . . 5
⊢
0𝑝 = (ℂ × {0}) |
78 | 77 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 0𝑝 =
(ℂ × {0})) |
79 | 72, 76, 78 | 3eqtr4d 2654 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝐹 = 0𝑝) |
80 | 79 | ex 449 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ((𝐴‘𝑁) = 0 → 𝐹 = 0𝑝)) |
81 | 15, 80 | impbid2 215 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |