aareccl

Description: The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014)

		Ref	Expression
	Assertion	aareccl	$⊢ (A \in 𝔸 \land A \neq 0) \to \frac{1}{A} \in 𝔸$

Proof

Step	Hyp	Ref	Expression
1		elaa	$⊢ A \in 𝔸 \leftrightarrow (A \in ℂ \land \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0)$
2	1	simprbi	$⊢ A \in 𝔸 \to \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0$
3	2	adantr	$⊢ (A \in 𝔸 \land A \neq 0) \to \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (A) = 0$
4		aacn	$⊢ A \in 𝔸 \to A \in ℂ$
5		reccl	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \in ℂ$
6	4 5	sylan	$⊢ (A \in 𝔸 \land A \neq 0) \to \frac{1}{A} \in ℂ$
7	6	adantr	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \frac{1}{A} \in ℂ$
8		zsscn	$⊢ ℤ \subseteq ℂ$
9	8	a1i	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to ℤ \subseteq ℂ$
10		simprl	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to f \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
11		eldifsn	$⊢ f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \leftrightarrow (f \in Poly (ℤ) \land f \neq 0_{𝑝})$
12	10 11	sylib	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (f \in Poly (ℤ) \land f \neq 0_{𝑝})$
13	12	simpld	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to f \in Poly (ℤ)$
14		dgrcl	$⊢ f \in Poly (ℤ) \to \deg (f) \in ℕ_{0}$
15	13 14	syl	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \deg (f) \in ℕ_{0}$
16	13	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to f \in Poly (ℤ)$
17		0z	$⊢ 0 \in ℤ$
18		eqid	$⊢ coeff (f) = coeff (f)$
19	18	coef2	$⊢ (f \in Poly (ℤ) \land 0 \in ℤ) \to coeff (f) : ℕ_{0} ⟶ ℤ$
20	16 17 19	sylancl	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to coeff (f) : ℕ_{0} ⟶ ℤ$
21		fznn0sub	$⊢ k \in (0 \dots \deg (f)) \to \deg (f) - k \in ℕ_{0}$
22	21	adantl	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \deg (f) - k \in ℕ_{0}$
23	20 22	ffvelrnd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to coeff (f) (\deg (f) - k) \in ℤ$
24	9 15 23	elplyd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \in Poly (ℤ)$
25		0cn	$⊢ 0 \in ℂ$
26		eqid	$⊢ coeff ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})) = coeff ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}))$
27	26	coefv0	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \in Poly (ℤ) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (0) = coeff ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})) (0)$
28	24 27	syl	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (0) = coeff ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})) (0)$
29	23	zcnd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to coeff (f) (\deg (f) - k) \in ℂ$
30		eqidd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})$
31	24 15 29 30	coeeq2	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to coeff ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})) = (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0))$
32	31	fveq1d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to coeff ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})) (0) = (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0)) (0)$
33		0nn0	$⊢ 0 \in ℕ_{0}$
34		breq1	$⊢ k = 0 \to (k \leq \deg (f) \leftrightarrow 0 \leq \deg (f))$
35		oveq2	$⊢ k = 0 \to \deg (f) - k = \deg (f) - 0$
36	35	fveq2d	$⊢ k = 0 \to coeff (f) (\deg (f) - k) = coeff (f) (\deg (f) - 0)$
37	34 36	ifbieq1d	$⊢ k = 0 \to if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0) = if (0 \leq \deg (f), coeff (f) (\deg (f) - 0), 0)$
38		eqid	$⊢ (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0)) = (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0))$
39		fvex	$⊢ coeff (f) (\deg (f) - 0) \in V$
40		c0ex	$⊢ 0 \in V$
41	39 40	ifex	$⊢ if (0 \leq \deg (f), coeff (f) (\deg (f) - 0), 0) \in V$
42	37 38 41	fvmpt	$⊢ 0 \in ℕ_{0} \to (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0)) (0) = if (0 \leq \deg (f), coeff (f) (\deg (f) - 0), 0)$
43	33 42	ax-mp	$⊢ (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0)) (0) = if (0 \leq \deg (f), coeff (f) (\deg (f) - 0), 0)$
44	15	nn0ge0d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to 0 \leq \deg (f)$
45	44	iftrued	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to if (0 \leq \deg (f), coeff (f) (\deg (f) - 0), 0) = coeff (f) (\deg (f) - 0)$
46	15	nn0cnd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \deg (f) \in ℂ$
47	46	subid1d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \deg (f) - 0 = \deg (f)$
48	47	fveq2d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to coeff (f) (\deg (f) - 0) = coeff (f) (\deg (f))$
49	45 48	eqtrd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to if (0 \leq \deg (f), coeff (f) (\deg (f) - 0), 0) = coeff (f) (\deg (f))$
50	43 49	eqtrid	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (k \in ℕ_{0} ⟼ if (k \leq \deg (f), coeff (f) (\deg (f) - k), 0)) (0) = coeff (f) (\deg (f))$
51	28 32 50	3eqtrd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (0) = coeff (f) (\deg (f))$
52	12	simprd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to f \neq 0_{𝑝}$
53		eqid	$⊢ \deg (f) = \deg (f)$
54	53 18	dgreq0	$⊢ f \in Poly (ℤ) \to (f = 0_{𝑝} \leftrightarrow coeff (f) (\deg (f)) = 0)$
55	13 54	syl	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (f = 0_{𝑝} \leftrightarrow coeff (f) (\deg (f)) = 0)$
56	55	necon3bid	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (f \neq 0_{𝑝} \leftrightarrow coeff (f) (\deg (f)) \neq 0)$
57	52 56	mpbid	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to coeff (f) (\deg (f)) \neq 0$
58	51 57	eqnetrd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (0) \neq 0$
59		ne0p	$⊢ (0 \in ℂ \land (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (0) \neq 0) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \neq 0_{𝑝}$
60	25 58 59	sylancr	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \neq 0_{𝑝}$
61		eldifsn	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \leftrightarrow ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \in Poly (ℤ) \land (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \neq 0_{𝑝})$
62	24 60 61	sylanbrc	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
63		oveq1	$⊢ z = \frac{1}{A} \to z^{k} = {(\frac{1}{A})}^{k}$
64	63	oveq2d	$⊢ z = \frac{1}{A} \to coeff (f) (\deg (f) - k) z^{k} = coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
65	64	sumeq2sdv	$⊢ z = \frac{1}{A} \to \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k} = \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
66		eqid	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k})$
67		sumex	$⊢ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k} \in V$
68	65 66 67	fvmpt	$⊢ \frac{1}{A} \in ℂ \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (\frac{1}{A}) = \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
69	7 68	syl	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (\frac{1}{A}) = \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
70	18	coef3	$⊢ f \in Poly (ℤ) \to coeff (f) : ℕ_{0} ⟶ ℂ$
71	13 70	syl	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to coeff (f) : ℕ_{0} ⟶ ℂ$
72		elfznn0	$⊢ n \in (0 \dots \deg (f)) \to n \in ℕ_{0}$
73		ffvelrn	$⊢ (coeff (f) : ℕ_{0} ⟶ ℂ \land n \in ℕ_{0}) \to coeff (f) (n) \in ℂ$
74	71 72 73	syl2an	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land n \in (0 \dots \deg (f))) \to coeff (f) (n) \in ℂ$
75	4	ad2antrr	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to A \in ℂ$
76		expcl	$⊢ (A \in ℂ \land n \in ℕ_{0}) \to A^{n} \in ℂ$
77	75 72 76	syl2an	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land n \in (0 \dots \deg (f))) \to A^{n} \in ℂ$
78	74 77	mulcld	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land n \in (0 \dots \deg (f))) \to coeff (f) (n) A^{n} \in ℂ$
79	75 15	expcld	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to A^{\deg (f)} \in ℂ$
80	79	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land n \in (0 \dots \deg (f))) \to A^{\deg (f)} \in ℂ$
81		simplr	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to A \neq 0$
82	15	nn0zd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \deg (f) \in ℤ$
83	75 81 82	expne0d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to A^{\deg (f)} \neq 0$
84	83	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land n \in (0 \dots \deg (f))) \to A^{\deg (f)} \neq 0$
85	78 80 84	divcld	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land n \in (0 \dots \deg (f))) \to \frac{coeff (f) (n) A^{n}}{A^{\deg (f)}} \in ℂ$
86		fveq2	$⊢ n = 0 + \deg (f) - k \to coeff (f) (n) = coeff (f) (0 + \deg (f) - k)$
87		oveq2	$⊢ n = 0 + \deg (f) - k \to A^{n} = A^{0 + \deg (f) - k}$
88	86 87	oveq12d	$⊢ n = 0 + \deg (f) - k \to coeff (f) (n) A^{n} = coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k}$
89	88	oveq1d	$⊢ n = 0 + \deg (f) - k \to \frac{coeff (f) (n) A^{n}}{A^{\deg (f)}} = \frac{coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k}}{A^{\deg (f)}}$
90	85 89	fsumrev2	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \sum_{n = 0}^{\deg (f)} (\frac{coeff (f) (n) A^{n}}{A^{\deg (f)}}) = \sum_{k = 0}^{\deg (f)} (\frac{coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k}}{A^{\deg (f)}})$
91	46	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \deg (f) \in ℂ$
92	91	addid2d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to 0 + \deg (f) = \deg (f)$
93	92	oveq1d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to 0 + \deg (f) - k = \deg (f) - k$
94	93	fveq2d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to coeff (f) (0 + \deg (f) - k) = coeff (f) (\deg (f) - k)$
95	93	oveq2d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{0 + \deg (f) - k} = A^{\deg (f) - k}$
96	75	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A \in ℂ$
97	81	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A \neq 0$
98		elfznn0	$⊢ k \in (0 \dots \deg (f)) \to k \in ℕ_{0}$
99	98	adantl	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to k \in ℕ_{0}$
100	99	nn0zd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to k \in ℤ$
101	82	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \deg (f) \in ℤ$
102	96 97 100 101	expsubd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{\deg (f) - k} = \frac{A^{\deg (f)}}{A^{k}}$
103	95 102	eqtrd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{0 + \deg (f) - k} = \frac{A^{\deg (f)}}{A^{k}}$
104	94 103	oveq12d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k} = coeff (f) (\deg (f) - k) (\frac{A^{\deg (f)}}{A^{k}})$
105	104	oveq1d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k}}{A^{\deg (f)}} = \frac{coeff (f) (\deg (f) - k) (\frac{A^{\deg (f)}}{A^{k}})}{A^{\deg (f)}}$
106	79	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{\deg (f)} \in ℂ$
107		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
108	75 98 107	syl2an	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{k} \in ℂ$
109	96 97 100	expne0d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{k} \neq 0$
110	106 108 109	divcld	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{A^{\deg (f)}}{A^{k}} \in ℂ$
111	83	adantr	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to A^{\deg (f)} \neq 0$
112	29 110 106 111	divassd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{coeff (f) (\deg (f) - k) (\frac{A^{\deg (f)}}{A^{k}})}{A^{\deg (f)}} = coeff (f) (\deg (f) - k) (\frac{\frac{A^{\deg (f)}}{A^{k}}}{A^{\deg (f)}})$
113	106 111	dividd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{A^{\deg (f)}}{A^{\deg (f)}} = 1$
114	113	oveq1d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{\frac{A^{\deg (f)}}{A^{\deg (f)}}}{A^{k}} = \frac{1}{A^{k}}$
115	106 108 106 109 111	divdiv32d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{\frac{A^{\deg (f)}}{A^{k}}}{A^{\deg (f)}} = \frac{\frac{A^{\deg (f)}}{A^{\deg (f)}}}{A^{k}}$
116	96 97 100	exprecd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to {(\frac{1}{A})}^{k} = \frac{1}{A^{k}}$
117	114 115 116	3eqtr4d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{\frac{A^{\deg (f)}}{A^{k}}}{A^{\deg (f)}} = {(\frac{1}{A})}^{k}$
118	117	oveq2d	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to coeff (f) (\deg (f) - k) (\frac{\frac{A^{\deg (f)}}{A^{k}}}{A^{\deg (f)}}) = coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
119	105 112 118	3eqtrd	$⊢ (((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \land k \in (0 \dots \deg (f))) \to \frac{coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k}}{A^{\deg (f)}} = coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
120	119	sumeq2dv	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \sum_{k = 0}^{\deg (f)} (\frac{coeff (f) (0 + \deg (f) - k) A^{0 + \deg (f) - k}}{A^{\deg (f)}}) = \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
121	90 120	eqtrd	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \sum_{n = 0}^{\deg (f)} (\frac{coeff (f) (n) A^{n}}{A^{\deg (f)}}) = \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) {(\frac{1}{A})}^{k}$
122	18 53	coeid2	$⊢ (f \in Poly (ℤ) \land A \in ℂ) \to f (A) = \sum_{n = 0}^{\deg (f)} coeff (f) (n) A^{n}$
123	13 75 122	syl2anc	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to f (A) = \sum_{n = 0}^{\deg (f)} coeff (f) (n) A^{n}$
124		simprr	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to f (A) = 0$
125	123 124	eqtr3d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \sum_{n = 0}^{\deg (f)} coeff (f) (n) A^{n} = 0$
126	125	oveq1d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \frac{\sum_{n = 0}^{\deg (f)} coeff (f) (n) A^{n}}{A^{\deg (f)}} = \frac{0}{A^{\deg (f)}}$
127		fzfid	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (0 \dots \deg (f)) \in Fin$
128	127 79 78 83	fsumdivc	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \frac{\sum_{n = 0}^{\deg (f)} coeff (f) (n) A^{n}}{A^{\deg (f)}} = \sum_{n = 0}^{\deg (f)} (\frac{coeff (f) (n) A^{n}}{A^{\deg (f)}})$
129	79 83	div0d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \frac{0}{A^{\deg (f)}} = 0$
130	126 128 129	3eqtr3d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \sum_{n = 0}^{\deg (f)} (\frac{coeff (f) (n) A^{n}}{A^{\deg (f)}}) = 0$
131	69 121 130	3eqtr2d	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (\frac{1}{A}) = 0$
132		fveq1	$⊢ g = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \to g (\frac{1}{A}) = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (\frac{1}{A})$
133	132	eqeq1d	$⊢ g = (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \to (g (\frac{1}{A}) = 0 \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (\frac{1}{A}) = 0)$
134	133	rspcev	$⊢ ((z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land (z \in ℂ ⟼ \sum_{k = 0}^{\deg (f)} coeff (f) (\deg (f) - k) z^{k}) (\frac{1}{A}) = 0) \to \exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (\frac{1}{A}) = 0$
135	62 131 134	syl2anc	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (\frac{1}{A}) = 0$
136		elaa	$⊢ \frac{1}{A} \in 𝔸 \leftrightarrow (\frac{1}{A} \in ℂ \land \exists g \in (Poly (ℤ) ∖ \{0_{𝑝}\}) g (\frac{1}{A}) = 0)$
137	7 135 136	sylanbrc	$⊢ ((A \in 𝔸 \land A \neq 0) \land (f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land f (A) = 0)) \to \frac{1}{A} \in 𝔸$
138	3 137	rexlimddv	$⊢ (A \in 𝔸 \land A \neq 0) \to \frac{1}{A} \in 𝔸$

Metamath Proof Explorer

Theorem aareccl

Proof