| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aalioulem1.a | . . . . 5
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) | 
| 2 |  | aalioulem1.b | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℤ) | 
| 3 | 2 | zcnd 12723 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 4 |  | aalioulem1.c | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℕ) | 
| 5 | 4 | nncnd 12282 | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℂ) | 
| 6 | 4 | nnne0d 12316 | . . . . . 6
⊢ (𝜑 → 𝑌 ≠ 0) | 
| 7 | 3, 5, 6 | divcld 12043 | . . . . 5
⊢ (𝜑 → (𝑋 / 𝑌) ∈ ℂ) | 
| 8 |  | eqid 2737 | . . . . . 6
⊢
(coeff‘𝐹) =
(coeff‘𝐹) | 
| 9 |  | eqid 2737 | . . . . . 6
⊢
(deg‘𝐹) =
(deg‘𝐹) | 
| 10 | 8, 9 | coeid2 26278 | . . . . 5
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ (𝑋 / 𝑌) ∈ ℂ) → (𝐹‘(𝑋 / 𝑌)) = Σ𝑎 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎))) | 
| 11 | 1, 7, 10 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐹‘(𝑋 / 𝑌)) = Σ𝑎 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎))) | 
| 12 | 11 | oveq1d 7446 | . . 3
⊢ (𝜑 → ((𝐹‘(𝑋 / 𝑌)) · (𝑌↑(deg‘𝐹))) = (Σ𝑎 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹)))) | 
| 13 |  | fzfid 14014 | . . . 4
⊢ (𝜑 → (0...(deg‘𝐹)) ∈ Fin) | 
| 14 |  | dgrcl 26272 | . . . . . 6
⊢ (𝐹 ∈ (Poly‘ℤ)
→ (deg‘𝐹) ∈
ℕ0) | 
| 15 | 1, 14 | syl 17 | . . . . 5
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) | 
| 16 | 5, 15 | expcld 14186 | . . . 4
⊢ (𝜑 → (𝑌↑(deg‘𝐹)) ∈ ℂ) | 
| 17 |  | 0z 12624 | . . . . . . . 8
⊢ 0 ∈
ℤ | 
| 18 | 8 | coef2 26270 | . . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ 0 ∈ ℤ) → (coeff‘𝐹):ℕ0⟶ℤ) | 
| 19 | 1, 17, 18 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶ℤ) | 
| 20 |  | elfznn0 13660 | . . . . . . 7
⊢ (𝑎 ∈ (0...(deg‘𝐹)) → 𝑎 ∈ ℕ0) | 
| 21 |  | ffvelcdm 7101 | . . . . . . 7
⊢
(((coeff‘𝐹):ℕ0⟶ℤ ∧
𝑎 ∈
ℕ0) → ((coeff‘𝐹)‘𝑎) ∈ ℤ) | 
| 22 | 19, 20, 21 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((coeff‘𝐹)‘𝑎) ∈ ℤ) | 
| 23 | 22 | zcnd 12723 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((coeff‘𝐹)‘𝑎) ∈ ℂ) | 
| 24 |  | expcl 14120 | . . . . . 6
⊢ (((𝑋 / 𝑌) ∈ ℂ ∧ 𝑎 ∈ ℕ0) → ((𝑋 / 𝑌)↑𝑎) ∈ ℂ) | 
| 25 | 7, 20, 24 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((𝑋 / 𝑌)↑𝑎) ∈ ℂ) | 
| 26 | 23, 25 | mulcld 11281 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) ∈ ℂ) | 
| 27 | 13, 16, 26 | fsummulc1 15821 | . . 3
⊢ (𝜑 → (Σ𝑎 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹))) = Σ𝑎 ∈ (0...(deg‘𝐹))((((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹)))) | 
| 28 | 12, 27 | eqtrd 2777 | . 2
⊢ (𝜑 → ((𝐹‘(𝑋 / 𝑌)) · (𝑌↑(deg‘𝐹))) = Σ𝑎 ∈ (0...(deg‘𝐹))((((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹)))) | 
| 29 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑌 ∈ ℂ) | 
| 30 | 15 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈
ℕ0) | 
| 31 | 29, 30 | expcld 14186 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑌↑(deg‘𝐹)) ∈ ℂ) | 
| 32 | 23, 25, 31 | mulassd 11284 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹))) = (((coeff‘𝐹)‘𝑎) · (((𝑋 / 𝑌)↑𝑎) · (𝑌↑(deg‘𝐹))))) | 
| 33 | 2 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑋 ∈ ℤ) | 
| 34 | 33 | zcnd 12723 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑋 ∈ ℂ) | 
| 35 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑌 ≠ 0) | 
| 36 | 20 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑎 ∈ ℕ0) | 
| 37 | 34, 29, 35, 36 | expdivd 14200 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((𝑋 / 𝑌)↑𝑎) = ((𝑋↑𝑎) / (𝑌↑𝑎))) | 
| 38 | 37 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((𝑋 / 𝑌)↑𝑎) · (𝑌↑(deg‘𝐹))) = (((𝑋↑𝑎) / (𝑌↑𝑎)) · (𝑌↑(deg‘𝐹)))) | 
| 39 | 34, 36 | expcld 14186 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑋↑𝑎) ∈ ℂ) | 
| 40 |  | nnexpcl 14115 | . . . . . . . . . 10
⊢ ((𝑌 ∈ ℕ ∧ 𝑎 ∈ ℕ0)
→ (𝑌↑𝑎) ∈
ℕ) | 
| 41 | 4, 20, 40 | syl2an 596 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑌↑𝑎) ∈ ℕ) | 
| 42 | 41 | nncnd 12282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑌↑𝑎) ∈ ℂ) | 
| 43 | 41 | nnne0d 12316 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑌↑𝑎) ≠ 0) | 
| 44 | 39, 42, 31, 43 | div13d 12067 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((𝑋↑𝑎) / (𝑌↑𝑎)) · (𝑌↑(deg‘𝐹))) = (((𝑌↑(deg‘𝐹)) / (𝑌↑𝑎)) · (𝑋↑𝑎))) | 
| 45 | 38, 44 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((𝑋 / 𝑌)↑𝑎) · (𝑌↑(deg‘𝐹))) = (((𝑌↑(deg‘𝐹)) / (𝑌↑𝑎)) · (𝑋↑𝑎))) | 
| 46 |  | elfzelz 13564 | . . . . . . . . . 10
⊢ (𝑎 ∈ (0...(deg‘𝐹)) → 𝑎 ∈ ℤ) | 
| 47 | 46 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑎 ∈ ℤ) | 
| 48 | 30 | nn0zd 12639 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈ ℤ) | 
| 49 | 29, 35, 47, 48 | expsubd 14197 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑌↑((deg‘𝐹) − 𝑎)) = ((𝑌↑(deg‘𝐹)) / (𝑌↑𝑎))) | 
| 50 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑌 ∈ ℕ) | 
| 51 | 50 | nnzd 12640 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → 𝑌 ∈ ℤ) | 
| 52 |  | fznn0sub 13596 | . . . . . . . . . 10
⊢ (𝑎 ∈ (0...(deg‘𝐹)) → ((deg‘𝐹) − 𝑎) ∈
ℕ0) | 
| 53 | 52 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((deg‘𝐹) − 𝑎) ∈
ℕ0) | 
| 54 |  | zexpcl 14117 | . . . . . . . . 9
⊢ ((𝑌 ∈ ℤ ∧
((deg‘𝐹) −
𝑎) ∈
ℕ0) → (𝑌↑((deg‘𝐹) − 𝑎)) ∈ ℤ) | 
| 55 | 51, 53, 54 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑌↑((deg‘𝐹) − 𝑎)) ∈ ℤ) | 
| 56 | 49, 55 | eqeltrrd 2842 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((𝑌↑(deg‘𝐹)) / (𝑌↑𝑎)) ∈ ℤ) | 
| 57 |  | zexpcl 14117 | . . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑎 ∈ ℕ0)
→ (𝑋↑𝑎) ∈
ℤ) | 
| 58 | 2, 20, 57 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (𝑋↑𝑎) ∈ ℤ) | 
| 59 | 56, 58 | zmulcld 12728 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((𝑌↑(deg‘𝐹)) / (𝑌↑𝑎)) · (𝑋↑𝑎)) ∈ ℤ) | 
| 60 | 45, 59 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((𝑋 / 𝑌)↑𝑎) · (𝑌↑(deg‘𝐹))) ∈ ℤ) | 
| 61 | 22, 60 | zmulcld 12728 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → (((coeff‘𝐹)‘𝑎) · (((𝑋 / 𝑌)↑𝑎) · (𝑌↑(deg‘𝐹)))) ∈ ℤ) | 
| 62 | 32, 61 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (0...(deg‘𝐹))) → ((((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹))) ∈ ℤ) | 
| 63 | 13, 62 | fsumzcl 15771 | . 2
⊢ (𝜑 → Σ𝑎 ∈ (0...(deg‘𝐹))((((coeff‘𝐹)‘𝑎) · ((𝑋 / 𝑌)↑𝑎)) · (𝑌↑(deg‘𝐹))) ∈ ℤ) | 
| 64 | 28, 63 | eqeltrd 2841 | 1
⊢ (𝜑 → ((𝐹‘(𝑋 / 𝑌)) · (𝑌↑(deg‘𝐹))) ∈ ℤ) |