Metamath Proof Explorer

Theorem aalioulem1

Description: Lemma for aaliou . An integer polynomial cannot inflate the denominator of a rational by more than its degree. (Contributed by Stefan O'Rear, 12-Nov-2014)

Ref Expression
Hypotheses aalioulem1.a ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
aalioulem1.b ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
aalioulem1.c ⊢ ( 𝜑 → 𝑌 ∈ ℕ )
Assertion aalioulem1 ( 𝜑 → ( ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 aalioulem1.a ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
2 aalioulem1.b ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
3 aalioulem1.c ⊢ ( 𝜑 → 𝑌 ∈ ℕ )
4 2 zcnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5 3 nncnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
6 3 nnne0d ⊢ ( 𝜑 → 𝑌 ≠ 0 )
7 4 5 6 divcld ⊢ ( 𝜑 → ( 𝑋 / 𝑌 ) ∈ ℂ )
8 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
9 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
10 8 9 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℤ ) ∧ ( 𝑋 / 𝑌 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) = Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) )
11 1 7 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) = Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) )
12 11 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = ( Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) )
13 fzfid ⊢ ( 𝜑 → ( 0 ... ( deg ‘ 𝐹 ) ) ∈ Fin )
14 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
15 1 14 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
16 5 15 expcld ⊢ ( 𝜑 → ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ∈ ℂ )
17 0z ⊢ 0 ∈ ℤ
18 8 coef2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℤ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℤ )
19 1 17 18 sylancl ⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℤ )
20 elfznn0 ⊢ ( 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑎 ∈ ℕ0 )
21 ffvelcdm ⊢ ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℤ ∧ 𝑎 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) ∈ ℤ )
22 19 20 21 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) ∈ ℤ )
23 22 zcnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) ∈ ℂ )
24 expcl ⊢ ( ( ( 𝑋 / 𝑌 ) ∈ ℂ ∧ 𝑎 ∈ ℕ0 ) → ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ∈ ℂ )
25 7 20 24 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ∈ ℂ )
26 23 25 mulcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) ∈ ℂ )
27 13 16 26 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) )
28 12 27 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) )
29 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑌 ∈ ℂ )
30 15 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
31 29 30 expcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ∈ ℂ )
32 23 25 31 mulassd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ) )
33 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑋 ∈ ℤ )
34 33 zcnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑋 ∈ ℂ )
35 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑌 ≠ 0 )
36 20 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑎 ∈ ℕ0 )
37 34 29 35 36 expdivd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) = ( ( 𝑋 ↑ 𝑎 ) / ( 𝑌 ↑ 𝑎 ) ) )
38 37 oveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = ( ( ( 𝑋 ↑ 𝑎 ) / ( 𝑌 ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) )
39 34 36 expcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑋 ↑ 𝑎 ) ∈ ℂ )
40 nnexpcl ⊢ ( ( 𝑌 ∈ ℕ ∧ 𝑎 ∈ ℕ0 ) → ( 𝑌 ↑ 𝑎 ) ∈ ℕ )
41 3 20 40 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑌 ↑ 𝑎 ) ∈ ℕ )
42 41 nncnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑌 ↑ 𝑎 ) ∈ ℂ )
43 41 nnne0d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑌 ↑ 𝑎 ) ≠ 0 )
44 39 42 31 43 div13d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝑋 ↑ 𝑎 ) / ( 𝑌 ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = ( ( ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) / ( 𝑌 ↑ 𝑎 ) ) · ( 𝑋 ↑ 𝑎 ) ) )
45 38 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) = ( ( ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) / ( 𝑌 ↑ 𝑎 ) ) · ( 𝑋 ↑ 𝑎 ) ) )
46 elfzelz ⊢ ( 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑎 ∈ ℤ )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑎 ∈ ℤ )
48 30 nn0zd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( deg ‘ 𝐹 ) ∈ ℤ )
49 29 35 47 48 expsubd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑌 ↑ ( ( deg ‘ 𝐹 ) − 𝑎 ) ) = ( ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) / ( 𝑌 ↑ 𝑎 ) ) )
50 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑌 ∈ ℕ )
51 50 nnzd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑌 ∈ ℤ )
52 fznn0sub ⊢ ( 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → ( ( deg ‘ 𝐹 ) − 𝑎 ) ∈ ℕ0 )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( deg ‘ 𝐹 ) − 𝑎 ) ∈ ℕ0 )
54 zexpcl ⊢ ( ( 𝑌 ∈ ℤ ∧ ( ( deg ‘ 𝐹 ) − 𝑎 ) ∈ ℕ0 ) → ( 𝑌 ↑ ( ( deg ‘ 𝐹 ) − 𝑎 ) ) ∈ ℤ )
55 51 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑌 ↑ ( ( deg ‘ 𝐹 ) − 𝑎 ) ) ∈ ℤ )
56 49 55 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) / ( 𝑌 ↑ 𝑎 ) ) ∈ ℤ )
57 zexpcl ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑎 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑎 ) ∈ ℤ )
58 2 20 57 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑋 ↑ 𝑎 ) ∈ ℤ )
59 56 58 zmulcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) / ( 𝑌 ↑ 𝑎 ) ) · ( 𝑋 ↑ 𝑎 ) ) ∈ ℤ )
60 45 59 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ∈ ℤ )
61 22 60 zmulcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ) ∈ ℤ )
62 32 61 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ∈ ℤ )
63 13 62 fsumzcl ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( ( coeff ‘ 𝐹 ) ‘ 𝑎 ) · ( ( 𝑋 / 𝑌 ) ↑ 𝑎 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ∈ ℤ )
64 28 63 eqeltrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑋 / 𝑌 ) ) · ( 𝑌 ↑ ( deg ‘ 𝐹 ) ) ) ∈ ℤ )