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 
|- ( ph -> F e. ( Poly ` ZZ ) )
aalioulem1.b 
|- ( ph -> X e. ZZ )
aalioulem1.c 
|- ( ph -> Y e. NN )
Assertion aalioulem1 
|- ( ph -> ( ( F ` ( X / Y ) ) x. ( Y ^ ( deg ` F ) ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 aalioulem1.a 
 |-  ( ph -> F e. ( Poly ` ZZ ) )
2 aalioulem1.b 
 |-  ( ph -> X e. ZZ )
3 aalioulem1.c 
 |-  ( ph -> Y e. NN )
4 2 zcnd 
 |-  ( ph -> X e. CC )
5 3 nncnd 
 |-  ( ph -> Y e. CC )
6 3 nnne0d 
 |-  ( ph -> Y =/= 0 )
7 4 5 6 divcld 
 |-  ( ph -> ( X / Y ) e. CC )
8 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
9 eqid 
 |-  ( deg ` F ) = ( deg ` F )
10 8 9 coeid2 
 |-  ( ( F e. ( Poly ` ZZ ) /\ ( X / Y ) e. CC ) -> ( F ` ( X / Y ) ) = sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) )
11 1 7 10 syl2anc 
 |-  ( ph -> ( F ` ( X / Y ) ) = sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) )
12 11 oveq1d 
 |-  ( ph -> ( ( F ` ( X / Y ) ) x. ( Y ^ ( deg ` F ) ) ) = ( sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) )
13 fzfid 
 |-  ( ph -> ( 0 ... ( deg ` F ) ) e. Fin )
14 dgrcl 
 |-  ( F e. ( Poly ` ZZ ) -> ( deg ` F ) e. NN0 )
15 1 14 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
16 5 15 expcld 
 |-  ( ph -> ( Y ^ ( deg ` F ) ) e. CC )
17 0z 
 |-  0 e. ZZ
18 8 coef2 
 |-  ( ( F e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> ( coeff ` F ) : NN0 --> ZZ )
19 1 17 18 sylancl 
 |-  ( ph -> ( coeff ` F ) : NN0 --> ZZ )
20 elfznn0 
 |-  ( a e. ( 0 ... ( deg ` F ) ) -> a e. NN0 )
21 ffvelrn 
 |-  ( ( ( coeff ` F ) : NN0 --> ZZ /\ a e. NN0 ) -> ( ( coeff ` F ) ` a ) e. ZZ )
22 19 20 21 syl2an 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( coeff ` F ) ` a ) e. ZZ )
23 22 zcnd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( coeff ` F ) ` a ) e. CC )
24 expcl 
 |-  ( ( ( X / Y ) e. CC /\ a e. NN0 ) -> ( ( X / Y ) ^ a ) e. CC )
25 7 20 24 syl2an 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( X / Y ) ^ a ) e. CC )
26 23 25 mulcld 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) e. CC )
27 13 16 26 fsummulc1 
 |-  ( ph -> ( sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) = sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) )
28 12 27 eqtrd 
 |-  ( ph -> ( ( F ` ( X / Y ) ) x. ( Y ^ ( deg ` F ) ) ) = sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) )
29 5 adantr 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> Y e. CC )
30 15 adantr 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( deg ` F ) e. NN0 )
31 29 30 expcld 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( Y ^ ( deg ` F ) ) e. CC )
32 23 25 31 mulassd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) = ( ( ( coeff ` F ) ` a ) x. ( ( ( X / Y ) ^ a ) x. ( Y ^ ( deg ` F ) ) ) ) )
33 2 adantr 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> X e. ZZ )
34 33 zcnd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> X e. CC )
35 6 adantr 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> Y =/= 0 )
36 20 adantl 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> a e. NN0 )
37 34 29 35 36 expdivd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( X / Y ) ^ a ) = ( ( X ^ a ) / ( Y ^ a ) ) )
38 37 oveq1d 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( X / Y ) ^ a ) x. ( Y ^ ( deg ` F ) ) ) = ( ( ( X ^ a ) / ( Y ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) )
39 34 36 expcld 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( X ^ a ) e. CC )
40 nnexpcl 
 |-  ( ( Y e. NN /\ a e. NN0 ) -> ( Y ^ a ) e. NN )
41 3 20 40 syl2an 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( Y ^ a ) e. NN )
42 41 nncnd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( Y ^ a ) e. CC )
43 41 nnne0d 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( Y ^ a ) =/= 0 )
44 39 42 31 43 div13d 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( X ^ a ) / ( Y ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) = ( ( ( Y ^ ( deg ` F ) ) / ( Y ^ a ) ) x. ( X ^ a ) ) )
45 38 44 eqtrd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( X / Y ) ^ a ) x. ( Y ^ ( deg ` F ) ) ) = ( ( ( Y ^ ( deg ` F ) ) / ( Y ^ a ) ) x. ( X ^ a ) ) )
46 elfzelz 
 |-  ( a e. ( 0 ... ( deg ` F ) ) -> a e. ZZ )
47 46 adantl 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> a e. ZZ )
48 30 nn0zd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( deg ` F ) e. ZZ )
49 29 35 47 48 expsubd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( Y ^ ( ( deg ` F ) - a ) ) = ( ( Y ^ ( deg ` F ) ) / ( Y ^ a ) ) )
50 3 adantr 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> Y e. NN )
51 50 nnzd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> Y e. ZZ )
52 fznn0sub 
 |-  ( a e. ( 0 ... ( deg ` F ) ) -> ( ( deg ` F ) - a ) e. NN0 )
53 52 adantl 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( deg ` F ) - a ) e. NN0 )
54 zexpcl 
 |-  ( ( Y e. ZZ /\ ( ( deg ` F ) - a ) e. NN0 ) -> ( Y ^ ( ( deg ` F ) - a ) ) e. ZZ )
55 51 53 54 syl2anc 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( Y ^ ( ( deg ` F ) - a ) ) e. ZZ )
56 49 55 eqeltrrd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( Y ^ ( deg ` F ) ) / ( Y ^ a ) ) e. ZZ )
57 zexpcl 
 |-  ( ( X e. ZZ /\ a e. NN0 ) -> ( X ^ a ) e. ZZ )
58 2 20 57 syl2an 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( X ^ a ) e. ZZ )
59 56 58 zmulcld 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( Y ^ ( deg ` F ) ) / ( Y ^ a ) ) x. ( X ^ a ) ) e. ZZ )
60 45 59 eqeltrd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( X / Y ) ^ a ) x. ( Y ^ ( deg ` F ) ) ) e. ZZ )
61 22 60 zmulcld 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( coeff ` F ) ` a ) x. ( ( ( X / Y ) ^ a ) x. ( Y ^ ( deg ` F ) ) ) ) e. ZZ )
62 32 61 eqeltrd 
 |-  ( ( ph /\ a e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) e. ZZ )
63 13 62 fsumzcl 
 |-  ( ph -> sum_ a e. ( 0 ... ( deg ` F ) ) ( ( ( ( coeff ` F ) ` a ) x. ( ( X / Y ) ^ a ) ) x. ( Y ^ ( deg ` F ) ) ) e. ZZ )
64 28 63 eqeltrd 
 |-  ( ph -> ( ( F ` ( X / Y ) ) x. ( Y ^ ( deg ` F ) ) ) e. ZZ )