Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝑀 ∈
ℕ0) |
2 | | dgrub.1 |
. . . . . . . . . . . . . 14
⊢ 𝐴 = (coeff‘𝐹) |
3 | 2 | dgrlem 23789 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
4 | 3 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
5 | 4 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
6 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → 𝐴 Fn
ℕ0) |
7 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (𝐴 Fn ℕ0 →
(𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0})) ↔
(𝑦 ∈
ℕ0 ∧ (𝐴‘𝑦) ∈ (ℂ ∖
{0})))) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → (𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0})) ↔
(𝑦 ∈
ℕ0 ∧ (𝐴‘𝑦) ∈ (ℂ ∖
{0})))) |
9 | 8 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
(𝑦 ∈
ℕ0 ∧ (𝐴‘𝑦) ∈ (ℂ ∖
{0}))) |
10 | 9 | simprd 478 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
(𝐴‘𝑦) ∈ (ℂ ∖
{0})) |
11 | | eldifsni 4261 |
. . . . . . . 8
⊢ ((𝐴‘𝑦) ∈ (ℂ ∖ {0}) → (𝐴‘𝑦) ≠ 0) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
(𝐴‘𝑦) ≠ 0) |
13 | 9 | simpld 474 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
𝑦 ∈
ℕ0) |
14 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
15 | 2 | coef3 23792 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝐴:ℕ0⟶ℂ) |
17 | | plyco0 23752 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑦 ∈ ℕ0
((𝐴‘𝑦) ≠ 0 → 𝑦 ≤ 𝑀))) |
18 | 1, 16, 17 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑦 ∈ ℕ0
((𝐴‘𝑦) ≠ 0 → 𝑦 ≤ 𝑀))) |
19 | 14, 18 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ∀𝑦 ∈ ℕ0
((𝐴‘𝑦) ≠ 0 → 𝑦 ≤ 𝑀)) |
20 | 19 | r19.21bi 2916 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ ℕ0) → ((𝐴‘𝑦) ≠ 0 → 𝑦 ≤ 𝑀)) |
21 | 13, 20 | syldan 486 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
((𝐴‘𝑦) ≠ 0 → 𝑦 ≤ 𝑀)) |
22 | 12, 21 | mpd 15 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
𝑦 ≤ 𝑀) |
23 | 13 | nn0red 11229 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
𝑦 ∈
ℝ) |
24 | 1 | nn0red 11229 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝑀 ∈ ℝ) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
𝑀 ∈
ℝ) |
26 | 23, 25 | lenltd 10062 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
(𝑦 ≤ 𝑀 ↔ ¬ 𝑀 < 𝑦)) |
27 | 22, 26 | mpbid 221 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) ∧ 𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))) →
¬ 𝑀 < 𝑦) |
28 | 27 | ralrimiva 2949 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ∀𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0})) ¬ 𝑀 < 𝑦) |
29 | | nn0ssre 11173 |
. . . . . . 7
⊢
ℕ0 ⊆ ℝ |
30 | | ltso 9997 |
. . . . . . 7
⊢ < Or
ℝ |
31 | | soss 4977 |
. . . . . . 7
⊢
(ℕ0 ⊆ ℝ → ( < Or ℝ →
< Or ℕ0)) |
32 | 29, 30, 31 | mp2 9 |
. . . . . 6
⊢ < Or
ℕ0 |
33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → < Or
ℕ0) |
34 | | 0zd 11266 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 0 ∈
ℤ) |
35 | | cnvimass 5404 |
. . . . . . . 8
⊢ (◡𝐴 “ (ℂ ∖ {0})) ⊆ dom
𝐴 |
36 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐴:ℕ0⟶(𝑆 ∪ {0}) → dom 𝐴 =
ℕ0) |
37 | 4, 36 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → dom 𝐴 = ℕ0) |
38 | 35, 37 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (◡𝐴 “ (ℂ ∖ {0})) ⊆
ℕ0) |
39 | 3 | simprd 478 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
40 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
41 | 40 | uzsupss 11656 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ (◡𝐴 “ (ℂ ∖ {0}))
⊆ ℕ0 ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) → ∃𝑛 ∈ ℕ0 (∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0})) ¬ 𝑛 < 𝑥 ∧ ∀𝑥 ∈ ℕ0 (𝑥 < 𝑛 → ∃𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 < 𝑦))) |
42 | 34, 38, 39, 41 | syl3anc 1318 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
(∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0})) ¬ 𝑛 < 𝑥 ∧ ∀𝑥 ∈ ℕ0 (𝑥 < 𝑛 → ∃𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 < 𝑦))) |
43 | 42 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ∃𝑛 ∈ ℕ0
(∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0})) ¬ 𝑛 < 𝑥 ∧ ∀𝑥 ∈ ℕ0 (𝑥 < 𝑛 → ∃𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 < 𝑦))) |
44 | 33, 43 | supnub 8251 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ((𝑀 ∈ ℕ0 ∧
∀𝑦 ∈ (◡𝐴 “ (ℂ ∖ {0})) ¬ 𝑀 < 𝑦) → ¬ 𝑀 < sup((◡𝐴 “ (ℂ ∖ {0})),
ℕ0, < ))) |
45 | 1, 28, 44 | mp2and 711 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ¬ 𝑀 < sup((◡𝐴 “ (ℂ ∖ {0})),
ℕ0, < )) |
46 | | dgrub.2 |
. . . . . 6
⊢ 𝑁 = (deg‘𝐹) |
47 | 2 | dgrval 23788 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) = sup((◡𝐴 “ (ℂ ∖ {0})),
ℕ0, < )) |
48 | 46, 47 | syl5eq 2656 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑁 = sup((◡𝐴 “ (ℂ ∖ {0})),
ℕ0, < )) |
49 | 48 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝑁 = sup((◡𝐴 “ (ℂ ∖ {0})),
ℕ0, < )) |
50 | 49 | breq2d 4595 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → (𝑀 < 𝑁 ↔ 𝑀 < sup((◡𝐴 “ (ℂ ∖ {0})),
ℕ0, < ))) |
51 | 45, 50 | mtbird 314 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → ¬ 𝑀 < 𝑁) |
52 | | dgrcl 23793 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
53 | 46, 52 | syl5eqel 2692 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
54 | 53 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝑁 ∈
ℕ0) |
55 | 54 | nn0red 11229 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝑁 ∈ ℝ) |
56 | 55, 24 | lenltd 10062 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → (𝑁 ≤ 𝑀 ↔ ¬ 𝑀 < 𝑁)) |
57 | 51, 56 | mpbird 246 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) → 𝑁 ≤ 𝑀) |