| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elaa 26358 | . . . 4
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) | 
| 2 | 1 | simprbi 496 | . . 3
⊢ (𝐴 ∈ 𝔸 →
∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0) | 
| 3 | 2 | adantr 480 | . 2
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) → ∃𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝})(𝑓‘𝐴) = 0) | 
| 4 |  | aacn 26359 | . . . . 5
⊢ (𝐴 ∈ 𝔸 → 𝐴 ∈
ℂ) | 
| 5 |  | reccl 11929 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) | 
| 6 | 4, 5 | sylan 580 | . . . 4
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) | 
| 7 | 6 | adantr 480 | . . 3
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (1 / 𝐴) ∈ ℂ) | 
| 8 |  | zsscn 12621 | . . . . . . 7
⊢ ℤ
⊆ ℂ | 
| 9 | 8 | a1i 11 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ℤ ⊆
ℂ) | 
| 10 |  | simprl 771 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → 𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})) | 
| 11 |  | eldifsn 4786 | . . . . . . . . 9
⊢ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ↔ (𝑓 ∈ (Poly‘ℤ) ∧ 𝑓 ≠
0𝑝)) | 
| 12 | 10, 11 | sylib 218 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑓 ∈ (Poly‘ℤ) ∧ 𝑓 ≠
0𝑝)) | 
| 13 | 12 | simpld 494 | . . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → 𝑓 ∈
(Poly‘ℤ)) | 
| 14 |  | dgrcl 26272 | . . . . . . 7
⊢ (𝑓 ∈ (Poly‘ℤ)
→ (deg‘𝑓) ∈
ℕ0) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (deg‘𝑓) ∈
ℕ0) | 
| 16 | 13 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → 𝑓 ∈
(Poly‘ℤ)) | 
| 17 |  | 0z 12624 | . . . . . . . 8
⊢ 0 ∈
ℤ | 
| 18 |  | eqid 2737 | . . . . . . . . 9
⊢
(coeff‘𝑓) =
(coeff‘𝑓) | 
| 19 | 18 | coef2 26270 | . . . . . . . 8
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ 0 ∈ ℤ) → (coeff‘𝑓):ℕ0⟶ℤ) | 
| 20 | 16, 17, 19 | sylancl 586 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (coeff‘𝑓):ℕ0⟶ℤ) | 
| 21 |  | fznn0sub 13596 | . . . . . . . 8
⊢ (𝑘 ∈ (0...(deg‘𝑓)) → ((deg‘𝑓) − 𝑘) ∈
ℕ0) | 
| 22 | 21 | adantl 481 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((deg‘𝑓) − 𝑘) ∈
ℕ0) | 
| 23 | 20, 22 | ffvelcdmd 7105 | . . . . . 6
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) ∈ ℤ) | 
| 24 | 9, 15, 23 | elplyd 26241 | . . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ∈
(Poly‘ℤ)) | 
| 25 |  | 0cn 11253 | . . . . . 6
⊢ 0 ∈
ℂ | 
| 26 |  | eqid 2737 | . . . . . . . . . 10
⊢
(coeff‘(𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))) = (coeff‘(𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))) | 
| 27 | 26 | coefv0 26287 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ∈ (Poly‘ℤ) →
((𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘0) = ((coeff‘(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))))‘0)) | 
| 28 | 24, 27 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘0) = ((coeff‘(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))))‘0)) | 
| 29 | 23 | zcnd 12723 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) ∈ ℂ) | 
| 30 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))) | 
| 31 | 24, 15, 29, 30 | coeeq2 26281 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (coeff‘(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0))) | 
| 32 | 31 | fveq1d 6908 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((coeff‘(𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0))‘0)) | 
| 33 |  | 0nn0 12541 | . . . . . . . . . 10
⊢ 0 ∈
ℕ0 | 
| 34 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑘 ≤ (deg‘𝑓) ↔ 0 ≤ (deg‘𝑓))) | 
| 35 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((deg‘𝑓) − 𝑘) = ((deg‘𝑓) − 0)) | 
| 36 | 35 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) = ((coeff‘𝑓)‘((deg‘𝑓) − 0))) | 
| 37 | 34, 36 | ifbieq1d 4550 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → if(𝑘 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0) = if(0 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 0)),
0)) | 
| 38 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ≤
(deg‘𝑓),
((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0)) | 
| 39 |  | fvex 6919 | . . . . . . . . . . . 12
⊢
((coeff‘𝑓)‘((deg‘𝑓) − 0)) ∈ V | 
| 40 |  | c0ex 11255 | . . . . . . . . . . . 12
⊢ 0 ∈
V | 
| 41 | 39, 40 | ifex 4576 | . . . . . . . . . . 11
⊢ if(0 ≤
(deg‘𝑓),
((coeff‘𝑓)‘((deg‘𝑓) − 0)), 0) ∈ V | 
| 42 | 37, 38, 41 | fvmpt 7016 | . . . . . . . . . 10
⊢ (0 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0))‘0) = if(0 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 0)),
0)) | 
| 43 | 33, 42 | ax-mp 5 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
↦ if(𝑘 ≤
(deg‘𝑓),
((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0))‘0) = if(0 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 0)),
0) | 
| 44 | 15 | nn0ge0d 12590 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → 0 ≤ (deg‘𝑓)) | 
| 45 | 44 | iftrued 4533 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → if(0 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 0)), 0) =
((coeff‘𝑓)‘((deg‘𝑓) − 0))) | 
| 46 | 15 | nn0cnd 12589 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (deg‘𝑓) ∈ ℂ) | 
| 47 | 46 | subid1d 11609 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((deg‘𝑓) − 0) = (deg‘𝑓)) | 
| 48 | 47 | fveq2d 6910 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((coeff‘𝑓)‘((deg‘𝑓) − 0)) =
((coeff‘𝑓)‘(deg‘𝑓))) | 
| 49 | 45, 48 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → if(0 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 0)), 0) =
((coeff‘𝑓)‘(deg‘𝑓))) | 
| 50 | 43, 49 | eqtrid 2789 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ (deg‘𝑓), ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)), 0))‘0) = ((coeff‘𝑓)‘(deg‘𝑓))) | 
| 51 | 28, 32, 50 | 3eqtrd 2781 | . . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘0) = ((coeff‘𝑓)‘(deg‘𝑓))) | 
| 52 | 12 | simprd 495 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → 𝑓 ≠ 0𝑝) | 
| 53 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(deg‘𝑓) =
(deg‘𝑓) | 
| 54 | 53, 18 | dgreq0 26305 | . . . . . . . . . 10
⊢ (𝑓 ∈ (Poly‘ℤ)
→ (𝑓 =
0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) = 0)) | 
| 55 | 13, 54 | syl 17 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑓 = 0𝑝 ↔
((coeff‘𝑓)‘(deg‘𝑓)) = 0)) | 
| 56 | 55 | necon3bid 2985 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑓 ≠ 0𝑝 ↔
((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0)) | 
| 57 | 52, 56 | mpbid 232 | . . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0) | 
| 58 | 51, 57 | eqnetrd 3008 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘0) ≠ 0) | 
| 59 |  | ne0p 26246 | . . . . . 6
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘0) ≠ 0) → (𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ≠
0𝑝) | 
| 60 | 25, 58, 59 | sylancr 587 | . . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ≠
0𝑝) | 
| 61 |  | eldifsn 4786 | . . . . 5
⊢ ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ∈ ((Poly‘ℤ) ∖
{0𝑝}) ↔ ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ∈ (Poly‘ℤ) ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ≠
0𝑝)) | 
| 62 | 24, 60, 61 | sylanbrc 583 | . . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ∈ ((Poly‘ℤ) ∖
{0𝑝})) | 
| 63 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑧 = (1 / 𝐴) → (𝑧↑𝑘) = ((1 / 𝐴)↑𝑘)) | 
| 64 | 63 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑧 = (1 / 𝐴) → (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)) = (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 65 | 64 | sumeq2sdv 15739 | . . . . . . 7
⊢ (𝑧 = (1 / 𝐴) → Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 66 |  | eqid 2737 | . . . . . . 7
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) | 
| 67 |  | sumex 15724 | . . . . . . 7
⊢
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘)) ∈ V | 
| 68 | 65, 66, 67 | fvmpt 7016 | . . . . . 6
⊢ ((1 /
𝐴) ∈ ℂ →
((𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘(1 / 𝐴)) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 69 | 7, 68 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘(1 / 𝐴)) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 70 | 18 | coef3 26271 | . . . . . . . . . . 11
⊢ (𝑓 ∈ (Poly‘ℤ)
→ (coeff‘𝑓):ℕ0⟶ℂ) | 
| 71 | 13, 70 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (coeff‘𝑓):ℕ0⟶ℂ) | 
| 72 |  | elfznn0 13660 | . . . . . . . . . 10
⊢ (𝑛 ∈ (0...(deg‘𝑓)) → 𝑛 ∈ ℕ0) | 
| 73 |  | ffvelcdm 7101 | . . . . . . . . . 10
⊢
(((coeff‘𝑓):ℕ0⟶ℂ ∧
𝑛 ∈
ℕ0) → ((coeff‘𝑓)‘𝑛) ∈ ℂ) | 
| 74 | 71, 72, 73 | syl2an 596 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑛 ∈ (0...(deg‘𝑓))) → ((coeff‘𝑓)‘𝑛) ∈ ℂ) | 
| 75 | 4 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → 𝐴 ∈ ℂ) | 
| 76 |  | expcl 14120 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝐴↑𝑛) ∈
ℂ) | 
| 77 | 75, 72, 76 | syl2an 596 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑛 ∈ (0...(deg‘𝑓))) → (𝐴↑𝑛) ∈ ℂ) | 
| 78 | 74, 77 | mulcld 11281 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑛 ∈ (0...(deg‘𝑓))) → (((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) ∈ ℂ) | 
| 79 | 75, 15 | expcld 14186 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝐴↑(deg‘𝑓)) ∈ ℂ) | 
| 80 | 79 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑛 ∈ (0...(deg‘𝑓))) → (𝐴↑(deg‘𝑓)) ∈ ℂ) | 
| 81 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → 𝐴 ≠ 0) | 
| 82 | 15 | nn0zd 12639 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (deg‘𝑓) ∈ ℤ) | 
| 83 | 75, 81, 82 | expne0d 14192 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝐴↑(deg‘𝑓)) ≠ 0) | 
| 84 | 83 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑛 ∈ (0...(deg‘𝑓))) → (𝐴↑(deg‘𝑓)) ≠ 0) | 
| 85 | 78, 80, 84 | divcld 12043 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑛 ∈ (0...(deg‘𝑓))) → ((((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) ∈ ℂ) | 
| 86 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑛 = ((0 + (deg‘𝑓)) − 𝑘) → ((coeff‘𝑓)‘𝑛) = ((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘))) | 
| 87 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑛 = ((0 + (deg‘𝑓)) − 𝑘) → (𝐴↑𝑛) = (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) | 
| 88 | 86, 87 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑛 = ((0 + (deg‘𝑓)) − 𝑘) → (((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) = (((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘)))) | 
| 89 | 88 | oveq1d 7446 | . . . . . . 7
⊢ (𝑛 = ((0 + (deg‘𝑓)) − 𝑘) → ((((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) = ((((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) / (𝐴↑(deg‘𝑓)))) | 
| 90 | 85, 89 | fsumrev2 15818 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → Σ𝑛 ∈ (0...(deg‘𝑓))((((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) = Σ𝑘 ∈ (0...(deg‘𝑓))((((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) / (𝐴↑(deg‘𝑓)))) | 
| 91 | 46 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (deg‘𝑓) ∈ ℂ) | 
| 92 | 91 | addlidd 11462 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (0 + (deg‘𝑓)) = (deg‘𝑓)) | 
| 93 | 92 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((0 + (deg‘𝑓)) − 𝑘) = ((deg‘𝑓) − 𝑘)) | 
| 94 | 93 | fveq2d 6910 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) = ((coeff‘𝑓)‘((deg‘𝑓) − 𝑘))) | 
| 95 | 93 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑((0 + (deg‘𝑓)) − 𝑘)) = (𝐴↑((deg‘𝑓) − 𝑘))) | 
| 96 | 75 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → 𝐴 ∈ ℂ) | 
| 97 | 81 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → 𝐴 ≠ 0) | 
| 98 |  | elfznn0 13660 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...(deg‘𝑓)) → 𝑘 ∈ ℕ0) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → 𝑘 ∈ ℕ0) | 
| 100 | 99 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → 𝑘 ∈ ℤ) | 
| 101 | 82 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (deg‘𝑓) ∈ ℤ) | 
| 102 | 96, 97, 100, 101 | expsubd 14197 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑((deg‘𝑓) − 𝑘)) = ((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘))) | 
| 103 | 95, 102 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑((0 + (deg‘𝑓)) − 𝑘)) = ((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘))) | 
| 104 | 94, 103 | oveq12d 7449 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) = (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘)))) | 
| 105 | 104 | oveq1d 7446 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) / (𝐴↑(deg‘𝑓))) = ((((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘))) / (𝐴↑(deg‘𝑓)))) | 
| 106 | 79 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑(deg‘𝑓)) ∈ ℂ) | 
| 107 |  | expcl 14120 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) | 
| 108 | 75, 98, 107 | syl2an 596 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑𝑘) ∈ ℂ) | 
| 109 | 96, 97, 100 | expne0d 14192 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑𝑘) ≠ 0) | 
| 110 | 106, 108,
109 | divcld 12043 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘)) ∈ ℂ) | 
| 111 | 83 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (𝐴↑(deg‘𝑓)) ≠ 0) | 
| 112 | 29, 110, 106, 111 | divassd 12078 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘))) / (𝐴↑(deg‘𝑓))) = (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘)) / (𝐴↑(deg‘𝑓))))) | 
| 113 | 106, 111 | dividd 12041 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((𝐴↑(deg‘𝑓)) / (𝐴↑(deg‘𝑓))) = 1) | 
| 114 | 113 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (((𝐴↑(deg‘𝑓)) / (𝐴↑(deg‘𝑓))) / (𝐴↑𝑘)) = (1 / (𝐴↑𝑘))) | 
| 115 | 106, 108,
106, 109, 111 | divdiv32d 12068 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘)) / (𝐴↑(deg‘𝑓))) = (((𝐴↑(deg‘𝑓)) / (𝐴↑(deg‘𝑓))) / (𝐴↑𝑘))) | 
| 116 | 96, 97, 100 | exprecd 14194 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((1 / 𝐴)↑𝑘) = (1 / (𝐴↑𝑘))) | 
| 117 | 114, 115,
116 | 3eqtr4d 2787 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘)) / (𝐴↑(deg‘𝑓))) = ((1 / 𝐴)↑𝑘)) | 
| 118 | 117 | oveq2d 7447 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (((𝐴↑(deg‘𝑓)) / (𝐴↑𝑘)) / (𝐴↑(deg‘𝑓)))) = (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 119 | 105, 112,
118 | 3eqtrd 2781 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) ∧ 𝑘 ∈ (0...(deg‘𝑓))) → ((((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) / (𝐴↑(deg‘𝑓))) = (((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 120 | 119 | sumeq2dv 15738 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → Σ𝑘 ∈ (0...(deg‘𝑓))((((coeff‘𝑓)‘((0 + (deg‘𝑓)) − 𝑘)) · (𝐴↑((0 + (deg‘𝑓)) − 𝑘))) / (𝐴↑(deg‘𝑓))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 121 | 90, 120 | eqtrd 2777 | . . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → Σ𝑛 ∈ (0...(deg‘𝑓))((((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · ((1 / 𝐴)↑𝑘))) | 
| 122 | 18, 53 | coeid2 26278 | . . . . . . . . 9
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ 𝐴 ∈ ℂ)
→ (𝑓‘𝐴) = Σ𝑛 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛))) | 
| 123 | 13, 75, 122 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑓‘𝐴) = Σ𝑛 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛))) | 
| 124 |  | simprr 773 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (𝑓‘𝐴) = 0) | 
| 125 | 123, 124 | eqtr3d 2779 | . . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → Σ𝑛 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) = 0) | 
| 126 | 125 | oveq1d 7446 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (Σ𝑛 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) = (0 / (𝐴↑(deg‘𝑓)))) | 
| 127 |  | fzfid 14014 | . . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (0...(deg‘𝑓)) ∈ Fin) | 
| 128 | 127, 79, 78, 83 | fsumdivc 15822 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (Σ𝑛 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) = Σ𝑛 ∈ (0...(deg‘𝑓))((((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓)))) | 
| 129 | 79, 83 | div0d 12042 | . . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (0 / (𝐴↑(deg‘𝑓))) = 0) | 
| 130 | 126, 128,
129 | 3eqtr3d 2785 | . . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → Σ𝑛 ∈ (0...(deg‘𝑓))((((coeff‘𝑓)‘𝑛) · (𝐴↑𝑛)) / (𝐴↑(deg‘𝑓))) = 0) | 
| 131 | 69, 121, 130 | 3eqtr2d 2783 | . . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘(1 / 𝐴)) = 0) | 
| 132 |  | fveq1 6905 | . . . . . 6
⊢ (𝑔 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) → (𝑔‘(1 / 𝐴)) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘(1 / 𝐴))) | 
| 133 | 132 | eqeq1d 2739 | . . . . 5
⊢ (𝑔 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) → ((𝑔‘(1 / 𝐴)) = 0 ↔ ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘(1 / 𝐴)) = 0)) | 
| 134 | 133 | rspcev 3622 | . . . 4
⊢ (((𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘))) ∈ ((Poly‘ℤ) ∖
{0𝑝}) ∧ ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘((deg‘𝑓) − 𝑘)) · (𝑧↑𝑘)))‘(1 / 𝐴)) = 0) → ∃𝑔 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑔‘(1 / 𝐴)) = 0) | 
| 135 | 62, 131, 134 | syl2anc 584 | . . 3
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → ∃𝑔 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑔‘(1 / 𝐴)) = 0) | 
| 136 |  | elaa 26358 | . . 3
⊢ ((1 /
𝐴) ∈ 𝔸 ↔
((1 / 𝐴) ∈ ℂ
∧ ∃𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑔‘(1 / 𝐴)) = 0)) | 
| 137 | 7, 135, 136 | sylanbrc 583 | . 2
⊢ (((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) ∧ (𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (𝑓‘𝐴) = 0)) → (1 / 𝐴) ∈ 𝔸) | 
| 138 | 3, 137 | rexlimddv 3161 | 1
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
𝔸) |