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 φ A
elqaa.2 φ F Poly 0 𝑝
elqaa.3 φ F A = 0
elqaa.4 B = coeff F
elqaa.5 N = k 0 sup n | B k n <
elqaa.6 R = seq 0 × N deg F
Assertion elqaalem1 φ K 0 N K B K N K

Proof

Step Hyp Ref Expression
1 elqaa.1 φ A
2 elqaa.2 φ F Poly 0 𝑝
3 elqaa.3 φ F A = 0
4 elqaa.4 B = coeff F
5 elqaa.5 N = k 0 sup n | B k n <
6 elqaa.6 R = seq 0 × N deg F
7 fveq2 k = K B k = B K
8 7 oveq1d k = K B k n = B K n
9 8 eleq1d k = K B k n B K n
10 9 rabbidv k = K n | B k n = n | B K n
11 10 infeq1d k = K sup n | B k n < = sup n | B K n <
12 ltso < Or
13 12 infex sup n | B K n < V
14 11 5 13 fvmpt K 0 N K = sup n | B K n <
15 14 adantl φ K 0 N K = sup n | B K n <
16 ssrab2 n | B K n
17 nnuz = 1
18 16 17 sseqtri n | B K n 1
19 2 eldifad φ F Poly
20 0z 0
21 zq 0 0
22 20 21 ax-mp 0
23 4 coef2 F Poly 0 B : 0
24 19 22 23 sylancl φ B : 0
25 24 ffvelrnda φ K 0 B K
26 qmulz B K n B K n
27 25 26 syl φ K 0 n B K n
28 rabn0 n | B K n n B K n
29 27 28 sylibr φ K 0 n | B K n
30 infssuzcl n | B K n 1 n | B K n sup n | B K n < n | B K n
31 18 29 30 sylancr φ K 0 sup n | B K n < n | B K n
32 15 31 eqeltrd φ K 0 N K n | B K n
33 oveq2 n = N K B K n = B K N K
34 33 eleq1d n = N K B K n B K N K
35 34 elrab N K n | B K n N K B K N K
36 32 35 sylib φ K 0 N K B K N K