Metamath Proof Explorer

Theorem aannenlem2

Description: Lemma for aannen . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypothesis aannenlem.a ⊢H=a∈ℕ0⟼b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
Assertion aannenlem2 ⊢𝔸=⋃ran⁡H

Proof

Step Hyp Ref Expression
1 aannenlem.a ⊢H=a∈ℕ0⟼b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
2 fveqeq2 ⊢b=g→c⁡b=0↔c⁡g=0
3 2 rexbidv ⊢b=g→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0↔∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡g=0
4 simp3 ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→g∈ℂ
5 neeq1 ⊢d=h→d≠0𝑝↔h≠0𝑝
6 fveq2 ⊢d=h→deg⁡d=deg⁡h
7 6 breq1d ⊢d=h→deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<↔deg⁡h≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
8 fveq2 ⊢d=h→coeff⁡d=coeff⁡h
9 8 fveq1d ⊢d=h→coeff⁡d⁡e=coeff⁡h⁡e
10 9 fveq2d ⊢d=h→coeff⁡d⁡e=coeff⁡h⁡e
11 10 breq1d ⊢d=h→coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<↔coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
12 11 ralbidv ⊢d=h→∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<↔∀e∈ℕ0coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
13 5 7 12 3anbi123d ⊢d=h→d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<↔h≠0𝑝∧deg⁡h≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
14 eldifi ⊢h∈Poly⁡ℤ∖0𝑝→h∈Poly⁡ℤ
15 14 adantr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→h∈Poly⁡ℤ
16 15 3adant2 ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→h∈Poly⁡ℤ
17 eldifsni ⊢h∈Poly⁡ℤ∖0𝑝→h≠0𝑝
18 17 adantr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→h≠0𝑝
19 0nn0 ⊢0∈ℕ0
20 dgrcl ⊢h∈Poly⁡ℤ→deg⁡h∈ℕ0
21 15 20 syl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→deg⁡h∈ℕ0
22 prssi ⊢0∈ℕ0∧deg⁡h∈ℕ0→0deg⁡h⊆ℕ0
23 19 21 22 sylancr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→0deg⁡h⊆ℕ0
24 ssrab2 ⊢g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℕ0
25 24 a1i ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℕ0
26 23 25 unssd ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℕ0
27 nn0ssre ⊢ℕ0⊆ℝ
28 ressxr ⊢ℝ⊆ℝ*
29 27 28 sstri ⊢ℕ0⊆ℝ*
30 26 29 sstrdi ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℝ*
31 fvex ⊢deg⁡h∈V
32 31 prid2 ⊢deg⁡h∈0deg⁡h
33 elun1 ⊢deg⁡h∈0deg⁡h→deg⁡h∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
34 32 33 ax-mp ⊢deg⁡h∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
35 supxrub ⊢0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℝ*∧deg⁡h∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i→deg⁡h≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
36 30 34 35 sylancl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→deg⁡h≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
37 30 adantr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0→0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℝ*
38 fveq2 ⊢coeff⁡h⁡e=0→coeff⁡h⁡e=0
39 abs0 ⊢0=0
40 38 39 eqtrdi ⊢coeff⁡h⁡e=0→coeff⁡h⁡e=0
41 c0ex ⊢0∈V
42 41 prid1 ⊢0∈0deg⁡h
43 elun1 ⊢0∈0deg⁡h→0∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
44 42 43 ax-mp ⊢0∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
45 40 44 eqeltrdi ⊢coeff⁡h⁡e=0→coeff⁡h⁡e∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
46 45 adantl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e=0→coeff⁡h⁡e∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
47 eqeq1 ⊢g=coeff⁡h⁡e→g=coeff⁡h⁡i↔coeff⁡h⁡e=coeff⁡h⁡i
48 47 rexbidv ⊢g=coeff⁡h⁡e→∃i∈0…deg⁡hg=coeff⁡h⁡i↔∃i∈0…deg⁡hcoeff⁡h⁡e=coeff⁡h⁡i
49 0z ⊢0∈ℤ
50 eqid ⊢coeff⁡h=coeff⁡h
51 50 coef2 ⊢h∈Poly⁡ℤ∧0∈ℤ→coeff⁡h:ℕ0⟶ℤ
52 15 49 51 sylancl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→coeff⁡h:ℕ0⟶ℤ
53 52 ffvelcdmda ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0→coeff⁡h⁡e∈ℤ
54 nn0abscl ⊢coeff⁡h⁡e∈ℤ→coeff⁡h⁡e∈ℕ0
55 53 54 syl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0→coeff⁡h⁡e∈ℕ0
56 55 adantr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→coeff⁡h⁡e∈ℕ0
57 simplr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→e∈ℕ0
58 21 ad2antrr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→deg⁡h∈ℕ0
59 15 ad2antrr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→h∈Poly⁡ℤ
60 simpr ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→coeff⁡h⁡e≠0
61 eqid ⊢deg⁡h=deg⁡h
62 50 61 dgrub ⊢h∈Poly⁡ℤ∧e∈ℕ0∧coeff⁡h⁡e≠0→e≤deg⁡h
63 59 57 60 62 syl3anc ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→e≤deg⁡h
64 elfz2nn0 ⊢e∈0…deg⁡h↔e∈ℕ0∧deg⁡h∈ℕ0∧e≤deg⁡h
65 57 58 63 64 syl3anbrc ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→e∈0…deg⁡h
66 eqid ⊢coeff⁡h⁡e=coeff⁡h⁡e
67 2fveq3 ⊢i=e→coeff⁡h⁡i=coeff⁡h⁡e
68 67 rspceeqv ⊢e∈0…deg⁡h∧coeff⁡h⁡e=coeff⁡h⁡e→∃i∈0…deg⁡hcoeff⁡h⁡e=coeff⁡h⁡i
69 65 66 68 sylancl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→∃i∈0…deg⁡hcoeff⁡h⁡e=coeff⁡h⁡i
70 48 56 69 elrabd ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→coeff⁡h⁡e∈g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
71 elun2 ⊢coeff⁡h⁡e∈g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i→coeff⁡h⁡e∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
72 70 71 syl ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0∧coeff⁡h⁡e≠0→coeff⁡h⁡e∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
73 46 72 pm2.61dane ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0→coeff⁡h⁡e∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
74 supxrub ⊢0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℝ*∧coeff⁡h⁡e∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i→coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
75 37 73 74 syl2anc ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ∧e∈ℕ0→coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
76 75 ralrimiva ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→∀e∈ℕ0coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
77 18 36 76 3jca ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→h≠0𝑝∧deg⁡h≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
78 77 3adant2 ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→h≠0𝑝∧deg⁡h≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡h⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
79 13 16 78 elrabd ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→h∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
80 simp2 ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→h⁡g=0
81 fveq1 ⊢c=h→c⁡g=h⁡g
82 81 eqeq1d ⊢c=h→c⁡g=0↔h⁡g=0
83 82 rspcev ⊢h∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧h⁡g=0→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡g=0
84 79 80 83 syl2anc ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡g=0
85 3 4 84 elrabd ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0
86 prfi ⊢0deg⁡h∈Fin
87 fzfi ⊢0…deg⁡h∈Fin
88 abrexfi ⊢0…deg⁡h∈Fin→g|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin
89 87 88 ax-mp ⊢g|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin
90 rabssab ⊢g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆g|∃i∈0…deg⁡hg=coeff⁡h⁡i
91 ssfi ⊢g|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin∧g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆g|∃i∈0…deg⁡hg=coeff⁡h⁡i→g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin
92 89 90 91 mp2an ⊢g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin
93 unfi ⊢0deg⁡h∈Fin∧g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin→0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin
94 86 92 93 mp2an ⊢0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin
95 34 ne0ii ⊢0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i≠∅
96 xrltso ⊢<Orℝ*
97 fisupcl ⊢<Orℝ*∧0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin∧0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i≠∅∧0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℝ*→sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
98 96 97 mpan ⊢0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i∈Fin∧0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i≠∅∧0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i⊆ℝ*→sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
99 94 95 30 98 mp3an12i ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∈0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡i
100 26 99 sseldd ⊢h∈Poly⁡ℤ∖0𝑝∧g∈ℂ→sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∈ℕ0
101 100 3adant2 ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∈ℕ0
102 eqidd ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0
103 breq2 ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→deg⁡d≤a↔deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
104 breq2 ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→coeff⁡d⁡e≤a↔coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
105 104 ralbidv ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→∀e∈ℕ0coeff⁡d⁡e≤a↔∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
106 103 105 3anbi23d ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a↔d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
107 106 rabbidv ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a=d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<
108 107 rexeqdv ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0
109 108 rabbidv ⊢a=sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<→b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0
110 109 rspceeqv ⊢sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∈ℕ0∧b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0→∃a∈ℕ0b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
111 101 102 110 syl2anc ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→∃a∈ℕ0b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
112 cnex ⊢ℂ∈V
113 112 rabex ⊢b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0∈V
114 eleq2 ⊢f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0→g∈f↔g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0
115 eqeq1 ⊢f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0→f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
116 115 rexbidv ⊢f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0→∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔∃a∈ℕ0b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
117 114 116 anbi12d ⊢f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0→g∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0∧∃a∈ℕ0b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
118 113 117 spcev ⊢g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0∧∃a∈ℕ0b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<∧∀e∈ℕ0coeff⁡d⁡e≤sup0deg⁡h∪g∈ℕ0|∃i∈0…deg⁡hg=coeff⁡h⁡iℝ*<c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
119 85 111 118 syl2anc ⊢h∈Poly⁡ℤ∖0𝑝∧h⁡g=0∧g∈ℂ→∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
120 119 3exp ⊢h∈Poly⁡ℤ∖0𝑝→h⁡g=0→g∈ℂ→∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
121 120 rexlimiv ⊢∃h∈Poly⁡ℤ∖0𝑝h⁡g=0→g∈ℂ→∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
122 121 impcom ⊢g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0→∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
123 eleq2 ⊢f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→g∈f↔g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
124 2 rexbidv ⊢b=g→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡g=0
125 124 elrab ⊢g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔g∈ℂ∧∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡g=0
126 simp1 ⊢h≠0𝑝∧deg⁡h≤a∧∀e∈ℕ0coeff⁡h⁡e≤a→h≠0𝑝
127 126 anim2i ⊢h∈Poly⁡ℤ∧h≠0𝑝∧deg⁡h≤a∧∀e∈ℕ0coeff⁡h⁡e≤a→h∈Poly⁡ℤ∧h≠0𝑝
128 6 breq1d ⊢d=h→deg⁡d≤a↔deg⁡h≤a
129 10 breq1d ⊢d=h→coeff⁡d⁡e≤a↔coeff⁡h⁡e≤a
130 129 ralbidv ⊢d=h→∀e∈ℕ0coeff⁡d⁡e≤a↔∀e∈ℕ0coeff⁡h⁡e≤a
131 5 128 130 3anbi123d ⊢d=h→d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a↔h≠0𝑝∧deg⁡h≤a∧∀e∈ℕ0coeff⁡h⁡e≤a
132 131 elrab ⊢h∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a↔h∈Poly⁡ℤ∧h≠0𝑝∧deg⁡h≤a∧∀e∈ℕ0coeff⁡h⁡e≤a
133 eldifsn ⊢h∈Poly⁡ℤ∖0𝑝↔h∈Poly⁡ℤ∧h≠0𝑝
134 127 132 133 3imtr4i ⊢h∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a→h∈Poly⁡ℤ∖0𝑝
135 134 ssriv ⊢d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a⊆Poly⁡ℤ∖0𝑝
136 ssrexv ⊢d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a⊆Poly⁡ℤ∖0𝑝→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡g=0→∃c∈Poly⁡ℤ∖0𝑝c⁡g=0
137 82 cbvrexvw ⊢∃c∈Poly⁡ℤ∖0𝑝c⁡g=0↔∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
138 136 137 imbitrdi ⊢d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a⊆Poly⁡ℤ∖0𝑝→∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡g=0→∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
139 135 138 ax-mp ⊢∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡g=0→∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
140 139 anim2i ⊢g∈ℂ∧∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡g=0→g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
141 125 140 sylbi ⊢g∈b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
142 123 141 syl6bi ⊢f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→g∈f→g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
143 142 rexlimivw ⊢∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→g∈f→g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
144 143 impcom ⊢g∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
145 144 exlimiv ⊢∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0→g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
146 122 145 impbii ⊢g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0↔∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
147 elaa ⊢g∈𝔸↔g∈ℂ∧∃h∈Poly⁡ℤ∖0𝑝h⁡g=0
148 eluniab ⊢g∈⋃f|∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0↔∃fg∈f∧∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
149 146 147 148 3bitr4i ⊢g∈𝔸↔g∈⋃f|∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
150 149 eqriv ⊢𝔸=⋃f|∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
151 1 rnmpt ⊢ran⁡H=f|∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
152 151 unieqi ⊢⋃ran⁡H=⋃f|∃a∈ℕ0f=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0
153 150 152 eqtr4i ⊢𝔸=⋃ran⁡H