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	$⊢ φ \to F \in Poly (ℤ)$
	aalioulem1.b	$⊢ φ \to X \in ℤ$
	aalioulem1.c	$⊢ φ \to Y \in ℕ$
Assertion	aalioulem1	$⊢ φ \to F (\frac{X}{Y}) Y^{\deg (F)} \in ℤ$

Proof

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

Metamath Proof Explorer

Theorem aalioulem1

Proof