elqaalem3

Description: Lemma for elqaa . (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	elqaalem3	$⊢ φ \to A \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		cnex	$⊢ ℂ \in V$
8	7	a1i	$⊢ φ \to ℂ \in V$
9	6	fvexi	$⊢ R \in V$
10	9	a1i	$⊢ (φ \land z \in ℂ) \to R \in V$
11		fvexd	$⊢ (φ \land z \in ℂ) \to F (z) \in V$
12		fconstmpt	$⊢ ℂ \times \{R\} = (z \in ℂ ⟼ R)$
13	12	a1i	$⊢ φ \to ℂ \times \{R\} = (z \in ℂ ⟼ R)$
14	2	eldifad	$⊢ φ \to F \in Poly (ℚ)$
15		plyf	$⊢ F \in Poly (ℚ) \to F : ℂ ⟶ ℂ$
16	14 15	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
17	16	feqmptd	$⊢ φ \to F = (z \in ℂ ⟼ F (z))$
18	8 10 11 13 17	offval2	$⊢ φ \to (ℂ \times \{R\}) \times_{f} F = (z \in ℂ ⟼ R F (z))$
19		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots \deg (F)) \in Fin$
20		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
21		0zd	$⊢ φ \to 0 \in ℤ$
22		ssrab2	$⊢ \{n \in ℕ \| B (m) n \in ℤ\} \subseteq ℕ$
23		fveq2	$⊢ k = m \to B (k) = B (m)$
24	23	oveq1d	$⊢ k = m \to B (k) n = B (m) n$
25	24	eleq1d	$⊢ k = m \to (B (k) n \in ℤ \leftrightarrow B (m) n \in ℤ)$
26	25	rabbidv	$⊢ k = m \to \{n \in ℕ \| B (k) n \in ℤ\} = \{n \in ℕ \| B (m) n \in ℤ\}$
27	26	infeq1d	$⊢ k = m \to inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <) = inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <)$
28		ltso	$⊢ < Or ℝ$
29	28	infex	$⊢ inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <) \in V$
30	27 5 29	fvmpt	$⊢ m \in ℕ_{0} \to N (m) = inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <)$
31	30	adantl	$⊢ (φ \land m \in ℕ_{0}) \to N (m) = inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <)$
32		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
33	22 32	sseqtri	$⊢ \{n \in ℕ \| B (m) n \in ℤ\} \subseteq ℤ_{\geq 1}$
34		0z	$⊢ 0 \in ℤ$
35		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
36	34 35	ax-mp	$⊢ 0 \in ℚ$
37	4	coef2	$⊢ (F \in Poly (ℚ) \land 0 \in ℚ) \to B : ℕ_{0} ⟶ ℚ$
38	14 36 37	sylancl	$⊢ φ \to B : ℕ_{0} ⟶ ℚ$
39	38	ffvelcdmda	$⊢ (φ \land m \in ℕ_{0}) \to B (m) \in ℚ$
40		qmulz	$⊢ B (m) \in ℚ \to \exists n \in ℕ B (m) n \in ℤ$
41	39 40	syl	$⊢ (φ \land m \in ℕ_{0}) \to \exists n \in ℕ B (m) n \in ℤ$
42		rabn0	$⊢ \{n \in ℕ \| B (m) n \in ℤ\} \neq \emptyset \leftrightarrow \exists n \in ℕ B (m) n \in ℤ$
43	41 42	sylibr	$⊢ (φ \land m \in ℕ_{0}) \to \{n \in ℕ \| B (m) n \in ℤ\} \neq \emptyset$
44		infssuzcl	$⊢ (\{n \in ℕ \| B (m) n \in ℤ\} \subseteq ℤ_{\geq 1} \land \{n \in ℕ \| B (m) n \in ℤ\} \neq \emptyset) \to inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <) \in \{n \in ℕ \| B (m) n \in ℤ\}$
45	33 43 44	sylancr	$⊢ (φ \land m \in ℕ_{0}) \to inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <) \in \{n \in ℕ \| B (m) n \in ℤ\}$
46	31 45	eqeltrd	$⊢ (φ \land m \in ℕ_{0}) \to N (m) \in \{n \in ℕ \| B (m) n \in ℤ\}$
47	22 46	sselid	$⊢ (φ \land m \in ℕ_{0}) \to N (m) \in ℕ$
48		nnmulcl	$⊢ (m \in ℕ \land k \in ℕ) \to m k \in ℕ$
49	48	adantl	$⊢ (φ \land (m \in ℕ \land k \in ℕ)) \to m k \in ℕ$
50	20 21 47 49	seqf	$⊢ φ \to seq 0 (\times N) : ℕ_{0} ⟶ ℕ$
51		dgrcl	$⊢ F \in Poly (ℚ) \to \deg (F) \in ℕ_{0}$
52	14 51	syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
53	50 52	ffvelcdmd	$⊢ φ \to seq 0 (\times N) (\deg (F)) \in ℕ$
54	6 53	eqeltrid	$⊢ φ \to R \in ℕ$
55	54	nncnd	$⊢ φ \to R \in ℂ$
56	55	adantr	$⊢ (φ \land z \in ℂ) \to R \in ℂ$
57		elfznn0	$⊢ m \in (0 \dots \deg (F)) \to m \in ℕ_{0}$
58	4	coef3	$⊢ F \in Poly (ℚ) \to B : ℕ_{0} ⟶ ℂ$
59	14 58	syl	$⊢ φ \to B : ℕ_{0} ⟶ ℂ$
60	59	adantr	$⊢ (φ \land z \in ℂ) \to B : ℕ_{0} ⟶ ℂ$
61	60	ffvelcdmda	$⊢ ((φ \land z \in ℂ) \land m \in ℕ_{0}) \to B (m) \in ℂ$
62		expcl	$⊢ (z \in ℂ \land m \in ℕ_{0}) \to z^{m} \in ℂ$
63	62	adantll	$⊢ ((φ \land z \in ℂ) \land m \in ℕ_{0}) \to z^{m} \in ℂ$
64	61 63	mulcld	$⊢ ((φ \land z \in ℂ) \land m \in ℕ_{0}) \to B (m) z^{m} \in ℂ$
65	57 64	sylan2	$⊢ ((φ \land z \in ℂ) \land m \in (0 \dots \deg (F))) \to B (m) z^{m} \in ℂ$
66	19 56 65	fsummulc2	$⊢ (φ \land z \in ℂ) \to R \sum_{m = 0}^{\deg (F)} B (m) z^{m} = \sum_{m = 0}^{\deg (F)} R B (m) z^{m}$
67		eqid	$⊢ \deg (F) = \deg (F)$
68	4 67	coeid2	$⊢ (F \in Poly (ℚ) \land z \in ℂ) \to F (z) = \sum_{m = 0}^{\deg (F)} B (m) z^{m}$
69	14 68	sylan	$⊢ (φ \land z \in ℂ) \to F (z) = \sum_{m = 0}^{\deg (F)} B (m) z^{m}$
70	69	oveq2d	$⊢ (φ \land z \in ℂ) \to R F (z) = R \sum_{m = 0}^{\deg (F)} B (m) z^{m}$
71	56	adantr	$⊢ ((φ \land z \in ℂ) \land m \in ℕ_{0}) \to R \in ℂ$
72	71 61 63	mulassd	$⊢ ((φ \land z \in ℂ) \land m \in ℕ_{0}) \to R B (m) z^{m} = R B (m) z^{m}$
73	57 72	sylan2	$⊢ ((φ \land z \in ℂ) \land m \in (0 \dots \deg (F))) \to R B (m) z^{m} = R B (m) z^{m}$
74	73	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{m = 0}^{\deg (F)} R B (m) z^{m} = \sum_{m = 0}^{\deg (F)} R B (m) z^{m}$
75	66 70 74	3eqtr4d	$⊢ (φ \land z \in ℂ) \to R F (z) = \sum_{m = 0}^{\deg (F)} R B (m) z^{m}$
76	75	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ R F (z)) = (z \in ℂ ⟼ \sum_{m = 0}^{\deg (F)} R B (m) z^{m})$
77	18 76	eqtrd	$⊢ φ \to (ℂ \times \{R\}) \times_{f} F = (z \in ℂ ⟼ \sum_{m = 0}^{\deg (F)} R B (m) z^{m})$
78		zsscn	$⊢ ℤ \subseteq ℂ$
79	78	a1i	$⊢ φ \to ℤ \subseteq ℂ$
80	55	adantr	$⊢ (φ \land m \in ℕ_{0}) \to R \in ℂ$
81	47	nncnd	$⊢ (φ \land m \in ℕ_{0}) \to N (m) \in ℂ$
82	47	nnne0d	$⊢ (φ \land m \in ℕ_{0}) \to N (m) \neq 0$
83	80 81 82	divcan2d	$⊢ (φ \land m \in ℕ_{0}) \to N (m) (\frac{R}{N (m)}) = R$
84	83	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to B (m) N (m) (\frac{R}{N (m)}) = B (m) R$
85	59	ffvelcdmda	$⊢ (φ \land m \in ℕ_{0}) \to B (m) \in ℂ$
86	80 81 82	divcld	$⊢ (φ \land m \in ℕ_{0}) \to \frac{R}{N (m)} \in ℂ$
87	85 81 86	mulassd	$⊢ (φ \land m \in ℕ_{0}) \to B (m) N (m) (\frac{R}{N (m)}) = B (m) N (m) (\frac{R}{N (m)})$
88	80 85	mulcomd	$⊢ (φ \land m \in ℕ_{0}) \to R B (m) = B (m) R$
89	84 87 88	3eqtr4rd	$⊢ (φ \land m \in ℕ_{0}) \to R B (m) = B (m) N (m) (\frac{R}{N (m)})$
90	57 89	sylan2	$⊢ (φ \land m \in (0 \dots \deg (F))) \to R B (m) = B (m) N (m) (\frac{R}{N (m)})$
91		oveq2	$⊢ n = N (m) \to B (m) n = B (m) N (m)$
92	91	eleq1d	$⊢ n = N (m) \to (B (m) n \in ℤ \leftrightarrow B (m) N (m) \in ℤ)$
93	92	elrab	$⊢ N (m) \in \{n \in ℕ \| B (m) n \in ℤ\} \leftrightarrow (N (m) \in ℕ \land B (m) N (m) \in ℤ)$
94	93	simprbi	$⊢ N (m) \in \{n \in ℕ \| B (m) n \in ℤ\} \to B (m) N (m) \in ℤ$
95	46 94	syl	$⊢ (φ \land m \in ℕ_{0}) \to B (m) N (m) \in ℤ$
96	57 95	sylan2	$⊢ (φ \land m \in (0 \dots \deg (F))) \to B (m) N (m) \in ℤ$
97		eqid	$⊢ (x \in V, y \in V ⟼ x y \mod N (m)) = (x \in V, y \in V ⟼ x y \mod N (m))$
98	1 2 3 4 5 6 97	elqaalem2	$⊢ (φ \land m \in (0 \dots \deg (F))) \to R \mod N (m) = 0$
99	54	adantr	$⊢ (φ \land m \in (0 \dots \deg (F))) \to R \in ℕ$
100	57 47	sylan2	$⊢ (φ \land m \in (0 \dots \deg (F))) \to N (m) \in ℕ$
101		nnre	$⊢ R \in ℕ \to R \in ℝ$
102		nnrp	$⊢ N (m) \in ℕ \to N (m) \in ℝ^{+}$
103		mod0	$⊢ (R \in ℝ \land N (m) \in ℝ^{+}) \to (R \mod N (m) = 0 \leftrightarrow \frac{R}{N (m)} \in ℤ)$
104	101 102 103	syl2an	$⊢ (R \in ℕ \land N (m) \in ℕ) \to (R \mod N (m) = 0 \leftrightarrow \frac{R}{N (m)} \in ℤ)$
105	99 100 104	syl2anc	$⊢ (φ \land m \in (0 \dots \deg (F))) \to (R \mod N (m) = 0 \leftrightarrow \frac{R}{N (m)} \in ℤ)$
106	98 105	mpbid	$⊢ (φ \land m \in (0 \dots \deg (F))) \to \frac{R}{N (m)} \in ℤ$
107	96 106	zmulcld	$⊢ (φ \land m \in (0 \dots \deg (F))) \to B (m) N (m) (\frac{R}{N (m)}) \in ℤ$
108	90 107	eqeltrd	$⊢ (φ \land m \in (0 \dots \deg (F))) \to R B (m) \in ℤ$
109	79 52 108	elplyd	$⊢ φ \to (z \in ℂ ⟼ \sum_{m = 0}^{\deg (F)} R B (m) z^{m}) \in Poly (ℤ)$
110	77 109	eqeltrd	$⊢ φ \to (ℂ \times \{R\}) \times_{f} F \in Poly (ℤ)$
111		eldifsn	$⊢ F \in (Poly (ℚ) ∖ \{0_{𝑝}\}) \leftrightarrow (F \in Poly (ℚ) \land F \neq 0_{𝑝})$
112	2 111	sylib	$⊢ φ \to (F \in Poly (ℚ) \land F \neq 0_{𝑝})$
113	112	simprd	$⊢ φ \to F \neq 0_{𝑝}$
114		oveq1	$⊢ (ℂ \times \{R\}) \times_{f} F = 0_{𝑝} \to ((ℂ \times \{R\}) \times_{f} F) \div_{f} (ℂ \times \{R\}) = 0_{𝑝} \div_{f} (ℂ \times \{R\})$
115	16	ffvelcdmda	$⊢ (φ \land z \in ℂ) \to F (z) \in ℂ$
116	54	nnne0d	$⊢ φ \to R \neq 0$
117	116	adantr	$⊢ (φ \land z \in ℂ) \to R \neq 0$
118	115 56 117	divcan3d	$⊢ (φ \land z \in ℂ) \to \frac{R F (z)}{R} = F (z)$
119	118	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ \frac{R F (z)}{R}) = (z \in ℂ ⟼ F (z))$
120		ovexd	$⊢ (φ \land z \in ℂ) \to R F (z) \in V$
121	8 120 10 18 13	offval2	$⊢ φ \to ((ℂ \times \{R\}) \times_{f} F) \div_{f} (ℂ \times \{R\}) = (z \in ℂ ⟼ \frac{R F (z)}{R})$
122	119 121 17	3eqtr4d	$⊢ φ \to ((ℂ \times \{R\}) \times_{f} F) \div_{f} (ℂ \times \{R\}) = F$
123	55 116	div0d	$⊢ φ \to \frac{0}{R} = 0$
124	123	mpteq2dv	$⊢ φ \to (z \in ℂ ⟼ \frac{0}{R}) = (z \in ℂ ⟼ 0)$
125		0cnd	$⊢ (φ \land z \in ℂ) \to 0 \in ℂ$
126		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
127		fconstmpt	$⊢ ℂ \times \{0\} = (z \in ℂ ⟼ 0)$
128	126 127	eqtri	$⊢ 0_{𝑝} = (z \in ℂ ⟼ 0)$
129	128	a1i	$⊢ φ \to 0_{𝑝} = (z \in ℂ ⟼ 0)$
130	8 125 10 129 13	offval2	$⊢ φ \to 0_{𝑝} \div_{f} (ℂ \times \{R\}) = (z \in ℂ ⟼ \frac{0}{R})$
131	124 130 129	3eqtr4d	$⊢ φ \to 0_{𝑝} \div_{f} (ℂ \times \{R\}) = 0_{𝑝}$
132	122 131	eqeq12d	$⊢ φ \to (((ℂ \times \{R\}) \times_{f} F) \div_{f} (ℂ \times \{R\}) = 0_{𝑝} \div_{f} (ℂ \times \{R\}) \leftrightarrow F = 0_{𝑝})$
133	114 132	imbitrid	$⊢ φ \to ((ℂ \times \{R\}) \times_{f} F = 0_{𝑝} \to F = 0_{𝑝})$
134	133	necon3d	$⊢ φ \to (F \neq 0_{𝑝} \to (ℂ \times \{R\}) \times_{f} F \neq 0_{𝑝})$
135	113 134	mpd	$⊢ φ \to (ℂ \times \{R\}) \times_{f} F \neq 0_{𝑝}$
136		eldifsn	$⊢ (ℂ \times \{R\}) \times_{f} F \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \leftrightarrow ((ℂ \times \{R\}) \times_{f} F \in Poly (ℤ) \land (ℂ \times \{R\}) \times_{f} F \neq 0_{𝑝})$
137	110 135 136	sylanbrc	$⊢ φ \to (ℂ \times \{R\}) \times_{f} F \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
138	9	fconst	$⊢ (ℂ \times \{R\}) : ℂ ⟶ \{R\}$
139		ffn	$⊢ (ℂ \times \{R\}) : ℂ ⟶ \{R\} \to (ℂ \times \{R\}) Fn ℂ$
140	138 139	mp1i	$⊢ φ \to (ℂ \times \{R\}) Fn ℂ$
141	16	ffnd	$⊢ φ \to F Fn ℂ$
142		inidm	$⊢ ℂ \cap ℂ = ℂ$
143	9	fvconst2	$⊢ A \in ℂ \to (ℂ \times \{R\}) (A) = R$
144	143	adantl	$⊢ (φ \land A \in ℂ) \to (ℂ \times \{R\}) (A) = R$
145	3	adantr	$⊢ (φ \land A \in ℂ) \to F (A) = 0$
146	140 141 8 8 142 144 145	ofval	$⊢ (φ \land A \in ℂ) \to ((ℂ \times \{R\}) \times_{f} F) (A) = R \cdot 0$
147	1 146	mpdan	$⊢ φ \to ((ℂ \times \{R\}) \times_{f} F) (A) = R \cdot 0$
148	55	mul01d	$⊢ φ \to R \cdot 0 = 0$
149	147 148	eqtrd	$⊢ φ \to ((ℂ \times \{R\}) \times_{f} F) (A) = 0$
150		fveq1	$⊢ f = (ℂ \times \{R\}) \times_{f} F \to f (A) = ((ℂ \times \{R\}) \times_{f} F) (A)$
151	150	eqeq1d	$⊢ f = (ℂ \times \{R\}) \times_{f} F \to (f (A) = 0 \leftrightarrow ((ℂ \times \{R\}) \times_{f} F) (A) = 0)$
152	151	rspcev	$⊢ ((ℂ \times \{R\}) \times_{f} F \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land ((ℂ \times \{R\}) \times_{f} F) (A) = 0) \to \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0$
153	137 149 152	syl2anc	$⊢ φ \to \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0$
154		elaa	$⊢ A \in 𝔸 \leftrightarrow (A \in ℂ \land \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0)$
155	1 153 154	sylanbrc	$⊢ φ \to A \in 𝔸$

Metamath Proof Explorer

Theorem elqaalem3

Proof