Step | Hyp | Ref
| Expression |
1 | | elaa2lem.f |
. . . 4
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)))) |
3 | | zsscn 11719 |
. . . . 5
⊢ ℤ
⊆ ℂ |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ℤ ⊆
ℂ) |
5 | | elaa2lem.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈
(Poly‘ℤ)) |
6 | | dgrcl 24395 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (deg‘𝐺) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
8 | 7 | nn0zd 11815 |
. . . . . . 7
⊢ (𝜑 → (deg‘𝐺) ∈
ℤ) |
9 | | elaa2lem.m |
. . . . . . . . 9
⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) |
10 | | ssrab2 3914 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
ℕ0 |
11 | | nn0uz 12011 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
12 | 10, 11 | sseqtri 3862 |
. . . . . . . . . . . 12
⊢ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0)) |
14 | | elaa2lem.gn0 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
15 | 14 | neneqd 3004 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝐺 = 0𝑝) |
16 | | eqid 2825 |
. . . . . . . . . . . . . . . . . 18
⊢
(deg‘𝐺) =
(deg‘𝐺) |
17 | | eqid 2825 |
. . . . . . . . . . . . . . . . . 18
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
18 | 16, 17 | dgreq0 24427 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (𝐺 =
0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
19 | 5, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
20 | 15, 19 | mtbid 316 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ ((coeff‘𝐺)‘(deg‘𝐺)) = 0) |
21 | 20 | neqned 3006 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0) |
22 | 7, 21 | jca 507 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ0
∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
23 | | fveq2 6437 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺))) |
24 | 23 | neeq1d 3058 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
25 | 24 | elrab 3585 |
. . . . . . . . . . . . 13
⊢
((deg‘𝐺)
∈ {𝑛 ∈
ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0
∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
26 | 22, 25 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
27 | 26 | ne0d 4153 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) |
28 | | infssuzcl 12062 |
. . . . . . . . . . 11
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) |
29 | 13, 27, 28 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) |
30 | 10, 29 | sseldi 3825 |
. . . . . . . . 9
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈
ℕ0) |
31 | 9, 30 | syl5eqel 2910 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
32 | 31 | nn0zd 11815 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
33 | 8, 32 | zsubcld 11822 |
. . . . . 6
⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ) |
34 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )) |
35 | | infssuzle 12061 |
. . . . . . . . 9
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤
(deg‘𝐺)) |
36 | 13, 26, 35 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤
(deg‘𝐺)) |
37 | 34, 36 | eqbrtrd 4897 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺)) |
38 | 7 | nn0red 11686 |
. . . . . . . 8
⊢ (𝜑 → (deg‘𝐺) ∈
ℝ) |
39 | 31 | nn0red 11686 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
40 | 38, 39 | subge0d 10949 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺))) |
41 | 37, 40 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀)) |
42 | 33, 41 | jca 507 |
. . . . 5
⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤
((deg‘𝐺) −
𝑀))) |
43 | | elnn0z 11724 |
. . . . 5
⊢
(((deg‘𝐺)
− 𝑀) ∈
ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤
((deg‘𝐺) −
𝑀))) |
44 | 42, 43 | sylibr 226 |
. . . 4
⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈
ℕ0) |
45 | | id 22 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ 𝐺 ∈
(Poly‘ℤ)) |
46 | | 0zd 11723 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ 0 ∈ ℤ) |
47 | 17 | coef2 24393 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ) |
48 | 45, 46, 47 | syl2anc 579 |
. . . . . . . 8
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (coeff‘𝐺):ℕ0⟶ℤ) |
49 | 5, 48 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℤ) |
50 | 49 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(coeff‘𝐺):ℕ0⟶ℤ) |
51 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
52 | 31 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
53 | 51, 52 | nn0addcld 11689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈
ℕ0) |
54 | 50, 53 | ffvelrnd 6614 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) |
55 | | elaa2lem.i |
. . . . 5
⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀))) |
56 | 54, 55 | fmptd 6638 |
. . . 4
⊢ (𝜑 → 𝐼:ℕ0⟶ℤ) |
57 | | elplyr 24363 |
. . . 4
⊢ ((ℤ
⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0 ∧ 𝐼:ℕ0⟶ℤ) →
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...((deg‘𝐺) −
𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) |
58 | 4, 44, 56, 57 | syl3anc 1494 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) |
59 | 2, 58 | eqeltrd 2906 |
. 2
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
60 | | simpr 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀)) |
61 | 60 | iftrued 4316 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
62 | | iffalse 4317 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0) |
63 | 62 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0) |
64 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) |
65 | 38 | ad2antrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ) |
66 | 39 | ad2antrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ) |
67 | 65, 66 | resubcld 10789 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ) |
68 | | nn0re 11635 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
69 | 68 | ad2antlr 718 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ) |
70 | 67, 69 | ltnled 10510 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))) |
71 | 64, 70 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘) |
72 | 65, 66, 69 | ltsubaddd 10955 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀))) |
73 | 71, 72 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀)) |
74 | | olc 899 |
. . . . . . . . . . . . 13
⊢
((deg‘𝐺) <
(𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀))) |
76 | 5 | ad2antrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈
(Poly‘ℤ)) |
77 | 53 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈
ℕ0) |
78 | 16, 17 | dgrlt 24428 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ (𝑘 + 𝑀) ∈ ℕ0)
→ ((𝐺 =
0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))) |
79 | 76, 77, 78 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))) |
80 | 75, 79 | mpbid 224 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)) |
81 | 80 | simprd 491 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0) |
82 | 63, 81 | eqtr4d 2864 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
83 | 61, 82 | pm2.61dan 847 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
84 | 83 | mpteq2dva 4969 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀)))) |
85 | 49, 4 | fssd 6296 |
. . . . . . . . . 10
⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ) |
86 | 85 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ) |
87 | | elfznn0 12734 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0) |
88 | 87 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0) |
89 | 31 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈
ℕ0) |
90 | 88, 89 | nn0addcld 11689 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈
ℕ0) |
91 | 86, 90 | ffvelrnd 6614 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ) |
92 | | eqidd 2826 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) →
(0...((deg‘𝐺) −
𝑀)) =
(0...((deg‘𝐺) −
𝑀))) |
93 | | simpl 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑) |
94 | 55 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀)))) |
95 | 94, 54 | fvmpt2d 6545 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
96 | 93, 88, 95 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
97 | 96 | adantlr 706 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
98 | 97 | oveq1d 6925 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))) |
99 | 92, 98 | sumeq12rdv 14822 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))) |
100 | 99 | mpteq2dva 4969 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))) |
101 | 2, 100 | eqtrd 2861 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))) |
102 | 59, 44, 91, 101 | coeeq2 24404 |
. . . . . . 7
⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0))) |
103 | 84, 102, 94 | 3eqtr4d 2871 |
. . . . . 6
⊢ (𝜑 → (coeff‘𝐹) = 𝐼) |
104 | 103 | fveq1d 6439 |
. . . . 5
⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0)) |
105 | | oveq1 6917 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀)) |
106 | 105 | adantl 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀)) |
107 | 3, 32 | sseldi 3825 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
108 | 107 | addid2d 10563 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 𝑀) = 𝑀) |
109 | 108 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀) |
110 | 106, 109 | eqtrd 2861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀) |
111 | 110 | fveq2d 6441 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀)) |
112 | | 0nn0 11642 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
113 | 112 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℕ0) |
114 | 49, 31 | ffvelrnd 6614 |
. . . . . 6
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ) |
115 | 94, 111, 113, 114 | fvmptd 6539 |
. . . . 5
⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀)) |
116 | | eqidd 2826 |
. . . . 5
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀)) |
117 | 104, 115,
116 | 3eqtrd 2865 |
. . . 4
⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀)) |
118 | 34, 29 | eqeltrd 2906 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
119 | | fveq2 6437 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀)) |
120 | 119 | neeq1d 3058 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0)) |
121 | 120 | elrab 3585 |
. . . . . 6
⊢ (𝑀 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑀) ≠ 0)) |
122 | 118, 121 | sylib 210 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑀) ≠ 0)) |
123 | 122 | simprd 491 |
. . . 4
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0) |
124 | 117, 123 | eqnetrd 3066 |
. . 3
⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠
0) |
125 | 5, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
126 | | aasscn 24479 |
. . . . . . . . . . 11
⊢ 𝔸
⊆ ℂ |
127 | | elaa2lem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝔸) |
128 | 126, 127 | sseldi 3825 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
129 | 93, 128 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ) |
130 | 129, 88 | expcld 13309 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ) |
131 | 91, 130 | mulcld 10384 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ) |
132 | | fvoveq1 6933 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀))) |
133 | | oveq2 6918 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀))) |
134 | 132, 133 | oveq12d 6928 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
135 | 32, 125, 33, 131, 134 | fsumshft 14893 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
136 | 3, 8 | sseldi 3825 |
. . . . . . . . . 10
⊢ (𝜑 → (deg‘𝐺) ∈
ℂ) |
137 | 136, 107 | npcand 10724 |
. . . . . . . . 9
⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺)) |
138 | 108, 137 | oveq12d 6928 |
. . . . . . . 8
⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺))) |
139 | 138 | sumeq1d 14815 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
140 | | elfzelz 12642 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ) |
141 | 140 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ) |
142 | 3, 141 | sseldi 3825 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ) |
143 | 107 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ) |
144 | 142, 143 | npcand 10724 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗) |
145 | 144 | fveq2d 6441 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗)) |
146 | 145 | oveq1d 6925 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀)))) |
147 | 128 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ∈ ℂ) |
148 | | elaa2lem.an0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≠ 0) |
149 | 148 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ≠ 0) |
150 | 32 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℤ) |
151 | 147, 149,
150, 141 | expsubd 13320 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀))) |
152 | 151 | oveq2d 6926 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀)))) |
153 | 85 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ) |
154 | | 0red 10367 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈
ℝ) |
155 | 39 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ) |
156 | 141 | zred 11817 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ) |
157 | 31 | nn0ge0d 11688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ 𝑀) |
158 | 157 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀) |
159 | | elfzle1 12644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗) |
160 | 159 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗) |
161 | 154, 155,
156, 158, 160 | letrd 10520 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗) |
162 | 141, 161 | jca 507 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) |
163 | | elnn0z 11724 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
↔ (𝑗 ∈ ℤ
∧ 0 ≤ 𝑗)) |
164 | 162, 163 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
165 | 153, 164 | ffvelrnd 6614 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ) |
166 | 147, 164 | expcld 13309 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ) |
167 | 128, 31 | expcld 13309 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ) |
168 | 167 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ) |
169 | 147, 149,
150 | expne0d 13315 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0) |
170 | 165, 166,
168, 169 | divassd 11169 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀)))) |
171 | 170 | eqcomd 2831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
172 | 152, 171 | eqtr2d 2862 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀)))) |
173 | 146, 172 | eqtr4d 2864 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
174 | 173 | sumeq2dv 14817 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
175 | 139, 174 | eqtrd 2861 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
176 | 31, 11 | syl6eleq 2916 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
177 | | fzss1 12680 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺))) |
178 | 176, 177 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺))) |
179 | 165, 166 | mulcld 10384 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ) |
180 | 179, 168,
169 | divcld 11134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ) |
181 | 32 | ad2antrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ) |
182 | 8 | ad2antrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ) |
183 | | eldifi 3961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺))) |
184 | | elfznn0 12734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ0) |
185 | 184 | nn0zd 11815 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℤ) |
186 | 183, 185 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ) |
187 | 186 | ad2antlr 718 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ) |
188 | 181, 182,
187 | 3jca 1162 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈
ℤ)) |
189 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀) |
190 | 39 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ) |
191 | 187 | zred 11817 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ) |
192 | 190, 191 | lenltd 10509 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀)) |
193 | 189, 192 | mpbird 249 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗) |
194 | | elfzle2 12645 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺)) |
195 | 183, 194 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺)) |
196 | 195 | ad2antlr 718 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺)) |
197 | 188, 193,
196 | jca32 511 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ((𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (𝑀 ≤ 𝑗 ∧ 𝑗 ≤ (deg‘𝐺)))) |
198 | | elfz2 12633 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) ↔ ((𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (𝑀 ≤ 𝑗 ∧ 𝑗 ≤ (deg‘𝐺)))) |
199 | 197, 198 | sylibr 226 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺))) |
200 | | eldifn 3962 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺))) |
201 | 200 | ad2antlr 718 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺))) |
202 | 199, 201 | condan 852 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 < 𝑀) |
203 | 202 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 < 𝑀) |
204 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )) |
205 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0)) |
206 | 183, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
207 | 206 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ0) |
208 | | neqne 3007 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
((coeff‘𝐺)‘𝑗) = 0 → ((coeff‘𝐺)‘𝑗) ≠ 0) |
209 | 208 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ((coeff‘𝐺)‘𝑗) ≠ 0) |
210 | 207, 209 | jca 507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑗 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑗) ≠ 0)) |
211 | | fveq2 6437 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗)) |
212 | 211 | neeq1d 3058 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0)) |
213 | 212 | elrab 3585 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑗) ≠ 0)) |
214 | 210, 213 | sylibr 226 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
215 | 214 | adantll 705 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
216 | | infssuzle 12061 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗) |
217 | 205, 215,
216 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗) |
218 | 204, 217 | eqbrtrd 4897 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗) |
219 | 39 | ad2antrr 717 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ) |
220 | 186 | zred 11817 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ) |
221 | 220 | ad2antlr 718 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ) |
222 | 219, 221 | lenltd 10509 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀)) |
223 | 218, 222 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀) |
224 | 203, 223 | condan 852 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0) |
225 | 224 | oveq1d 6925 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = (0 · (𝐴↑𝑗))) |
226 | 128 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ) |
227 | 206 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ0) |
228 | 226, 227 | expcld 13309 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ) |
229 | 228 | mul02d 10560 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0) |
230 | 225, 229 | eqtrd 2861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0) |
231 | 230 | oveq1d 6925 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀))) |
232 | 128, 148,
32 | expne0d 13315 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑𝑀) ≠ 0) |
233 | 167, 232 | div0d 11133 |
. . . . . . . . 9
⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0) |
234 | 233 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0) |
235 | 231, 234 | eqtrd 2861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0) |
236 | | fzfid 13074 |
. . . . . . 7
⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin) |
237 | 178, 180,
235, 236 | fsumss 14840 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
238 | 135, 175,
237 | 3eqtrd 2865 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
239 | 88, 54 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) |
240 | 55 | fvmpt2 6543 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
241 | 88, 239, 240 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
242 | 241 | adantlr 706 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
243 | | oveq1 6917 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘)) |
244 | 243 | ad2antlr 718 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘)) |
245 | 242, 244 | oveq12d 6928 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
246 | 245 | sumeq2dv 14817 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
247 | | fzfid 13074 |
. . . . . . 7
⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin) |
248 | 247, 131 | fsumcl 14848 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ) |
249 | 2, 246, 128, 248 | fvmptd 6539 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
250 | 17, 16 | coeid2 24401 |
. . . . . . . 8
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ 𝐴 ∈ ℂ)
→ (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗))) |
251 | 5, 128, 250 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗))) |
252 | 251 | oveq1d 6925 |
. . . . . 6
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
253 | 85 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ) |
254 | 184 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
255 | 253, 254 | ffvelrnd 6614 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ) |
256 | 128 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ) |
257 | 256, 254 | expcld 13309 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ) |
258 | 255, 257 | mulcld 10384 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ) |
259 | 236, 167,
258, 232 | fsumdivc 14899 |
. . . . . 6
⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
260 | 252, 259 | eqtrd 2861 |
. . . . 5
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
261 | 238, 249,
260 | 3eqtr4d 2871 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀))) |
262 | | elaa2lem.ga |
. . . . 5
⊢ (𝜑 → (𝐺‘𝐴) = 0) |
263 | 262 | oveq1d 6925 |
. . . 4
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀))) |
264 | 261, 263,
233 | 3eqtrd 2865 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
265 | 124, 264 | jca 507 |
. 2
⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) |
266 | | fveq2 6437 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹)) |
267 | 266 | fveq1d 6439 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0)) |
268 | 267 | neeq1d 3058 |
. . . 4
⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠
0)) |
269 | | fveq1 6436 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴)) |
270 | 269 | eqeq1d 2827 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0)) |
271 | 268, 270 | anbi12d 624 |
. . 3
⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))) |
272 | 271 | rspcev 3526 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
273 | 59, 265, 272 | syl2anc 579 |
1
⊢ (𝜑 → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |