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	$⊢ φ \to A \in ℂ$
	elqaa.2	$⊢ φ \to F \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
	elqaa.3	$⊢ φ \to F (A) = 0$
	elqaa.4	$⊢ B = coeff (F)$
	elqaa.5	$⊢ N = (k \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <))$
	elqaa.6	$⊢ R = seq 0 (\times N) (\deg (F))$
Assertion	elqaalem1	$⊢ (φ \land K \in ℕ_{0}) \to (N (K) \in ℕ \land B (K) N (K) \in ℤ)$

Proof

Step	Hyp	Ref	Expression
1		elqaa.1	$⊢ φ \to A \in ℂ$
2		elqaa.2	$⊢ φ \to F \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
3		elqaa.3	$⊢ φ \to F (A) = 0$
4		elqaa.4	$⊢ B = coeff (F)$
5		elqaa.5	$⊢ N = (k \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <))$
6		elqaa.6	$⊢ R = seq 0 (\times N) (\deg (F))$
7		fveq2	$⊢ k = K \to B (k) = B (K)$
8	7	oveq1d	$⊢ k = K \to B (k) n = B (K) n$
9	8	eleq1d	$⊢ k = K \to (B (k) n \in ℤ \leftrightarrow B (K) n \in ℤ)$
10	9	rabbidv	$⊢ k = K \to \{n \in ℕ \| B (k) n \in ℤ\} = \{n \in ℕ \| B (K) n \in ℤ\}$
11	10	infeq1d	$⊢ k = K \to inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <) = inf (\{n \in ℕ \| B (K) n \in ℤ\} ℝ <)$
12		ltso	$⊢ < Or ℝ$
13	12	infex	$⊢ inf (\{n \in ℕ \| B (K) n \in ℤ\} ℝ <) \in V$
14	11 5 13	fvmpt	$⊢ K \in ℕ_{0} \to N (K) = inf (\{n \in ℕ \| B (K) n \in ℤ\} ℝ <)$
15	14	adantl	$⊢ (φ \land K \in ℕ_{0}) \to N (K) = inf (\{n \in ℕ \| B (K) n \in ℤ\} ℝ <)$
16		ssrab2	$⊢ \{n \in ℕ \| B (K) n \in ℤ\} \subseteq ℕ$
17		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
18	16 17	sseqtri	$⊢ \{n \in ℕ \| B (K) n \in ℤ\} \subseteq ℤ_{\geq 1}$
19	2	eldifad	$⊢ φ \to F \in Poly (ℚ)$
20		0z	$⊢ 0 \in ℤ$
21		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
22	20 21	ax-mp	$⊢ 0 \in ℚ$
23	4	coef2	$⊢ (F \in Poly (ℚ) \land 0 \in ℚ) \to B : ℕ_{0} ⟶ ℚ$
24	19 22 23	sylancl	$⊢ φ \to B : ℕ_{0} ⟶ ℚ$
25	24	ffvelcdmda	$⊢ (φ \land K \in ℕ_{0}) \to B (K) \in ℚ$
26		qmulz	$⊢ B (K) \in ℚ \to \exists n \in ℕ B (K) n \in ℤ$
27	25 26	syl	$⊢ (φ \land K \in ℕ_{0}) \to \exists n \in ℕ B (K) n \in ℤ$
28		rabn0	$⊢ \{n \in ℕ \| B (K) n \in ℤ\} \neq \emptyset \leftrightarrow \exists n \in ℕ B (K) n \in ℤ$
29	27 28	sylibr	$⊢ (φ \land K \in ℕ_{0}) \to \{n \in ℕ \| B (K) n \in ℤ\} \neq \emptyset$
30		infssuzcl	$⊢ (\{n \in ℕ \| B (K) n \in ℤ\} \subseteq ℤ_{\geq 1} \land \{n \in ℕ \| B (K) n \in ℤ\} \neq \emptyset) \to inf (\{n \in ℕ \| B (K) n \in ℤ\} ℝ <) \in \{n \in ℕ \| B (K) n \in ℤ\}$
31	18 29 30	sylancr	$⊢ (φ \land K \in ℕ_{0}) \to inf (\{n \in ℕ \| B (K) n \in ℤ\} ℝ <) \in \{n \in ℕ \| B (K) n \in ℤ\}$
32	15 31	eqeltrd	$⊢ (φ \land K \in ℕ_{0}) \to N (K) \in \{n \in ℕ \| B (K) n \in ℤ\}$
33		oveq2	$⊢ n = N (K) \to B (K) n = B (K) N (K)$
34	33	eleq1d	$⊢ n = N (K) \to (B (K) n \in ℤ \leftrightarrow B (K) N (K) \in ℤ)$
35	34	elrab	$⊢ N (K) \in \{n \in ℕ \| B (K) n \in ℤ\} \leftrightarrow (N (K) \in ℕ \land B (K) N (K) \in ℤ)$
36	32 35	sylib	$⊢ (φ \land K \in ℕ_{0}) \to (N (K) \in ℕ \land B (K) N (K) \in ℤ)$

Metamath Proof Explorer

Theorem elqaalem1

Proof