| Step | Hyp | Ref
| Expression |
| 1 | | elaa2lem.f |
. . . 4
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)))) |
| 3 | | zsscn 12621 |
. . . . 5
⊢ ℤ
⊆ ℂ |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ℤ ⊆
ℂ) |
| 5 | | elaa2lem.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈
(Poly‘ℤ)) |
| 6 | | dgrcl 26272 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (deg‘𝐺) ∈
ℕ0) |
| 7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
| 8 | 7 | nn0zd 12639 |
. . . . . . 7
⊢ (𝜑 → (deg‘𝐺) ∈
ℤ) |
| 9 | | elaa2lem.m |
. . . . . . . . 9
⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) |
| 10 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
ℕ0 |
| 11 | | nn0uz 12920 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
| 12 | 10, 11 | sseqtri 4032 |
. . . . . . . . . . . 12
⊢ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) |
| 13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0)) |
| 14 | | elaa2lem.gn0 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
| 15 | 14 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝐺 = 0𝑝) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(deg‘𝐺) =
(deg‘𝐺) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
| 18 | 16, 17 | dgreq0 26305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (Poly‘ℤ)
→ (𝐺 =
0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
| 19 | 5, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 = 0𝑝 ↔
((coeff‘𝐺)‘(deg‘𝐺)) = 0)) |
| 20 | 15, 19 | mtbid 324 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ ((coeff‘𝐺)‘(deg‘𝐺)) = 0) |
| 21 | 20 | neqned 2947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0) |
| 22 | 7, 21 | jca 511 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((deg‘𝐺) ∈ ℕ0
∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
| 23 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺))) |
| 24 | 23 | neeq1d 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
| 25 | 24 | elrab 3692 |
. . . . . . . . . . . . 13
⊢
((deg‘𝐺)
∈ {𝑛 ∈
ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0
∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)) |
| 26 | 22, 25 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
| 27 | 26 | ne0d 4342 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) |
| 28 | | infssuzcl 12974 |
. . . . . . . . . . 11
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) |
| 29 | 13, 27, 28 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) |
| 30 | 10, 29 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈
ℕ0) |
| 31 | 9, 30 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 32 | 31 | nn0zd 12639 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 33 | 8, 32 | zsubcld 12727 |
. . . . . 6
⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ) |
| 34 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )) |
| 35 | | infssuzle 12973 |
. . . . . . . . 9
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤
(deg‘𝐺)) |
| 36 | 13, 26, 35 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤
(deg‘𝐺)) |
| 37 | 34, 36 | eqbrtrd 5165 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≤ (deg‘𝐺)) |
| 38 | 7 | nn0red 12588 |
. . . . . . . 8
⊢ (𝜑 → (deg‘𝐺) ∈
ℝ) |
| 39 | 31 | nn0red 12588 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 40 | 38, 39 | subge0d 11853 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺))) |
| 41 | 37, 40 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀)) |
| 42 | 33, 41 | jca 511 |
. . . . 5
⊢ (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤
((deg‘𝐺) −
𝑀))) |
| 43 | | elnn0z 12626 |
. . . . 5
⊢
(((deg‘𝐺)
− 𝑀) ∈
ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤
((deg‘𝐺) −
𝑀))) |
| 44 | 42, 43 | sylibr 234 |
. . . 4
⊢ (𝜑 → ((deg‘𝐺) − 𝑀) ∈
ℕ0) |
| 45 | | 0zd 12625 |
. . . . . . . 8
⊢ (𝐺 ∈ (Poly‘ℤ)
→ 0 ∈ ℤ) |
| 46 | 17 | coef2 26270 |
. . . . . . . 8
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ) |
| 47 | 5, 45, 46 | syl2anc2 585 |
. . . . . . 7
⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℤ) |
| 48 | 47 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(coeff‘𝐺):ℕ0⟶ℤ) |
| 49 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
| 50 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
| 51 | 49, 50 | nn0addcld 12591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈
ℕ0) |
| 52 | 48, 51 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) |
| 53 | | elaa2lem.i |
. . . . 5
⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 54 | 52, 53 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝐼:ℕ0⟶ℤ) |
| 55 | | elplyr 26240 |
. . . 4
⊢ ((ℤ
⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0 ∧ 𝐼:ℕ0⟶ℤ) →
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...((deg‘𝐺) −
𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) |
| 56 | 4, 44, 54, 55 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) |
| 57 | 2, 56 | eqeltrd 2841 |
. 2
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
| 58 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀)) |
| 59 | 58 | iftrued 4533 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 60 | | iffalse 4534 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0) |
| 61 | 60 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0) |
| 62 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) |
| 63 | 38 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ) |
| 64 | 39 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ) |
| 65 | 63, 64 | resubcld 11691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ) |
| 66 | | nn0re 12535 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
| 67 | 66 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ) |
| 68 | 65, 67 | ltnled 11408 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))) |
| 69 | 62, 68 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘) |
| 70 | 63, 64, 67 | ltsubaddd 11859 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀))) |
| 71 | 69, 70 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀)) |
| 72 | | olc 869 |
. . . . . . . . . . . . 13
⊢
((deg‘𝐺) <
(𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀))) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀))) |
| 74 | 5 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈
(Poly‘ℤ)) |
| 75 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈
ℕ0) |
| 76 | 16, 17 | dgrlt 26306 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ (𝑘 + 𝑀) ∈ ℕ0)
→ ((𝐺 =
0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))) |
| 77 | 74, 75, 76 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0𝑝 ∨
(deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))) |
| 78 | 73, 77 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)) |
| 79 | 78 | simprd 495 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0) |
| 80 | 61, 79 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 81 | 59, 80 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 82 | 81 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀)))) |
| 83 | 47, 4 | fssd 6753 |
. . . . . . . . . 10
⊢ (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ) |
| 84 | 83 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ) |
| 85 | | elfznn0 13660 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0) |
| 86 | 85 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0) |
| 87 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈
ℕ0) |
| 88 | 86, 87 | nn0addcld 12591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈
ℕ0) |
| 89 | 84, 88 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ) |
| 90 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) →
(0...((deg‘𝐺) −
𝑀)) =
(0...((deg‘𝐺) −
𝑀))) |
| 91 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑) |
| 92 | 53 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 = (𝑘 ∈ ℕ0 ↦
((coeff‘𝐺)‘(𝑘 + 𝑀)))) |
| 93 | 92, 52 | fvmpt2d 7029 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 94 | 91, 86, 93 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 95 | 94 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 96 | 95 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))) |
| 97 | 90, 96 | sumeq12rdv 15743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘))) |
| 98 | 97 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))) |
| 99 | 2, 98 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧↑𝑘)))) |
| 100 | 57, 44, 89, 99 | coeeq2 26281 |
. . . . . . 7
⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0))) |
| 101 | 82, 100, 92 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝜑 → (coeff‘𝐹) = 𝐼) |
| 102 | 101 | fveq1d 6908 |
. . . . 5
⊢ (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0)) |
| 103 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀)) |
| 104 | 103 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀)) |
| 105 | 3, 32 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 106 | 105 | addlidd 11462 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 𝑀) = 𝑀) |
| 107 | 106 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 0) → (0 + 𝑀) = 𝑀) |
| 108 | 104, 107 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 + 𝑀) = 𝑀) |
| 109 | 108 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀)) |
| 110 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 111 | 110 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℕ0) |
| 112 | 47, 31 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ) |
| 113 | 92, 109, 111, 112 | fvmptd 7023 |
. . . . 5
⊢ (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀)) |
| 114 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀)) |
| 115 | 102, 113,
114 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀)) |
| 116 | 34, 29 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
| 117 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀)) |
| 118 | 117 | neeq1d 3000 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0)) |
| 119 | 118 | elrab 3692 |
. . . . . 6
⊢ (𝑀 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑀) ≠ 0)) |
| 120 | 116, 119 | sylib 218 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑀) ≠ 0)) |
| 121 | 120 | simprd 495 |
. . . 4
⊢ (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0) |
| 122 | 115, 121 | eqnetrd 3008 |
. . 3
⊢ (𝜑 → ((coeff‘𝐹)‘0) ≠
0) |
| 123 | 5, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
| 124 | | aasscn 26360 |
. . . . . . . . . . 11
⊢ 𝔸
⊆ ℂ |
| 125 | | elaa2lem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝔸) |
| 126 | 124, 125 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 127 | 91, 126 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ) |
| 128 | 127, 86 | expcld 14186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴↑𝑘) ∈ ℂ) |
| 129 | 89, 128 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ) |
| 130 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀))) |
| 131 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑗 − 𝑀))) |
| 132 | 130, 131 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
| 133 | 32, 123, 33, 129, 132 | fsumshft 15816 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
| 134 | 3, 8 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → (deg‘𝐺) ∈
ℂ) |
| 135 | 134, 105 | npcand 11624 |
. . . . . . . . 9
⊢ (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺)) |
| 136 | 106, 135 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺))) |
| 137 | 136 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀)))) |
| 138 | | elfzelz 13564 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ) |
| 139 | 138 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ) |
| 140 | 3, 139 | sselid 3981 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ) |
| 141 | 105 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ) |
| 142 | 140, 141 | npcand 11624 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗 − 𝑀) + 𝑀) = 𝑗) |
| 143 | 142 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗)) |
| 144 | 143 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀)))) |
| 145 | 126 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ∈ ℂ) |
| 146 | | elaa2lem.an0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≠ 0) |
| 147 | 146 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ≠ 0) |
| 148 | 32 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℤ) |
| 149 | 145, 147,
148, 139 | expsubd 14197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗 − 𝑀)) = ((𝐴↑𝑗) / (𝐴↑𝑀))) |
| 150 | 149 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀)))) |
| 151 | 83 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ) |
| 152 | | 0red 11264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈
ℝ) |
| 153 | 39 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ) |
| 154 | 139 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ) |
| 155 | 31 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ 𝑀) |
| 156 | 155 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀) |
| 157 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀 ≤ 𝑗) |
| 158 | 157 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ≤ 𝑗) |
| 159 | 152, 153,
154, 156, 158 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗) |
| 160 | 139, 159 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) |
| 161 | | elnn0z 12626 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
↔ (𝑗 ∈ ℤ
∧ 0 ≤ 𝑗)) |
| 162 | 160, 161 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
| 163 | 151, 162 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ) |
| 164 | 145, 162 | expcld 14186 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ) |
| 165 | 126, 31 | expcld 14186 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ) |
| 166 | 165 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ∈ ℂ) |
| 167 | 145, 147,
148 | expne0d 14192 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑𝑀) ≠ 0) |
| 168 | 163, 164,
166, 167 | divassd 12078 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀)))) |
| 169 | 168 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴↑𝑗) / (𝐴↑𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 170 | 150, 169 | eqtr2d 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗 − 𝑀)))) |
| 171 | 144, 170 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 172 | 171 | sumeq2dv 15738 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 173 | 137, 172 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗 − 𝑀) + 𝑀)) · (𝐴↑(𝑗 − 𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 174 | 31, 11 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
| 175 | | fzss1 13603 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺))) |
| 176 | 174, 175 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺))) |
| 177 | 163, 164 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ) |
| 178 | 177, 166,
167 | divcld 12043 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) ∈ ℂ) |
| 179 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ) |
| 180 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ) |
| 181 | | eldifi 4131 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺))) |
| 182 | 181 | elfzelzd 13565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ) |
| 183 | 182 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ) |
| 184 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀) |
| 185 | 39 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ) |
| 186 | 183 | zred 12722 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ) |
| 187 | 185, 186 | lenltd 11407 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀)) |
| 188 | 184, 187 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ≤ 𝑗) |
| 189 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺)) |
| 190 | 181, 189 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺)) |
| 191 | 190 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺)) |
| 192 | 179, 180,
183, 188, 191 | elfzd 13555 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺))) |
| 193 | | eldifn 4132 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺))) |
| 194 | 193 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺))) |
| 195 | 192, 194 | condan 818 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 < 𝑀) |
| 196 | 195 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 < 𝑀) |
| 197 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 = inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )) |
| 198 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0)) |
| 199 | | elfznn0 13660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ0) |
| 200 | 181, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
| 201 | 200 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ0) |
| 202 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
((coeff‘𝐺)‘𝑗) = 0 → ((coeff‘𝐺)‘𝑗) ≠ 0) |
| 203 | 202 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ((coeff‘𝐺)‘𝑗) ≠ 0) |
| 204 | 201, 203 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑗 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑗) ≠ 0)) |
| 205 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗)) |
| 206 | 205 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0)) |
| 207 | 206 | elrab 3692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧
((coeff‘𝐺)‘𝑗) ≠ 0)) |
| 208 | 204, 207 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
| 209 | 208 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) |
| 210 | | infssuzle 12973 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛 ∈ ℕ0
∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆
(ℤ≥‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗) |
| 211 | 198, 209,
210 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣
((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗) |
| 212 | 197, 211 | eqbrtrd 5165 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ≤ 𝑗) |
| 213 | 39 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ) |
| 214 | 182 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ) |
| 215 | 214 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ) |
| 216 | 213, 215 | lenltd 11407 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀)) |
| 217 | 212, 216 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀) |
| 218 | 196, 217 | condan 818 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0) |
| 219 | 218 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = (0 · (𝐴↑𝑗))) |
| 220 | 126 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ) |
| 221 | 200 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ0) |
| 222 | 220, 221 | expcld 14186 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴↑𝑗) ∈ ℂ) |
| 223 | 222 | mul02d 11459 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴↑𝑗)) = 0) |
| 224 | 219, 223 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) = 0) |
| 225 | 224 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀))) |
| 226 | 126, 146,
32 | expne0d 14192 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑𝑀) ≠ 0) |
| 227 | 165, 226 | div0d 12042 |
. . . . . . . . 9
⊢ (𝜑 → (0 / (𝐴↑𝑀)) = 0) |
| 228 | 227 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴↑𝑀)) = 0) |
| 229 | 225, 228 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = 0) |
| 230 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (0...(deg‘𝐺)) ∈ Fin) |
| 231 | 176, 178,
229, 230 | fsumss 15761 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 232 | 133, 173,
231 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 233 | 86, 52 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) |
| 234 | 53 | fvmpt2 7027 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 235 | 86, 233, 234 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 236 | 235 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼‘𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀))) |
| 237 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝑧↑𝑘) = (𝐴↑𝑘)) |
| 238 | 237 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧↑𝑘) = (𝐴↑𝑘)) |
| 239 | 236, 238 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
| 240 | 239 | sumeq2dv 15738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
| 241 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin) |
| 242 | 241, 129 | fsumcl 15769 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘)) ∈ ℂ) |
| 243 | 2, 240, 126, 242 | fvmptd 7023 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴↑𝑘))) |
| 244 | 17, 16 | coeid2 26278 |
. . . . . . . 8
⊢ ((𝐺 ∈ (Poly‘ℤ)
∧ 𝐴 ∈ ℂ)
→ (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗))) |
| 245 | 5, 126, 244 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗))) |
| 246 | 245 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 247 | 83 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ) |
| 248 | 199 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ0) |
| 249 | 247, 248 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ) |
| 250 | 126 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ) |
| 251 | 250, 248 | expcld 14186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (𝐴↑𝑗) ∈ ℂ) |
| 252 | 249, 251 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) ∈ ℂ) |
| 253 | 230, 165,
252, 226 | fsumdivc 15822 |
. . . . . 6
⊢ (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 254 | 246, 253 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴↑𝑗)) / (𝐴↑𝑀))) |
| 255 | 232, 243,
254 | 3eqtr4d 2787 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐺‘𝐴) / (𝐴↑𝑀))) |
| 256 | | elaa2lem.ga |
. . . . 5
⊢ (𝜑 → (𝐺‘𝐴) = 0) |
| 257 | 256 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((𝐺‘𝐴) / (𝐴↑𝑀)) = (0 / (𝐴↑𝑀))) |
| 258 | 255, 257,
227 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
| 259 | 122, 258 | jca 511 |
. 2
⊢ (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) |
| 260 | | fveq2 6906 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹)) |
| 261 | 260 | fveq1d 6908 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0)) |
| 262 | 261 | neeq1d 3000 |
. . . 4
⊢ (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠
0)) |
| 263 | | fveq1 6905 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓‘𝐴) = (𝐹‘𝐴)) |
| 264 | 263 | eqeq1d 2739 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓‘𝐴) = 0 ↔ (𝐹‘𝐴) = 0)) |
| 265 | 262, 264 | anbi12d 632 |
. . 3
⊢ (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0))) |
| 266 | 265 | rspcev 3622 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹‘𝐴) = 0)) → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
| 267 | 57, 259, 266 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |