Step | Hyp | Ref
| Expression |
1 | | elaa2lem.f |
. . . 4
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)))) |
3 | | zsscn 11385 |
. . . . 5
⊢ ℤ
⊆ ℂ |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ℤ ⊆
ℂ) |
5 | | elaa2lem.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈
(Poly‘ℤ)) |
6 | | dgrcl 23989 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (deg‘𝐺) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
8 | 7 | nn0zd 11480 |
. . . . . . 7
⊢ (𝜑 → (deg‘𝐺) ∈
ℤ) |
9 | | elaa2lem.m |
. . . . . . . . 9
⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) |
10 | | ssrab2 3687 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
ℕ0 |
11 | | nn0uz 11722 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
12 | 10, 11 | sseqtri 3637 |
. . . . . . . . . . . 12
⊢ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0)) |
14 | | elaa2lem.gn0 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
15 | 14 | neneqd 2799 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝐺 = 0𝑝) |
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(deg‘𝐺) =
(deg‘𝐺) |
17 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
18 | 16, 17 | dgreq0 24021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (𝐺 =
0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
19 | 5, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
20 | 15, 19 | mtbid 314 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ ((coeff‘𝐺)‘(deg‘𝐺)) = 0) |
21 | 20 | neqned 2801 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0) |
22 | 7, 21 | jca 554 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ0
∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
23 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺))) |
24 | 23 | neeq1d 2853 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
25 | 24 | elrab 3363 |
. . . . . . . . . . . . 13
⊢
((deg‘𝐺)
∈ {𝑛 ∈
ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0
∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
26 | 22, 25 | sylibr 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
27 | | ne0i 3921 |
. . . . . . . . . . . 12
⊢
((deg‘𝐺)
∈ {𝑛 ∈
ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) |
29 | | infssuzcl 11772 |
. . . . . . . . . . 11
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) |
30 | 13, 28, 29 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) |
31 | 10, 30 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈
ℕ0) |
32 | 9, 31 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
33 | 32 | nn0zd 11480 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
34 | 8, 33 | zsubcld 11487 |
. . . . . 6
⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ) |
35 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )) |
36 | | infssuzle 11771 |
. . . . . . . . 9
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤
(deg‘𝐺)) |
37 | 13, 26, 36 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤
(deg‘𝐺)) |
38 | 35, 37 | eqbrtrd 4675 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺)) |
39 | 7 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → (deg‘𝐺) ∈
ℝ) |
40 | 32 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
41 | 39, 40 | subge0d 10617 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺))) |
42 | 38, 41 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀)) |
43 | 34, 42 | jca 554 |
. . . . 5
⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤
((deg‘𝐺) −
𝑀))) |
44 | | elnn0z 11390 |
. . . . 5
⊢
(((deg‘𝐺)
− 𝑀) ∈
ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤
((deg‘𝐺) −
𝑀))) |
45 | 43, 44 | sylibr 224 |
. . . 4
⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈
ℕ0) |
46 | | id 22 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ 𝐺 ∈
(Poly‘ℤ)) |
47 | | 0zd 11389 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ 0 ∈ ℤ) |
48 | 17 | coef2 23987 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ) |
49 | 46, 47, 48 | syl2anc 693 |
. . . . . . . 8
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (coeff‘𝐺):ℕ0⟶ℤ) |
50 | 5, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℤ) |
51 | 50 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(coeff‘𝐺):ℕ0⟶ℤ) |
52 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
53 | 32 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
54 | 52, 53 | nn0addcld 11355 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈
ℕ0) |
55 | 51, 54 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) |
56 | | elaa2lem.i |
. . . . 5
⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀))) |
57 | 55, 56 | fmptd 6385 |
. . . 4
⊢ (𝜑 → 𝐼:ℕ0⟶ℤ) |
58 | | elplyr 23957 |
. . . 4
⊢ ((ℤ
⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0 ∧ 𝐼:ℕ0⟶ℤ) →
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...((deg‘𝐺) −
𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) |
59 | 4, 45, 57, 58 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) |
60 | 2, 59 | eqeltrd 2701 |
. 2
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
61 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀)) |
62 | 61 | iftrued 4094 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
63 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0) |
64 | 63 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0) |
65 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) |
66 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ) |
67 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ) |
68 | 66, 67 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ) |
69 | | nn0re 11301 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
70 | 69 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ) |
71 | 68, 70 | ltnled 10184 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))) |
72 | 65, 71 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘) |
73 | 66, 67, 70 | ltsubaddd 10623 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀))) |
74 | 72, 73 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀)) |
75 | | olc 399 |
. . . . . . . . . . . . 13
⊢
((deg‘𝐺) <
(𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀))) |
77 | 5 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈
(Poly‘ℤ)) |
78 | 54 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈
ℕ0) |
79 | 16, 17 | dgrlt 24022 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ (𝑘 + 𝑀) ∈ ℕ0)
→ ((𝐺 =
0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))) |
80 | 77, 78, 79 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))) |
81 | 76, 80 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)) |
82 | 81 | simprd 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0) |
83 | 64, 82 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
84 | 62, 83 | pm2.61dan 832 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
85 | 84 | mpteq2dva 4744 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀)))) |
86 | 50, 4 | fssd 6057 |
. . . . . . . . . 10
⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ) |
87 | 86 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ) |
88 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0) |
89 | 88 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0) |
90 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈
ℕ0) |
91 | 89, 90 | nn0addcld 11355 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈
ℕ0) |
92 | 87, 91 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ) |
93 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) →
(0...((deg‘𝐺) −
𝑀)) =
(0...((deg‘𝐺) −
𝑀))) |
94 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑) |
95 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀)))) |
96 | 95, 55 | fvmpt2d 6293 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
97 | 94, 89, 96 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
98 | 97 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
99 | 98 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))) |
100 | 93, 99 | sumeq12rdv 14438 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))) |
101 | 100 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))) |
102 | 2, 101 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))) |
103 | 60, 45, 92, 102 | coeeq2 23998 |
. . . . . . 7
⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0))) |
104 | 85, 103, 95 | 3eqtr4d 2666 |
. . . . . 6
⊢ (𝜑 → (coeff‘𝐹) = 𝐼) |
105 | 104 | fveq1d 6193 |
. . . . 5
⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0)) |
106 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀)) |
107 | 106 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀)) |
108 | 3, 33 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
109 | 108 | addid2d 10237 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 𝑀) = 𝑀) |
110 | 109 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀) |
111 | 107, 110 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀) |
112 | 111 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀)) |
113 | | 0nn0 11307 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
114 | 113 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℕ0) |
115 | 50, 32 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ) |
116 | 95, 112, 114, 115 | fvmptd 6288 |
. . . . 5
⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀)) |
117 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀)) |
118 | 105, 116,
117 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀)) |
119 | 35, 30 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
120 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀)) |
121 | 120 | neeq1d 2853 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0)) |
122 | 121 | elrab 3363 |
. . . . . 6
⊢ (𝑀 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑀) ≠ 0)) |
123 | 119, 122 | sylib 208 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑀) ≠ 0)) |
124 | 123 | simprd 479 |
. . . 4
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0) |
125 | 118, 124 | eqnetrd 2861 |
. . 3
⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠
0) |
126 | 5, 47 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
127 | | aasscn 24073 |
. . . . . . . . . . 11
⊢ 𝔸
⊆ ℂ |
128 | | elaa2lem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝔸) |
129 | 127, 128 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
130 | 94, 129 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ) |
131 | 130, 89 | expcld 13008 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ) |
132 | 92, 131 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ) |
133 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 − 𝑀) → (𝑘 + 𝑀) = ((𝑗 − 𝑀) + 𝑀)) |
134 | 133 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀))) |
135 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀))) |
136 | 134, 135 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
137 | 33, 126, 34, 132, 136 | fsumshft 14512 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
138 | 3, 8 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → (deg‘𝐺) ∈
ℂ) |
139 | 138, 108 | npcand 10396 |
. . . . . . . . 9
⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺)) |
140 | 109, 139 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺))) |
141 | 140 | sumeq1d 14431 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
142 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ) |
144 | 3, 143 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ) |
145 | 108 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ) |
146 | 144, 145 | npcand 10396 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗) |
147 | 146 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗)) |
148 | 147 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀)))) |
149 | 129 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ∈ ℂ) |
150 | | elaa2lem.an0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≠ 0) |
151 | 150 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ≠ 0) |
152 | 33 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℤ) |
153 | 149, 151,
152, 143 | expsubd 13019 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀))) |
154 | 153 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀)))) |
155 | 86 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ) |
156 | | 0red 10041 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈
ℝ) |
157 | 40 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ) |
158 | 143 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ) |
159 | 32 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ 𝑀) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀) |
161 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗) |
162 | 161 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗) |
163 | 156, 157,
158, 160, 162 | letrd 10194 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗) |
164 | 143, 163 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) |
165 | | elnn0z 11390 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
↔ (𝑗 ∈ ℤ
∧ 0 ≤ 𝑗)) |
166 | 164, 165 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
167 | 155, 166 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ) |
168 | 149, 166 | expcld 13008 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ) |
169 | 129, 32 | expcld 13008 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ) |
170 | 169 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ) |
171 | 149, 151,
152 | expne0d 13014 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0) |
172 | 167, 168,
170, 171 | divassd 10836 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀)))) |
173 | 172 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
174 | 154, 173 | eqtr2d 2657 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀)))) |
175 | 148, 174 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
176 | 175 | sumeq2dv 14433 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
177 | 141, 176 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
178 | 32, 11 | syl6eleq 2711 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
179 | | fzss1 12380 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺))) |
180 | 178, 179 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺))) |
181 | 167, 168 | mulcld 10060 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ) |
182 | 181, 170,
171 | divcld 10801 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ) |
183 | 33 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ) |
184 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ) |
185 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺))) |
186 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ0) |
187 | 186 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℤ) |
188 | 185, 187 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ) |
189 | 188 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ) |
190 | 183, 184,
189 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈
ℤ)) |
191 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀) |
192 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ) |
193 | 189 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ) |
194 | 192, 193 | lenltd 10183 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀)) |
195 | 191, 194 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗) |
196 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺)) |
197 | 185, 196 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺)) |
198 | 197 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺)) |
199 | 190, 195,
198 | jca32 558 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ((𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (𝑀 ≤ 𝑗 ∧ 𝑗 ≤ (deg‘𝐺)))) |
200 | | elfz2 12333 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) ↔ ((𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (𝑀 ≤ 𝑗 ∧ 𝑗 ≤ (deg‘𝐺)))) |
201 | 199, 200 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺))) |
202 | | eldifn 3733 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺))) |
203 | 202 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺))) |
204 | 201, 203 | condan 835 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 < 𝑀) |
205 | 204 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 < 𝑀) |
206 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )) |
207 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0)) |
208 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
209 | 208 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ0) |
210 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
((coeff‘𝐺)‘𝑗) = 0 → ((coeff‘𝐺)‘𝑗) ≠ 0) |
211 | 210 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ((coeff‘𝐺)‘𝑗) ≠ 0) |
212 | 209, 211 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑗 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑗) ≠ 0)) |
213 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗)) |
214 | 213 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0)) |
215 | 214 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑗) ≠ 0)) |
216 | 212, 215 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
217 | 216 | adantll 750 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
218 | | infssuzle 11771 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗) |
219 | 207, 217,
218 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗) |
220 | 206, 219 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗) |
221 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ) |
222 | 188 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ) |
223 | 222 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ) |
224 | 221, 223 | lenltd 10183 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀)) |
225 | 220, 224 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀) |
226 | 205, 225 | condan 835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0) |
227 | 226 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = (0 · (𝐴↑𝑗))) |
228 | 129 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ) |
229 | 208 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ0) |
230 | 228, 229 | expcld 13008 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ) |
231 | 230 | mul02d 10234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0) |
232 | 227, 231 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0) |
233 | 232 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀))) |
234 | 129, 150,
33 | expne0d 13014 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑𝑀) ≠ 0) |
235 | 169, 234 | div0d 10800 |
. . . . . . . . 9
⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0) |
236 | 235 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0) |
237 | 233, 236 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0) |
238 | | fzfid 12772 |
. . . . . . 7
⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin) |
239 | 180, 182,
237, 238 | fsumss 14456 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
240 | 137, 177,
239 | 3eqtrd 2660 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
241 | 89, 55 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) |
242 | 56 | fvmpt2 6291 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
243 | 89, 241, 242 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
244 | 243 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
245 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘)) |
246 | 245 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘)) |
247 | 244, 246 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
248 | 247 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
249 | | fzfid 12772 |
. . . . . . 7
⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin) |
250 | 249, 132 | fsumcl 14464 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ) |
251 | 2, 248, 129, 250 | fvmptd 6288 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
252 | 17, 16 | coeid2 23995 |
. . . . . . . 8
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ 𝐴 ∈ ℂ)
→ (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗))) |
253 | 5, 129, 252 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗))) |
254 | 253 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
255 | 86 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ) |
256 | 186 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
257 | 255, 256 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ) |
258 | 129 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ) |
259 | 258, 256 | expcld 13008 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ) |
260 | 257, 259 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ) |
261 | 238, 169,
260, 234 | fsumdivc 14518 |
. . . . . 6
⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
262 | 254, 261 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
263 | 240, 251,
262 | 3eqtr4d 2666 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀))) |
264 | | elaa2lem.ga |
. . . . 5
⊢ (𝜑 → (𝐺‘𝐴) = 0) |
265 | 264 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀))) |
266 | 263, 265,
235 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
267 | 125, 266 | jca 554 |
. 2
⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) |
268 | | fveq2 6191 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹)) |
269 | 268 | fveq1d 6193 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0)) |
270 | 269 | neeq1d 2853 |
. . . 4
⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠
0)) |
271 | | fveq1 6190 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴)) |
272 | 271 | eqeq1d 2624 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0)) |
273 | 270, 272 | anbi12d 747 |
. . 3
⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))) |
274 | 273 | rspcev 3309 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
275 | 60, 267, 274 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |