# Metamath Proof Explorer

## Theorem elqaalem3

Description: Lemma for elqaa . (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses elqaa.1 ${⊢}{\phi }\to {A}\in ℂ$
elqaa.2 ${⊢}{\phi }\to {F}\in \left(\mathrm{Poly}\left(ℚ\right)\setminus \left\{{0}_{𝑝}\right\}\right)$
elqaa.3 ${⊢}{\phi }\to {F}\left({A}\right)=0$
elqaa.4 ${⊢}{B}=\mathrm{coeff}\left({F}\right)$
elqaa.5 ${⊢}{N}=\left({k}\in {ℕ}_{0}⟼sup\left(\left\{{n}\in ℕ|{B}\left({k}\right){n}\in ℤ\right\},ℝ,<\right)\right)$
elqaa.6 ${⊢}{R}=seq0\left(×,{N}\right)\left(\mathrm{deg}\left({F}\right)\right)$
Assertion elqaalem3 ${⊢}{\phi }\to {A}\in 𝔸$

### Proof

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