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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	elqaa.2	⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
	elqaa.3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
	elqaa.4	⊢ 𝐵 = ( coeff ‘ 𝐹 )
	elqaa.5	⊢ 𝑁 = ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
	elqaa.6	⊢ 𝑅 = ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) )
Assertion	elqaalem1	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝐾 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝐾 ) · ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		elqaa.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		elqaa.2	⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
3		elqaa.3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
4		elqaa.4	⊢ 𝐵 = ( coeff ‘ 𝐹 )
5		elqaa.5	⊢ 𝑁 = ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
6		elqaa.6	⊢ 𝑅 = ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) )
7		fveq2	⊢ ( 𝑘 = 𝐾 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝐾 ) )
8	7	oveq1d	⊢ ( 𝑘 = 𝐾 → ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) = ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) )
9	8	eleq1d	⊢ ( 𝑘 = 𝐾 → ( ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ ↔ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ ) )
10	9	rabbidv	⊢ ( 𝑘 = 𝐾 → { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } = { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } )
11	10	infeq1d	⊢ ( 𝑘 = 𝐾 → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
12		ltso	⊢ < Or ℝ
13	12	infex	⊢ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ∈ V
14	11 5 13	fvmpt	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑁 ‘ 𝐾 ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ‘ 𝐾 ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
16		ssrab2	⊢ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ⊆ ℕ
17		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
18	16 17	sseqtri	⊢ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ⊆ ( ℤ≥ ‘ 1 )
19	2	eldifad	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℚ ) )
20		0z	⊢ 0 ∈ ℤ
21		zq	⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
22	20 21	ax-mp	⊢ 0 ∈ ℚ
23	4	coef2	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℚ ) ∧ 0 ∈ ℚ ) → 𝐵 : ℕ0 ⟶ ℚ )
24	19 22 23	sylancl	⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℚ )
25	24	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ‘ 𝐾 ) ∈ ℚ )
26		qmulz	⊢ ( ( 𝐵 ‘ 𝐾 ) ∈ ℚ → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ )
27	25 26	syl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ )
28		rabn0	⊢ ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ≠ ∅ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ )
29	27 28	sylibr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ≠ ∅ )
30		infssuzcl	⊢ ( ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } )
31	18 29 30	sylancr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } )
32	15 31	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ‘ 𝐾 ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } )
33		oveq2	⊢ ( 𝑛 = ( 𝑁 ‘ 𝐾 ) → ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) = ( ( 𝐵 ‘ 𝐾 ) · ( 𝑁 ‘ 𝐾 ) ) )
34	33	eleq1d	⊢ ( 𝑛 = ( 𝑁 ‘ 𝐾 ) → ( ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ ↔ ( ( 𝐵 ‘ 𝐾 ) · ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )
35	34	elrab	⊢ ( ( 𝑁 ‘ 𝐾 ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝐾 ) · 𝑛 ) ∈ ℤ } ↔ ( ( 𝑁 ‘ 𝐾 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝐾 ) · ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )
36	32 35	sylib	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝐾 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝐾 ) · ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )