elaa2lem

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 . (Contributed by Glauco Siliprandi, 5-Apr-2020) (Revised by AV, 1-Oct-2020)

	Ref	Expression
Hypotheses	elaa2lem.a	$⊢ φ \to A \in 𝔸$
	elaa2lem.an0	$⊢ φ \to A \neq 0$
	elaa2lem.g	$⊢ φ \to G \in Poly (ℤ)$
	elaa2lem.gn0	$⊢ φ \to G \neq 0_{𝑝}$
	elaa2lem.ga	$⊢ φ \to G (A) = 0$
	elaa2lem.m	$⊢ M = sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <)$
	elaa2lem.i	$⊢ I = (k \in ℕ_{0} ⟼ coeff (G) (k + M))$
	elaa2lem.f	$⊢ F = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} I (k) z^{k})$
Assertion	elaa2lem	$⊢ φ \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$

Proof

Step	Hyp	Ref	Expression
1		elaa2lem.a	$⊢ φ \to A \in 𝔸$
2		elaa2lem.an0	$⊢ φ \to A \neq 0$
3		elaa2lem.g	$⊢ φ \to G \in Poly (ℤ)$
4		elaa2lem.gn0	$⊢ φ \to G \neq 0_{𝑝}$
5		elaa2lem.ga	$⊢ φ \to G (A) = 0$
6		elaa2lem.m	$⊢ M = sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <)$
7		elaa2lem.i	$⊢ I = (k \in ℕ_{0} ⟼ coeff (G) (k + M))$
8		elaa2lem.f	$⊢ F = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} I (k) z^{k})$
9	8	a1i	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} I (k) z^{k})$
10		zsscn	$⊢ ℤ \subseteq ℂ$
11	10	a1i	$⊢ φ \to ℤ \subseteq ℂ$
12		dgrcl	$⊢ G \in Poly (ℤ) \to \deg (G) \in ℕ_{0}$
13	3 12	syl	$⊢ φ \to \deg (G) \in ℕ_{0}$
14	13	nn0zd	$⊢ φ \to \deg (G) \in ℤ$
15		ssrab2	$⊢ \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℕ_{0}$
16		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
17	15 16	sseqtri	$⊢ \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℤ_{\geq 0}$
18	17	a1i	$⊢ φ \to \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℤ_{\geq 0}$
19	4	neneqd	$⊢ φ \to \neg G = 0_{𝑝}$
20		eqid	$⊢ \deg (G) = \deg (G)$
21		eqid	$⊢ coeff (G) = coeff (G)$
22	20 21	dgreq0	$⊢ G \in Poly (ℤ) \to (G = 0_{𝑝} \leftrightarrow coeff (G) (\deg (G)) = 0)$
23	3 22	syl	$⊢ φ \to (G = 0_{𝑝} \leftrightarrow coeff (G) (\deg (G)) = 0)$
24	19 23	mtbid	$⊢ φ \to \neg coeff (G) (\deg (G)) = 0$
25	24	neqned	$⊢ φ \to coeff (G) (\deg (G)) \neq 0$
26	13 25	jca	$⊢ φ \to (\deg (G) \in ℕ_{0} \land coeff (G) (\deg (G)) \neq 0)$
27		fveq2	$⊢ n = \deg (G) \to coeff (G) (n) = coeff (G) (\deg (G))$
28	27	neeq1d	$⊢ n = \deg (G) \to (coeff (G) (n) \neq 0 \leftrightarrow coeff (G) (\deg (G)) \neq 0)$
29	28	elrab	$⊢ \deg (G) \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \leftrightarrow (\deg (G) \in ℕ_{0} \land coeff (G) (\deg (G)) \neq 0)$
30	26 29	sylibr	$⊢ φ \to \deg (G) \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}$
31	30	ne0d	$⊢ φ \to \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \neq \emptyset$
32		infssuzcl	$⊢ (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℤ_{\geq 0} \land \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \neq \emptyset) \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}$
33	18 31 32	syl2anc	$⊢ φ \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}$
34	15 33	sseldi	$⊢ φ \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \in ℕ_{0}$
35	6 34	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
36	35	nn0zd	$⊢ φ \to M \in ℤ$
37	14 36	zsubcld	$⊢ φ \to \deg (G) - M \in ℤ$
38	6	a1i	$⊢ φ \to M = sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <)$
39		infssuzle	$⊢ (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℤ_{\geq 0} \land \deg (G) \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}) \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \leq \deg (G)$
40	18 30 39	syl2anc	$⊢ φ \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \leq \deg (G)$
41	38 40	eqbrtrd	$⊢ φ \to M \leq \deg (G)$
42	13	nn0red	$⊢ φ \to \deg (G) \in ℝ$
43	35	nn0red	$⊢ φ \to M \in ℝ$
44	42 43	subge0d	$⊢ φ \to (0 \leq \deg (G) - M \leftrightarrow M \leq \deg (G))$
45	41 44	mpbird	$⊢ φ \to 0 \leq \deg (G) - M$
46	37 45	jca	$⊢ φ \to (\deg (G) - M \in ℤ \land 0 \leq \deg (G) - M)$
47		elnn0z	$⊢ \deg (G) - M \in ℕ_{0} \leftrightarrow (\deg (G) - M \in ℤ \land 0 \leq \deg (G) - M)$
48	46 47	sylibr	$⊢ φ \to \deg (G) - M \in ℕ_{0}$
49		0zd	$⊢ G \in Poly (ℤ) \to 0 \in ℤ$
50	21	coef2	$⊢ (G \in Poly (ℤ) \land 0 \in ℤ) \to coeff (G) : ℕ_{0} ⟶ ℤ$
51	3 49 50	syl2anc2	$⊢ φ \to coeff (G) : ℕ_{0} ⟶ ℤ$
52	51	adantr	$⊢ (φ \land k \in ℕ_{0}) \to coeff (G) : ℕ_{0} ⟶ ℤ$
53		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
54	35	adantr	$⊢ (φ \land k \in ℕ_{0}) \to M \in ℕ_{0}$
55	53 54	nn0addcld	$⊢ (φ \land k \in ℕ_{0}) \to k + M \in ℕ_{0}$
56	52 55	ffvelrnd	$⊢ (φ \land k \in ℕ_{0}) \to coeff (G) (k + M) \in ℤ$
57	56 7	fmptd	$⊢ φ \to I : ℕ_{0} ⟶ ℤ$
58		elplyr	$⊢ (ℤ \subseteq ℂ \land \deg (G) - M \in ℕ_{0} \land I : ℕ_{0} ⟶ ℤ) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} I (k) z^{k}) \in Poly (ℤ)$
59	11 48 57 58	syl3anc	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} I (k) z^{k}) \in Poly (ℤ)$
60	9 59	eqeltrd	$⊢ φ \to F \in Poly (ℤ)$
61		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land k \leq \deg (G) - M) \to k \leq \deg (G) - M$
62	61	iftrued	$⊢ ((φ \land k \in ℕ_{0}) \land k \leq \deg (G) - M) \to if (k \leq \deg (G) - M, coeff (G) (k + M), 0) = coeff (G) (k + M)$
63		iffalse	$⊢ \neg k \leq \deg (G) - M \to if (k \leq \deg (G) - M, coeff (G) (k + M), 0) = 0$
64	63	adantl	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to if (k \leq \deg (G) - M, coeff (G) (k + M), 0) = 0$
65		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to \neg k \leq \deg (G) - M$
66	42	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to \deg (G) \in ℝ$
67	43	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to M \in ℝ$
68	66 67	resubcld	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to \deg (G) - M \in ℝ$
69		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
70	69	ad2antlr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to k \in ℝ$
71	68 70	ltnled	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to (\deg (G) - M < k \leftrightarrow \neg k \leq \deg (G) - M)$
72	65 71	mpbird	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to \deg (G) - M < k$
73	66 67 70	ltsubaddd	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to (\deg (G) - M < k \leftrightarrow \deg (G) < k + M)$
74	72 73	mpbid	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to \deg (G) < k + M$
75		olc	$⊢ \deg (G) < k + M \to (G = 0_{𝑝} \lor \deg (G) < k + M)$
76	74 75	syl	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to (G = 0_{𝑝} \lor \deg (G) < k + M)$
77	3	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to G \in Poly (ℤ)$
78	55	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to k + M \in ℕ_{0}$
79	20 21	dgrlt	$⊢ (G \in Poly (ℤ) \land k + M \in ℕ_{0}) \to ((G = 0_{𝑝} \lor \deg (G) < k + M) \leftrightarrow (\deg (G) \leq k + M \land coeff (G) (k + M) = 0))$
80	77 78 79	syl2anc	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to ((G = 0_{𝑝} \lor \deg (G) < k + M) \leftrightarrow (\deg (G) \leq k + M \land coeff (G) (k + M) = 0))$
81	76 80	mpbid	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to (\deg (G) \leq k + M \land coeff (G) (k + M) = 0)$
82	81	simprd	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to coeff (G) (k + M) = 0$
83	64 82	eqtr4d	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \leq \deg (G) - M) \to if (k \leq \deg (G) - M, coeff (G) (k + M), 0) = coeff (G) (k + M)$
84	62 83	pm2.61dan	$⊢ (φ \land k \in ℕ_{0}) \to if (k \leq \deg (G) - M, coeff (G) (k + M), 0) = coeff (G) (k + M)$
85	84	mpteq2dva	$⊢ φ \to (k \in ℕ_{0} ⟼ if (k \leq \deg (G) - M, coeff (G) (k + M), 0)) = (k \in ℕ_{0} ⟼ coeff (G) (k + M))$
86	51 11	fssd	$⊢ φ \to coeff (G) : ℕ_{0} ⟶ ℂ$
87	86	adantr	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to coeff (G) : ℕ_{0} ⟶ ℂ$
88		elfznn0	$⊢ k \in (0 \dots \deg (G) - M) \to k \in ℕ_{0}$
89	88	adantl	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to k \in ℕ_{0}$
90	35	adantr	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to M \in ℕ_{0}$
91	89 90	nn0addcld	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to k + M \in ℕ_{0}$
92	87 91	ffvelrnd	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to coeff (G) (k + M) \in ℂ$
93		eqidd	$⊢ (φ \land z \in ℂ) \to (0 \dots \deg (G) - M) = (0 \dots \deg (G) - M)$
94		simpl	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to φ$
95	7	a1i	$⊢ φ \to I = (k \in ℕ_{0} ⟼ coeff (G) (k + M))$
96	95 56	fvmpt2d	$⊢ (φ \land k \in ℕ_{0}) \to I (k) = coeff (G) (k + M)$
97	94 89 96	syl2anc	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to I (k) = coeff (G) (k + M)$
98	97	adantlr	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots \deg (G) - M)) \to I (k) = coeff (G) (k + M)$
99	98	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots \deg (G) - M)) \to I (k) z^{k} = coeff (G) (k + M) z^{k}$
100	93 99	sumeq12rdv	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{\deg (G) - M} I (k) z^{k} = \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) z^{k}$
101	100	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} I (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) z^{k})$
102	9 101	eqtrd	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) z^{k})$
103	60 48 92 102	coeeq2	$⊢ φ \to coeff (F) = (k \in ℕ_{0} ⟼ if (k \leq \deg (G) - M, coeff (G) (k + M), 0))$
104	85 103 95	3eqtr4d	$⊢ φ \to coeff (F) = I$
105	104	fveq1d	$⊢ φ \to coeff (F) (0) = I (0)$
106		oveq1	$⊢ k = 0 \to k + M = 0 + M$
107	106	adantl	$⊢ (φ \land k = 0) \to k + M = 0 + M$
108	10 36	sseldi	$⊢ φ \to M \in ℂ$
109	108	addid2d	$⊢ φ \to 0 + M = M$
110	109	adantr	$⊢ (φ \land k = 0) \to 0 + M = M$
111	107 110	eqtrd	$⊢ (φ \land k = 0) \to k + M = M$
112	111	fveq2d	$⊢ (φ \land k = 0) \to coeff (G) (k + M) = coeff (G) (M)$
113		0nn0	$⊢ 0 \in ℕ_{0}$
114	113	a1i	$⊢ φ \to 0 \in ℕ_{0}$
115	51 35	ffvelrnd	$⊢ φ \to coeff (G) (M) \in ℤ$
116	95 112 114 115	fvmptd	$⊢ φ \to I (0) = coeff (G) (M)$
117		eqidd	$⊢ φ \to coeff (G) (M) = coeff (G) (M)$
118	105 116 117	3eqtrd	$⊢ φ \to coeff (F) (0) = coeff (G) (M)$
119	38 33	eqeltrd	$⊢ φ \to M \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}$
120		fveq2	$⊢ n = M \to coeff (G) (n) = coeff (G) (M)$
121	120	neeq1d	$⊢ n = M \to (coeff (G) (n) \neq 0 \leftrightarrow coeff (G) (M) \neq 0)$
122	121	elrab	$⊢ M \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \leftrightarrow (M \in ℕ_{0} \land coeff (G) (M) \neq 0)$
123	119 122	sylib	$⊢ φ \to (M \in ℕ_{0} \land coeff (G) (M) \neq 0)$
124	123	simprd	$⊢ φ \to coeff (G) (M) \neq 0$
125	118 124	eqnetrd	$⊢ φ \to coeff (F) (0) \neq 0$
126	3 49	syl	$⊢ φ \to 0 \in ℤ$
127		aasscn	$⊢ 𝔸 \subseteq ℂ$
128	127 1	sseldi	$⊢ φ \to A \in ℂ$
129	94 128	syl	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to A \in ℂ$
130	129 89	expcld	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to A^{k} \in ℂ$
131	92 130	mulcld	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to coeff (G) (k + M) A^{k} \in ℂ$
132		fvoveq1	$⊢ k = j - M \to coeff (G) (k + M) = coeff (G) (j - M + M)$
133		oveq2	$⊢ k = j - M \to A^{k} = A^{j - M}$
134	132 133	oveq12d	$⊢ k = j - M \to coeff (G) (k + M) A^{k} = coeff (G) (j - M + M) A^{j - M}$
135	36 126 37 131 134	fsumshft	$⊢ φ \to \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) A^{k} = \sum_{j = 0 + M}^{\deg (G) - M + M} coeff (G) (j - M + M) A^{j - M}$
136	10 14	sseldi	$⊢ φ \to \deg (G) \in ℂ$
137	136 108	npcand	$⊢ φ \to \deg (G) - M + M = \deg (G)$
138	109 137	oveq12d	$⊢ φ \to (0 + M \dots \deg (G) - M + M) = (M \dots \deg (G))$
139	138	sumeq1d	$⊢ φ \to \sum_{j = 0 + M}^{\deg (G) - M + M} coeff (G) (j - M + M) A^{j - M} = \sum_{j = M}^{\deg (G)} coeff (G) (j - M + M) A^{j - M}$
140		elfzelz	$⊢ j \in (M \dots \deg (G)) \to j \in ℤ$
141	140	adantl	$⊢ (φ \land j \in (M \dots \deg (G))) \to j \in ℤ$
142	10 141	sseldi	$⊢ (φ \land j \in (M \dots \deg (G))) \to j \in ℂ$
143	108	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to M \in ℂ$
144	142 143	npcand	$⊢ (φ \land j \in (M \dots \deg (G))) \to j - M + M = j$
145	144	fveq2d	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j - M + M) = coeff (G) (j)$
146	145	oveq1d	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j - M + M) A^{j - M} = coeff (G) (j) A^{j - M}$
147	128	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to A \in ℂ$
148	2	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to A \neq 0$
149	36	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to M \in ℤ$
150	147 148 149 141	expsubd	$⊢ (φ \land j \in (M \dots \deg (G))) \to A^{j - M} = \frac{A^{j}}{A^{M}}$
151	150	oveq2d	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j) A^{j - M} = coeff (G) (j) (\frac{A^{j}}{A^{M}})$
152	86	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) : ℕ_{0} ⟶ ℂ$
153		0red	$⊢ (φ \land j \in (M \dots \deg (G))) \to 0 \in ℝ$
154	43	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to M \in ℝ$
155	141	zred	$⊢ (φ \land j \in (M \dots \deg (G))) \to j \in ℝ$
156	35	nn0ge0d	$⊢ φ \to 0 \leq M$
157	156	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to 0 \leq M$
158		elfzle1	$⊢ j \in (M \dots \deg (G)) \to M \leq j$
159	158	adantl	$⊢ (φ \land j \in (M \dots \deg (G))) \to M \leq j$
160	153 154 155 157 159	letrd	$⊢ (φ \land j \in (M \dots \deg (G))) \to 0 \leq j$
161	141 160	jca	$⊢ (φ \land j \in (M \dots \deg (G))) \to (j \in ℤ \land 0 \leq j)$
162		elnn0z	$⊢ j \in ℕ_{0} \leftrightarrow (j \in ℤ \land 0 \leq j)$
163	161 162	sylibr	$⊢ (φ \land j \in (M \dots \deg (G))) \to j \in ℕ_{0}$
164	152 163	ffvelrnd	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j) \in ℂ$
165	147 163	expcld	$⊢ (φ \land j \in (M \dots \deg (G))) \to A^{j} \in ℂ$
166	128 35	expcld	$⊢ φ \to A^{M} \in ℂ$
167	166	adantr	$⊢ (φ \land j \in (M \dots \deg (G))) \to A^{M} \in ℂ$
168	147 148 149	expne0d	$⊢ (φ \land j \in (M \dots \deg (G))) \to A^{M} \neq 0$
169	164 165 167 168	divassd	$⊢ (φ \land j \in (M \dots \deg (G))) \to \frac{coeff (G) (j) A^{j}}{A^{M}} = coeff (G) (j) (\frac{A^{j}}{A^{M}})$
170	169	eqcomd	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j) (\frac{A^{j}}{A^{M}}) = \frac{coeff (G) (j) A^{j}}{A^{M}}$
171	151 170	eqtr2d	$⊢ (φ \land j \in (M \dots \deg (G))) \to \frac{coeff (G) (j) A^{j}}{A^{M}} = coeff (G) (j) A^{j - M}$
172	146 171	eqtr4d	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j - M + M) A^{j - M} = \frac{coeff (G) (j) A^{j}}{A^{M}}$
173	172	sumeq2dv	$⊢ φ \to \sum_{j = M}^{\deg (G)} coeff (G) (j - M + M) A^{j - M} = \sum_{j = M}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}})$
174	139 173	eqtrd	$⊢ φ \to \sum_{j = 0 + M}^{\deg (G) - M + M} coeff (G) (j - M + M) A^{j - M} = \sum_{j = M}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}})$
175	35 16	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
176		fzss1	$⊢ M \in ℤ_{\geq 0} \to (M \dots \deg (G)) \subseteq (0 \dots \deg (G))$
177	175 176	syl	$⊢ φ \to (M \dots \deg (G)) \subseteq (0 \dots \deg (G))$
178	164 165	mulcld	$⊢ (φ \land j \in (M \dots \deg (G))) \to coeff (G) (j) A^{j} \in ℂ$
179	178 167 168	divcld	$⊢ (φ \land j \in (M \dots \deg (G))) \to \frac{coeff (G) (j) A^{j}}{A^{M}} \in ℂ$
180	36	ad2antrr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to M \in ℤ$
181	14	ad2antrr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to \deg (G) \in ℤ$
182		eldifi	$⊢ j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \to j \in (0 \dots \deg (G))$
183		elfznn0	$⊢ j \in (0 \dots \deg (G)) \to j \in ℕ_{0}$
184	183	nn0zd	$⊢ j \in (0 \dots \deg (G)) \to j \in ℤ$
185	182 184	syl	$⊢ j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \to j \in ℤ$
186	185	ad2antlr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to j \in ℤ$
187	180 181 186	3jca	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to (M \in ℤ \land \deg (G) \in ℤ \land j \in ℤ)$
188		simpr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to \neg j < M$
189	43	ad2antrr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to M \in ℝ$
190	186	zred	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to j \in ℝ$
191	189 190	lenltd	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to (M \leq j \leftrightarrow \neg j < M)$
192	188 191	mpbird	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to M \leq j$
193		elfzle2	$⊢ j \in (0 \dots \deg (G)) \to j \leq \deg (G)$
194	182 193	syl	$⊢ j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \to j \leq \deg (G)$
195	194	ad2antlr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to j \leq \deg (G)$
196	187 192 195	jca32	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to ((M \in ℤ \land \deg (G) \in ℤ \land j \in ℤ) \land (M \leq j \land j \leq \deg (G)))$
197		elfz2	$⊢ j \in (M \dots \deg (G)) \leftrightarrow ((M \in ℤ \land \deg (G) \in ℤ \land j \in ℤ) \land (M \leq j \land j \leq \deg (G)))$
198	196 197	sylibr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to j \in (M \dots \deg (G))$
199		eldifn	$⊢ j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \to \neg j \in (M \dots \deg (G))$
200	199	ad2antlr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg j < M) \to \neg j \in (M \dots \deg (G))$
201	198 200	condan	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to j < M$
202	201	adantr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to j < M$
203	6	a1i	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to M = sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <)$
204	17	a1i	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℤ_{\geq 0}$
205	182 183	syl	$⊢ j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \to j \in ℕ_{0}$
206	205	adantr	$⊢ (j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \land \neg coeff (G) (j) = 0) \to j \in ℕ_{0}$
207		neqne	$⊢ \neg coeff (G) (j) = 0 \to coeff (G) (j) \neq 0$
208	207	adantl	$⊢ (j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \land \neg coeff (G) (j) = 0) \to coeff (G) (j) \neq 0$
209	206 208	jca	$⊢ (j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \land \neg coeff (G) (j) = 0) \to (j \in ℕ_{0} \land coeff (G) (j) \neq 0)$
210		fveq2	$⊢ n = j \to coeff (G) (n) = coeff (G) (j)$
211	210	neeq1d	$⊢ n = j \to (coeff (G) (n) \neq 0 \leftrightarrow coeff (G) (j) \neq 0)$
212	211	elrab	$⊢ j \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \leftrightarrow (j \in ℕ_{0} \land coeff (G) (j) \neq 0)$
213	209 212	sylibr	$⊢ (j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \land \neg coeff (G) (j) = 0) \to j \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}$
214	213	adantll	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to j \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}$
215		infssuzle	$⊢ (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} \subseteq ℤ_{\geq 0} \land j \in \{n \in ℕ_{0} \| coeff (G) (n) \neq 0\}) \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \leq j$
216	204 214 215	syl2anc	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to sup (\{n \in ℕ_{0} \| coeff (G) (n) \neq 0\} ℝ <) \leq j$
217	203 216	eqbrtrd	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to M \leq j$
218	43	ad2antrr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to M \in ℝ$
219	185	zred	$⊢ j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G))) \to j \in ℝ$
220	219	ad2antlr	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to j \in ℝ$
221	218 220	lenltd	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to (M \leq j \leftrightarrow \neg j < M)$
222	217 221	mpbid	$⊢ ((φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \land \neg coeff (G) (j) = 0) \to \neg j < M$
223	202 222	condan	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to coeff (G) (j) = 0$
224	223	oveq1d	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to coeff (G) (j) A^{j} = 0 \cdot A^{j}$
225	128	adantr	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to A \in ℂ$
226	205	adantl	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to j \in ℕ_{0}$
227	225 226	expcld	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to A^{j} \in ℂ$
228	227	mul02d	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to 0 \cdot A^{j} = 0$
229	224 228	eqtrd	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to coeff (G) (j) A^{j} = 0$
230	229	oveq1d	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to \frac{coeff (G) (j) A^{j}}{A^{M}} = \frac{0}{A^{M}}$
231	128 2 36	expne0d	$⊢ φ \to A^{M} \neq 0$
232	166 231	div0d	$⊢ φ \to \frac{0}{A^{M}} = 0$
233	232	adantr	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to \frac{0}{A^{M}} = 0$
234	230 233	eqtrd	$⊢ (φ \land j \in ((0 \dots \deg (G)) ∖ (M \dots \deg (G)))) \to \frac{coeff (G) (j) A^{j}}{A^{M}} = 0$
235		fzfid	$⊢ φ \to (0 \dots \deg (G)) \in Fin$
236	177 179 234 235	fsumss	$⊢ φ \to \sum_{j = M}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}}) = \sum_{j = 0}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}})$
237	135 174 236	3eqtrd	$⊢ φ \to \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) A^{k} = \sum_{j = 0}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}})$
238	89 56	syldan	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to coeff (G) (k + M) \in ℤ$
239	7	fvmpt2	$⊢ (k \in ℕ_{0} \land coeff (G) (k + M) \in ℤ) \to I (k) = coeff (G) (k + M)$
240	89 238 239	syl2anc	$⊢ (φ \land k \in (0 \dots \deg (G) - M)) \to I (k) = coeff (G) (k + M)$
241	240	adantlr	$⊢ ((φ \land z = A) \land k \in (0 \dots \deg (G) - M)) \to I (k) = coeff (G) (k + M)$
242		oveq1	$⊢ z = A \to z^{k} = A^{k}$
243	242	ad2antlr	$⊢ ((φ \land z = A) \land k \in (0 \dots \deg (G) - M)) \to z^{k} = A^{k}$
244	241 243	oveq12d	$⊢ ((φ \land z = A) \land k \in (0 \dots \deg (G) - M)) \to I (k) z^{k} = coeff (G) (k + M) A^{k}$
245	244	sumeq2dv	$⊢ (φ \land z = A) \to \sum_{k = 0}^{\deg (G) - M} I (k) z^{k} = \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) A^{k}$
246		fzfid	$⊢ φ \to (0 \dots \deg (G) - M) \in Fin$
247	246 131	fsumcl	$⊢ φ \to \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) A^{k} \in ℂ$
248	9 245 128 247	fvmptd	$⊢ φ \to F (A) = \sum_{k = 0}^{\deg (G) - M} coeff (G) (k + M) A^{k}$
249	21 20	coeid2	$⊢ (G \in Poly (ℤ) \land A \in ℂ) \to G (A) = \sum_{j = 0}^{\deg (G)} coeff (G) (j) A^{j}$
250	3 128 249	syl2anc	$⊢ φ \to G (A) = \sum_{j = 0}^{\deg (G)} coeff (G) (j) A^{j}$
251	250	oveq1d	$⊢ φ \to \frac{G (A)}{A^{M}} = \frac{\sum_{j = 0}^{\deg (G)} coeff (G) (j) A^{j}}{A^{M}}$
252	86	adantr	$⊢ (φ \land j \in (0 \dots \deg (G))) \to coeff (G) : ℕ_{0} ⟶ ℂ$
253	183	adantl	$⊢ (φ \land j \in (0 \dots \deg (G))) \to j \in ℕ_{0}$
254	252 253	ffvelrnd	$⊢ (φ \land j \in (0 \dots \deg (G))) \to coeff (G) (j) \in ℂ$
255	128	adantr	$⊢ (φ \land j \in (0 \dots \deg (G))) \to A \in ℂ$
256	255 253	expcld	$⊢ (φ \land j \in (0 \dots \deg (G))) \to A^{j} \in ℂ$
257	254 256	mulcld	$⊢ (φ \land j \in (0 \dots \deg (G))) \to coeff (G) (j) A^{j} \in ℂ$
258	235 166 257 231	fsumdivc	$⊢ φ \to \frac{\sum_{j = 0}^{\deg (G)} coeff (G) (j) A^{j}}{A^{M}} = \sum_{j = 0}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}})$
259	251 258	eqtrd	$⊢ φ \to \frac{G (A)}{A^{M}} = \sum_{j = 0}^{\deg (G)} (\frac{coeff (G) (j) A^{j}}{A^{M}})$
260	237 248 259	3eqtr4d	$⊢ φ \to F (A) = \frac{G (A)}{A^{M}}$
261	5	oveq1d	$⊢ φ \to \frac{G (A)}{A^{M}} = \frac{0}{A^{M}}$
262	260 261 232	3eqtrd	$⊢ φ \to F (A) = 0$
263	125 262	jca	$⊢ φ \to (coeff (F) (0) \neq 0 \land F (A) = 0)$
264		fveq2	$⊢ f = F \to coeff (f) = coeff (F)$
265	264	fveq1d	$⊢ f = F \to coeff (f) (0) = coeff (F) (0)$
266	265	neeq1d	$⊢ f = F \to (coeff (f) (0) \neq 0 \leftrightarrow coeff (F) (0) \neq 0)$
267		fveq1	$⊢ f = F \to f (A) = F (A)$
268	267	eqeq1d	$⊢ f = F \to (f (A) = 0 \leftrightarrow F (A) = 0)$
269	266 268	anbi12d	$⊢ f = F \to ((coeff (f) (0) \neq 0 \land f (A) = 0) \leftrightarrow (coeff (F) (0) \neq 0 \land F (A) = 0))$
270	269	rspcev	$⊢ (F \in Poly (ℤ) \land (coeff (F) (0) \neq 0 \land F (A) = 0)) \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$
271	60 263 270	syl2anc	$⊢ φ \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$

Metamath Proof Explorer

Theorem elaa2lem

Proof