Metamath Proof Explorer

Theorem elqaalem1

Description: Lemma for elqaa . The function N represents the denominators of the rational coefficients B . By multiplying them all together to make R , we get a number big enough to clear all the denominators and make R x. F an integer polynomial. (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses elqaa.1 
|- ( ph -> A e. CC )
elqaa.2 
|- ( ph -> F e. ( ( Poly ` QQ ) \ { 0p } ) )
elqaa.3 
|- ( ph -> ( F ` A ) = 0 )
elqaa.4 
|- B = ( coeff ` F )
elqaa.5 
|- N = ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) )
elqaa.6 
|- R = ( seq 0 ( x. , N ) ` ( deg ` F ) )
Assertion elqaalem1 
|- ( ( ph /\ K e. NN0 ) -> ( ( N ` K ) e. NN /\ ( ( B ` K ) x. ( N ` K ) ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 elqaa.1 
 |-  ( ph -> A e. CC )
2 elqaa.2 
 |-  ( ph -> F e. ( ( Poly ` QQ ) \ { 0p } ) )
3 elqaa.3 
 |-  ( ph -> ( F ` A ) = 0 )
4 elqaa.4 
 |-  B = ( coeff ` F )
5 elqaa.5 
 |-  N = ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) )
6 elqaa.6 
 |-  R = ( seq 0 ( x. , N ) ` ( deg ` F ) )
7 fveq2 
 |-  ( k = K -> ( B ` k ) = ( B ` K ) )
8 7 oveq1d 
 |-  ( k = K -> ( ( B ` k ) x. n ) = ( ( B ` K ) x. n ) )
9 8 eleq1d 
 |-  ( k = K -> ( ( ( B ` k ) x. n ) e. ZZ <-> ( ( B ` K ) x. n ) e. ZZ ) )
10 9 rabbidv 
 |-  ( k = K -> { n e. NN | ( ( B ` k ) x. n ) e. ZZ } = { n e. NN | ( ( B ` K ) x. n ) e. ZZ } )
11 10 infeq1d 
 |-  ( k = K -> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) = inf ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } , RR , < ) )
12 ltso 
 |-  < Or RR
13 12 infex 
 |-  inf ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } , RR , < ) e. _V
14 11 5 13 fvmpt 
 |-  ( K e. NN0 -> ( N ` K ) = inf ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } , RR , < ) )
15 14 adantl 
 |-  ( ( ph /\ K e. NN0 ) -> ( N ` K ) = inf ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } , RR , < ) )
16 ssrab2 
 |-  { n e. NN | ( ( B ` K ) x. n ) e. ZZ } C_ NN
17 nnuz 
 |-  NN = ( ZZ>= ` 1 )
18 16 17 sseqtri 
 |-  { n e. NN | ( ( B ` K ) x. n ) e. ZZ } C_ ( ZZ>= ` 1 )
19 2 eldifad 
 |-  ( ph -> F e. ( Poly ` QQ ) )
20 0z 
 |-  0 e. ZZ
21 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
22 20 21 ax-mp 
 |-  0 e. QQ
23 4 coef2 
 |-  ( ( F e. ( Poly ` QQ ) /\ 0 e. QQ ) -> B : NN0 --> QQ )
24 19 22 23 sylancl 
 |-  ( ph -> B : NN0 --> QQ )
25 24 ffvelrnda 
 |-  ( ( ph /\ K e. NN0 ) -> ( B ` K ) e. QQ )
26 qmulz 
 |-  ( ( B ` K ) e. QQ -> E. n e. NN ( ( B ` K ) x. n ) e. ZZ )
27 25 26 syl 
 |-  ( ( ph /\ K e. NN0 ) -> E. n e. NN ( ( B ` K ) x. n ) e. ZZ )
28 rabn0 
 |-  ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } =/= (/) <-> E. n e. NN ( ( B ` K ) x. n ) e. ZZ )
29 27 28 sylibr 
 |-  ( ( ph /\ K e. NN0 ) -> { n e. NN | ( ( B ` K ) x. n ) e. ZZ } =/= (/) )
30 infssuzcl 
 |-  ( ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } C_ ( ZZ>= ` 1 ) /\ { n e. NN | ( ( B ` K ) x. n ) e. ZZ } =/= (/) ) -> inf ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } , RR , < ) e. { n e. NN | ( ( B ` K ) x. n ) e. ZZ } )
31 18 29 30 sylancr 
 |-  ( ( ph /\ K e. NN0 ) -> inf ( { n e. NN | ( ( B ` K ) x. n ) e. ZZ } , RR , < ) e. { n e. NN | ( ( B ` K ) x. n ) e. ZZ } )
32 15 31 eqeltrd 
 |-  ( ( ph /\ K e. NN0 ) -> ( N ` K ) e. { n e. NN | ( ( B ` K ) x. n ) e. ZZ } )
33 oveq2 
 |-  ( n = ( N ` K ) -> ( ( B ` K ) x. n ) = ( ( B ` K ) x. ( N ` K ) ) )
34 33 eleq1d 
 |-  ( n = ( N ` K ) -> ( ( ( B ` K ) x. n ) e. ZZ <-> ( ( B ` K ) x. ( N ` K ) ) e. ZZ ) )
35 34 elrab 
 |-  ( ( N ` K ) e. { n e. NN | ( ( B ` K ) x. n ) e. ZZ } <-> ( ( N ` K ) e. NN /\ ( ( B ` K ) x. ( N ` K ) ) e. ZZ ) )
36 32 35 sylib 
 |-  ( ( ph /\ K e. NN0 ) -> ( ( N ` K ) e. NN /\ ( ( B ` K ) x. ( N ` K ) ) e. ZZ ) )