elaa2

Description: Elementhood in the set of nonzero algebraic numbers: when A is nonzero, the polynomial f can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Proof shortened by AV, 1-Oct-2020)

		Ref	Expression
	Assertion	elaa2	$⊢ A \in (𝔸 ∖ \{0\}) \leftrightarrow (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0))$

Proof

Step	Hyp	Ref	Expression
1		aasscn	$⊢ 𝔸 \subseteq ℂ$
2		eldifi	$⊢ A \in (𝔸 ∖ \{0\}) \to A \in 𝔸$
3	1 2	sselid	$⊢ A \in (𝔸 ∖ \{0\}) \to A \in ℂ$
4		elaa	$⊢ A \in 𝔸 \leftrightarrow (A \in ℂ \land \exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (A) = 0)$
5	2 4	sylib	$⊢ A \in (𝔸 ∖ \{0\}) \to (A \in ℂ \land \exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (A) = 0)$
6	5	simprd	$⊢ A \in (𝔸 ∖ \{0\}) \to \exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (A) = 0$
7	2	3ad2ant1	$⊢ (A \in (𝔸 ∖ \{0\}) \land g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land g (A) = 0) \to A \in 𝔸$
8		eldifsni	$⊢ A \in (𝔸 ∖ \{0\}) \to A \neq 0$
9	8	3ad2ant1	$⊢ (A \in (𝔸 ∖ \{0\}) \land g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land g (A) = 0) \to A \neq 0$
10		eldifi	$⊢ g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to g \in Poly (ℤ)$
11	10	3ad2ant2	$⊢ (A \in (𝔸 ∖ \{0\}) \land g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land g (A) = 0) \to g \in Poly (ℤ)$
12		eldifsni	$⊢ g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to g \neq 0_{𝑝}$
13	12	3ad2ant2	$⊢ (A \in (𝔸 ∖ \{0\}) \land g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land g (A) = 0) \to g \neq 0_{𝑝}$
14		simp3	$⊢ (A \in (𝔸 ∖ \{0\}) \land g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land g (A) = 0) \to g (A) = 0$
15		fveq2	$⊢ m = n \to coeff (g) (m) = coeff (g) (n)$
16	15	neeq1d	$⊢ m = n \to (coeff (g) (m) \neq 0 \leftrightarrow coeff (g) (n) \neq 0)$
17	16	cbvrabv	$⊢ \{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} = \{n \in ℕ_{0} \| coeff (g) (n) \neq 0\}$
18	17	infeq1i	$⊢ inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <) = inf (\{n \in ℕ_{0} \| coeff (g) (n) \neq 0\} ℝ <)$
19		fvoveq1	$⊢ j = k \to coeff (g) (j + inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <)) = coeff (g) (k + inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <))$
20	19	cbvmptv	$⊢ (j \in ℕ_{0} ⟼ coeff (g) (j + inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <))) = (k \in ℕ_{0} ⟼ coeff (g) (k + inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <)))$
21		eqid	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{\deg (g) - inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <)} (j \in ℕ_{0} ⟼ coeff (g) (j + inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <))) (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (g) - inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <)} (j \in ℕ_{0} ⟼ coeff (g) (j + inf (\{m \in ℕ_{0} \| coeff (g) (m) \neq 0\} ℝ <))) (k) z^{k})$
22	7 9 11 13 14 18 20 21	elaa2lem	$⊢ (A \in (𝔸 ∖ \{0\}) \land g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land g (A) = 0) \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$
23	22	rexlimdv3a	$⊢ A \in (𝔸 ∖ \{0\}) \to (\exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (A) = 0 \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0))$
24	6 23	mpd	$⊢ A \in (𝔸 ∖ \{0\}) \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$
25	3 24	jca	$⊢ A \in (𝔸 ∖ \{0\}) \to (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0))$
26		simpl	$⊢ (f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \to f \in Poly (ℤ)$
27		fveq2	$⊢ f = 0_{𝑝} \to coeff (f) = coeff (0_{𝑝})$
28		coe0	$⊢ coeff (0_{𝑝}) = ℕ_{0} \times \{0\}$
29	27 28	eqtrdi	$⊢ f = 0_{𝑝} \to coeff (f) = ℕ_{0} \times \{0\}$
30	29	fveq1d	$⊢ f = 0_{𝑝} \to coeff (f) (0) = (ℕ_{0} \times \{0\}) (0)$
31		0nn0	$⊢ 0 \in ℕ_{0}$
32		fvconst2g	$⊢ (0 \in ℕ_{0} \land 0 \in ℕ_{0}) \to (ℕ_{0} \times \{0\}) (0) = 0$
33	31 31 32	mp2an	$⊢ (ℕ_{0} \times \{0\}) (0) = 0$
34	30 33	eqtrdi	$⊢ f = 0_{𝑝} \to coeff (f) (0) = 0$
35	34	adantl	$⊢ ((f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \land f = 0_{𝑝}) \to coeff (f) (0) = 0$
36		neneq	$⊢ coeff (f) (0) \neq 0 \to \neg coeff (f) (0) = 0$
37	36	ad2antlr	$⊢ ((f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \land f = 0_{𝑝}) \to \neg coeff (f) (0) = 0$
38	35 37	pm2.65da	$⊢ (f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \to \neg f = 0_{𝑝}$
39		velsn	$⊢ f \in \{0_{𝑝}\} \leftrightarrow f = 0_{𝑝}$
40	38 39	sylnibr	$⊢ (f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \to \neg f \in \{0_{𝑝}\}$
41	26 40	eldifd	$⊢ (f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \to f \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
42	41	adantrr	$⊢ (f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \to f \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
43		simprr	$⊢ (f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \to f (A) = 0$
44	42 43	jca	$⊢ (f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \to (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)$
45	44	reximi2	$⊢ \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0) \to \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0$
46	45	anim2i	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to (A \in ℂ \land \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0)$
47		elaa	$⊢ A \in 𝔸 \leftrightarrow (A \in ℂ \land \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0)$
48	46 47	sylibr	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to A \in 𝔸$
49		simpr	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$
50		nfv	$⊢ Ⅎ f A \in ℂ$
51		nfre1	$⊢ Ⅎ f \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)$
52	50 51	nfan	$⊢ Ⅎ f (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0))$
53		nfv	$⊢ Ⅎ f \neg A \in \{0\}$
54		simpl3r	$⊢ ((A \in ℂ \land f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \land A = 0) \to f (A) = 0$
55		fveq2	$⊢ A = 0 \to f (A) = f (0)$
56		eqid	$⊢ coeff (f) = coeff (f)$
57	56	coefv0	$⊢ f \in Poly (ℤ) \to f (0) = coeff (f) (0)$
58	55 57	sylan9eqr	$⊢ (f \in Poly (ℤ) \land A = 0) \to f (A) = coeff (f) (0)$
59	58	adantlr	$⊢ ((f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \land A = 0) \to f (A) = coeff (f) (0)$
60		simplr	$⊢ ((f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \land A = 0) \to coeff (f) (0) \neq 0$
61	59 60	eqnetrd	$⊢ ((f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \land A = 0) \to f (A) \neq 0$
62	61	neneqd	$⊢ ((f \in Poly (ℤ) \land coeff (f) (0) \neq 0) \land A = 0) \to \neg f (A) = 0$
63	62	adantlrr	$⊢ ((f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \land A = 0) \to \neg f (A) = 0$
64	63	3adantl1	$⊢ ((A \in ℂ \land f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \land A = 0) \to \neg f (A) = 0$
65	54 64	pm2.65da	$⊢ (A \in ℂ \land f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \to \neg A = 0$
66		elsng	$⊢ A \in ℂ \to (A \in \{0\} \leftrightarrow A = 0)$
67	66	biimpa	$⊢ (A \in ℂ \land A \in \{0\}) \to A = 0$
68	67	3ad2antl1	$⊢ ((A \in ℂ \land f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \land A \in \{0\}) \to A = 0$
69	65 68	mtand	$⊢ (A \in ℂ \land f \in Poly (ℤ) \land (coeff (f) (0) \neq 0 \land f (A) = 0)) \to \neg A \in \{0\}$
70	69	3exp	$⊢ A \in ℂ \to (f \in Poly (ℤ) \to ((coeff (f) (0) \neq 0 \land f (A) = 0) \to \neg A \in \{0\}))$
71	70	adantr	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to (f \in Poly (ℤ) \to ((coeff (f) (0) \neq 0 \land f (A) = 0) \to \neg A \in \{0\}))$
72	52 53 71	rexlimd	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to (\exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0) \to \neg A \in \{0\})$
73	49 72	mpd	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to \neg A \in \{0\}$
74	48 73	eldifd	$⊢ (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0)) \to A \in (𝔸 ∖ \{0\})$
75	25 74	impbii	$⊢ A \in (𝔸 ∖ \{0\}) \leftrightarrow (A \in ℂ \land \exists f \in Poly (ℤ) (coeff (f) (0) \neq 0 \land f (A) = 0))$

Metamath Proof Explorer

Theorem elaa2

Proof