Metamath Proof Explorer

Theorem aareccl

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

Ref Expression
Assertion aareccl ⊢A∈𝔸∧A≠0→1A∈𝔸

Proof

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