Metamath Proof Explorer

Theorem aannenlem1

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 aannenlem1 ⊢A∈ℕ0→H⁡A∈Fin

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 breq2 ⊢a=A→deg⁡d≤a↔deg⁡d≤A
3 breq2 ⊢a=A→coeff⁡d⁡e≤a↔coeff⁡d⁡e≤A
4 3 ralbidv ⊢a=A→∀e∈ℕ0coeff⁡d⁡e≤a↔∀e∈ℕ0coeff⁡d⁡e≤A
5 2 4 3anbi23d ⊢a=A→d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a↔d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A
6 5 rabbidv ⊢a=A→d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤a=d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A
7 6 rexeqdv ⊢a=A→∃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⁡b=0
8 7 rabbidv ⊢a=A→b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤a∧∀e∈ℕ0coeff⁡d⁡e≤ac⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ac⁡b=0
9 cnex ⊢ℂ∈V
10 9 rabex ⊢b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ac⁡b=0∈V
11 8 1 10 fvmpt ⊢A∈ℕ0→H⁡A=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ac⁡b=0
12 iunrab ⊢⋃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ab∈ℂ|c⁡b=0=b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ac⁡b=0
13 fzfi ⊢−A…A∈Fin
14 fzfi ⊢0…A∈Fin
15 mapfi ⊢−A…A∈Fin∧0…A∈Fin→−A…A0…A∈Fin
16 13 14 15 mp2an ⊢−A…A0…A∈Fin
17 16 a1i ⊢A∈ℕ0→−A…A0…A∈Fin
18 ovex ⊢−A…A0…A∈V
19 neeq1 ⊢d=a→d≠0𝑝↔a≠0𝑝
20 fveq2 ⊢d=a→deg⁡d=deg⁡a
21 20 breq1d ⊢d=a→deg⁡d≤A↔deg⁡a≤A
22 fveq2 ⊢d=a→coeff⁡d=coeff⁡a
23 22 fveq1d ⊢d=a→coeff⁡d⁡e=coeff⁡a⁡e
24 23 fveq2d ⊢d=a→coeff⁡d⁡e=coeff⁡a⁡e
25 24 breq1d ⊢d=a→coeff⁡d⁡e≤A↔coeff⁡a⁡e≤A
26 25 ralbidv ⊢d=a→∀e∈ℕ0coeff⁡d⁡e≤A↔∀e∈ℕ0coeff⁡a⁡e≤A
27 19 21 26 3anbi123d ⊢d=a→d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A↔a≠0𝑝∧deg⁡a≤A∧∀e∈ℕ0coeff⁡a⁡e≤A
28 27 elrab ⊢a∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A↔a∈Poly⁡ℤ∧a≠0𝑝∧deg⁡a≤A∧∀e∈ℕ0coeff⁡a⁡e≤A
29 simp3 ⊢a≠0𝑝∧deg⁡a≤A∧∀e∈ℕ0coeff⁡a⁡e≤A→∀e∈ℕ0coeff⁡a⁡e≤A
30 29 anim2i ⊢a∈Poly⁡ℤ∧a≠0𝑝∧deg⁡a≤A∧∀e∈ℕ0coeff⁡a⁡e≤A→a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A
31 28 30 sylbi ⊢a∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A
32 0z ⊢0∈ℤ
33 eqid ⊢coeff⁡a=coeff⁡a
34 33 coef2 ⊢a∈Poly⁡ℤ∧0∈ℤ→coeff⁡a:ℕ0⟶ℤ
35 32 34 mpan2 ⊢a∈Poly⁡ℤ→coeff⁡a:ℕ0⟶ℤ
36 35 ad2antrl ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→coeff⁡a:ℕ0⟶ℤ
37 36 ffnd ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→coeff⁡aFnℕ0
38 35 adantl ⊢A∈ℕ0∧a∈Poly⁡ℤ→coeff⁡a:ℕ0⟶ℤ
39 38 ffvelcdmda ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→coeff⁡a⁡e∈ℤ
40 39 zred ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→coeff⁡a⁡e∈ℝ
41 nn0re ⊢A∈ℕ0→A∈ℝ
42 41 ad2antrr ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→A∈ℝ
43 40 42 absled ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→coeff⁡a⁡e≤A↔−A≤coeff⁡a⁡e∧coeff⁡a⁡e≤A
44 nn0z ⊢A∈ℕ0→A∈ℤ
45 44 ad2antrr ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→A∈ℤ
46 45 znegcld ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→−A∈ℤ
47 elfz ⊢coeff⁡a⁡e∈ℤ∧−A∈ℤ∧A∈ℤ→coeff⁡a⁡e∈−A…A↔−A≤coeff⁡a⁡e∧coeff⁡a⁡e≤A
48 39 46 45 47 syl3anc ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→coeff⁡a⁡e∈−A…A↔−A≤coeff⁡a⁡e∧coeff⁡a⁡e≤A
49 43 48 bitr4d ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→coeff⁡a⁡e≤A↔coeff⁡a⁡e∈−A…A
50 49 biimpd ⊢A∈ℕ0∧a∈Poly⁡ℤ∧e∈ℕ0→coeff⁡a⁡e≤A→coeff⁡a⁡e∈−A…A
51 50 ralimdva ⊢A∈ℕ0∧a∈Poly⁡ℤ→∀e∈ℕ0coeff⁡a⁡e≤A→∀e∈ℕ0coeff⁡a⁡e∈−A…A
52 51 impr ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→∀e∈ℕ0coeff⁡a⁡e∈−A…A
53 fnfvrnss ⊢coeff⁡aFnℕ0∧∀e∈ℕ0coeff⁡a⁡e∈−A…A→ran⁡coeff⁡a⊆−A…A
54 37 52 53 syl2anc ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→ran⁡coeff⁡a⊆−A…A
55 df-f ⊢coeff⁡a:ℕ0⟶−A…A↔coeff⁡aFnℕ0∧ran⁡coeff⁡a⊆−A…A
56 37 54 55 sylanbrc ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→coeff⁡a:ℕ0⟶−A…A
57 fz0ssnn0 ⊢0…A⊆ℕ0
58 fssres ⊢coeff⁡a:ℕ0⟶−A…A∧0…A⊆ℕ0→coeff⁡a↾0…A:0…A⟶−A…A
59 56 57 58 sylancl ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→coeff⁡a↾0…A:0…A⟶−A…A
60 ovex ⊢−A…A∈V
61 ovex ⊢0…A∈V
62 60 61 elmap ⊢coeff⁡a↾0…A∈−A…A0…A↔coeff⁡a↾0…A:0…A⟶−A…A
63 59 62 sylibr ⊢A∈ℕ0∧a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→coeff⁡a↾0…A∈−A…A0…A
64 63 ex ⊢A∈ℕ0→a∈Poly⁡ℤ∧∀e∈ℕ0coeff⁡a⁡e≤A→coeff⁡a↾0…A∈−A…A0…A
65 31 64 syl5 ⊢A∈ℕ0→a∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→coeff⁡a↾0…A∈−A…A0…A
66 simp2 ⊢a≠0𝑝∧deg⁡a≤A∧∀e∈ℕ0coeff⁡a⁡e≤A→deg⁡a≤A
67 66 anim2i ⊢a∈Poly⁡ℤ∧a≠0𝑝∧deg⁡a≤A∧∀e∈ℕ0coeff⁡a⁡e≤A→a∈Poly⁡ℤ∧deg⁡a≤A
68 28 67 sylbi ⊢a∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→a∈Poly⁡ℤ∧deg⁡a≤A
69 neeq1 ⊢d=b→d≠0𝑝↔b≠0𝑝
70 fveq2 ⊢d=b→deg⁡d=deg⁡b
71 70 breq1d ⊢d=b→deg⁡d≤A↔deg⁡b≤A
72 fveq2 ⊢d=b→coeff⁡d=coeff⁡b
73 72 fveq1d ⊢d=b→coeff⁡d⁡e=coeff⁡b⁡e
74 73 fveq2d ⊢d=b→coeff⁡d⁡e=coeff⁡b⁡e
75 74 breq1d ⊢d=b→coeff⁡d⁡e≤A↔coeff⁡b⁡e≤A
76 75 ralbidv ⊢d=b→∀e∈ℕ0coeff⁡d⁡e≤A↔∀e∈ℕ0coeff⁡b⁡e≤A
77 69 71 76 3anbi123d ⊢d=b→d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A↔b≠0𝑝∧deg⁡b≤A∧∀e∈ℕ0coeff⁡b⁡e≤A
78 77 elrab ⊢b∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A↔b∈Poly⁡ℤ∧b≠0𝑝∧deg⁡b≤A∧∀e∈ℕ0coeff⁡b⁡e≤A
79 simp2 ⊢b≠0𝑝∧deg⁡b≤A∧∀e∈ℕ0coeff⁡b⁡e≤A→deg⁡b≤A
80 79 anim2i ⊢b∈Poly⁡ℤ∧b≠0𝑝∧deg⁡b≤A∧∀e∈ℕ0coeff⁡b⁡e≤A→b∈Poly⁡ℤ∧deg⁡b≤A
81 78 80 sylbi ⊢b∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→b∈Poly⁡ℤ∧deg⁡b≤A
82 simplll ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A→a∈Poly⁡ℤ
83 plyf ⊢a∈Poly⁡ℤ→a:ℂ⟶ℂ
84 ffn ⊢a:ℂ⟶ℂ→aFnℂ
85 82 83 84 3syl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A→aFnℂ
86 simplrl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A→b∈Poly⁡ℤ
87 plyf ⊢b∈Poly⁡ℤ→b:ℂ⟶ℂ
88 ffn ⊢b:ℂ⟶ℂ→bFnℂ
89 86 87 88 3syl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A→bFnℂ
90 simplrr ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→coeff⁡a↾0…A=coeff⁡b↾0…A
91 90 adantr ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ∧d∈0…A→coeff⁡a↾0…A=coeff⁡b↾0…A
92 91 fveq1d ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ∧d∈0…A→coeff⁡a↾0…A⁡d=coeff⁡b↾0…A⁡d
93 fvres ⊢d∈0…A→coeff⁡a↾0…A⁡d=coeff⁡a⁡d
94 93 adantl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ∧d∈0…A→coeff⁡a↾0…A⁡d=coeff⁡a⁡d
95 fvres ⊢d∈0…A→coeff⁡b↾0…A⁡d=coeff⁡b⁡d
96 95 adantl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ∧d∈0…A→coeff⁡b↾0…A⁡d=coeff⁡b⁡d
97 92 94 96 3eqtr3d ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ∧d∈0…A→coeff⁡a⁡d=coeff⁡b⁡d
98 97 oveq1d ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ∧d∈0…A→coeff⁡a⁡d⁢cd=coeff⁡b⁡d⁢cd
99 98 sumeq2dv ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→∑d=0Acoeff⁡a⁡d⁢cd=∑d=0Acoeff⁡b⁡d⁢cd
100 simp-4l ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→a∈Poly⁡ℤ
101 simp-4r ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→deg⁡a≤A
102 dgrcl ⊢a∈Poly⁡ℤ→deg⁡a∈ℕ0
103 nn0z ⊢deg⁡a∈ℕ0→deg⁡a∈ℤ
104 100 102 103 3syl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→deg⁡a∈ℤ
105 simplrl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→A∈ℕ0
106 105 nn0zd ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→A∈ℤ
107 eluz ⊢deg⁡a∈ℤ∧A∈ℤ→A∈ℤ≥deg⁡a↔deg⁡a≤A
108 104 106 107 syl2anc ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→A∈ℤ≥deg⁡a↔deg⁡a≤A
109 101 108 mpbird ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→A∈ℤ≥deg⁡a
110 simpr ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→c∈ℂ
111 eqid ⊢deg⁡a=deg⁡a
112 33 111 coeid3 ⊢a∈Poly⁡ℤ∧A∈ℤ≥deg⁡a∧c∈ℂ→a⁡c=∑d=0Acoeff⁡a⁡d⁢cd
113 100 109 110 112 syl3anc ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→a⁡c=∑d=0Acoeff⁡a⁡d⁢cd
114 simp1rl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→b∈Poly⁡ℤ
115 114 3expa ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→b∈Poly⁡ℤ
116 simplrr ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A→deg⁡b≤A
117 116 adantr ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→deg⁡b≤A
118 dgrcl ⊢b∈Poly⁡ℤ→deg⁡b∈ℕ0
119 nn0z ⊢deg⁡b∈ℕ0→deg⁡b∈ℤ
120 115 118 119 3syl ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→deg⁡b∈ℤ
121 eluz ⊢deg⁡b∈ℤ∧A∈ℤ→A∈ℤ≥deg⁡b↔deg⁡b≤A
122 120 106 121 syl2anc ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→A∈ℤ≥deg⁡b↔deg⁡b≤A
123 117 122 mpbird ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→A∈ℤ≥deg⁡b
124 eqid ⊢coeff⁡b=coeff⁡b
125 eqid ⊢deg⁡b=deg⁡b
126 124 125 coeid3 ⊢b∈Poly⁡ℤ∧A∈ℤ≥deg⁡b∧c∈ℂ→b⁡c=∑d=0Acoeff⁡b⁡d⁢cd
127 115 123 110 126 syl3anc ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→b⁡c=∑d=0Acoeff⁡b⁡d⁢cd
128 99 113 127 3eqtr4d ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A∧c∈ℂ→a⁡c=b⁡c
129 85 89 128 eqfnfvd ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0∧coeff⁡a↾0…A=coeff⁡b↾0…A→a=b
130 129 expr ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0→coeff⁡a↾0…A=coeff⁡b↾0…A→a=b
131 fveq2 ⊢a=b→coeff⁡a=coeff⁡b
132 131 reseq1d ⊢a=b→coeff⁡a↾0…A=coeff⁡b↾0…A
133 130 132 impbid1 ⊢a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A∧A∈ℕ0→coeff⁡a↾0…A=coeff⁡b↾0…A↔a=b
134 133 expcom ⊢A∈ℕ0→a∈Poly⁡ℤ∧deg⁡a≤A∧b∈Poly⁡ℤ∧deg⁡b≤A→coeff⁡a↾0…A=coeff⁡b↾0…A↔a=b
135 68 81 134 syl2ani ⊢A∈ℕ0→a∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A∧b∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→coeff⁡a↾0…A=coeff⁡b↾0…A↔a=b
136 65 135 dom2d ⊢A∈ℕ0→−A…A0…A∈V→d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A≼−A…A0…A
137 18 136 mpi ⊢A∈ℕ0→d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A≼−A…A0…A
138 domfi ⊢−A…A0…A∈Fin∧d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A≼−A…A0…A→d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A∈Fin
139 17 137 138 syl2anc ⊢A∈ℕ0→d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A∈Fin
140 neeq1 ⊢d=c→d≠0𝑝↔c≠0𝑝
141 fveq2 ⊢d=c→deg⁡d=deg⁡c
142 141 breq1d ⊢d=c→deg⁡d≤A↔deg⁡c≤A
143 fveq2 ⊢d=c→coeff⁡d=coeff⁡c
144 143 fveq1d ⊢d=c→coeff⁡d⁡e=coeff⁡c⁡e
145 144 fveq2d ⊢d=c→coeff⁡d⁡e=coeff⁡c⁡e
146 145 breq1d ⊢d=c→coeff⁡d⁡e≤A↔coeff⁡c⁡e≤A
147 146 ralbidv ⊢d=c→∀e∈ℕ0coeff⁡d⁡e≤A↔∀e∈ℕ0coeff⁡c⁡e≤A
148 140 142 147 3anbi123d ⊢d=c→d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A↔c≠0𝑝∧deg⁡c≤A∧∀e∈ℕ0coeff⁡c⁡e≤A
149 148 elrab ⊢c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A↔c∈Poly⁡ℤ∧c≠0𝑝∧deg⁡c≤A∧∀e∈ℕ0coeff⁡c⁡e≤A
150 simp1 ⊢c≠0𝑝∧deg⁡c≤A∧∀e∈ℕ0coeff⁡c⁡e≤A→c≠0𝑝
151 150 anim2i ⊢c∈Poly⁡ℤ∧c≠0𝑝∧deg⁡c≤A∧∀e∈ℕ0coeff⁡c⁡e≤A→c∈Poly⁡ℤ∧c≠0𝑝
152 149 151 sylbi ⊢c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→c∈Poly⁡ℤ∧c≠0𝑝
153 fveqeq2 ⊢b=a→c⁡b=0↔c⁡a=0
154 153 elrab ⊢a∈b∈ℂ|c⁡b=0↔a∈ℂ∧c⁡a=0
155 plyf ⊢c∈Poly⁡ℤ→c:ℂ⟶ℂ
156 155 ffnd ⊢c∈Poly⁡ℤ→cFnℂ
157 156 adantr ⊢c∈Poly⁡ℤ∧c≠0𝑝→cFnℂ
158 fniniseg ⊢cFnℂ→a∈c-10↔a∈ℂ∧c⁡a=0
159 157 158 syl ⊢c∈Poly⁡ℤ∧c≠0𝑝→a∈c-10↔a∈ℂ∧c⁡a=0
160 154 159 bitr4id ⊢c∈Poly⁡ℤ∧c≠0𝑝→a∈b∈ℂ|c⁡b=0↔a∈c-10
161 160 eqrdv ⊢c∈Poly⁡ℤ∧c≠0𝑝→b∈ℂ|c⁡b=0=c-10
162 eqid ⊢c-10=c-10
163 162 fta1 ⊢c∈Poly⁡ℤ∧c≠0𝑝→c-10∈Fin∧c-10≤deg⁡c
164 163 simpld ⊢c∈Poly⁡ℤ∧c≠0𝑝→c-10∈Fin
165 161 164 eqeltrd ⊢c∈Poly⁡ℤ∧c≠0𝑝→b∈ℂ|c⁡b=0∈Fin
166 165 a1i ⊢A∈ℕ0→c∈Poly⁡ℤ∧c≠0𝑝→b∈ℂ|c⁡b=0∈Fin
167 152 166 syl5 ⊢A∈ℕ0→c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A→b∈ℂ|c⁡b=0∈Fin
168 167 ralrimiv ⊢A∈ℕ0→∀c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ab∈ℂ|c⁡b=0∈Fin
169 iunfi ⊢d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤A∈Fin∧∀c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ab∈ℂ|c⁡b=0∈Fin→⋃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ab∈ℂ|c⁡b=0∈Fin
170 139 168 169 syl2anc ⊢A∈ℕ0→⋃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ab∈ℂ|c⁡b=0∈Fin
171 12 170 eqeltrrid ⊢A∈ℕ0→b∈ℂ|∃c∈d∈Poly⁡ℤ|d≠0𝑝∧deg⁡d≤A∧∀e∈ℕ0coeff⁡d⁡e≤Ac⁡b=0∈Fin
172 11 171 eqeltrd ⊢A∈ℕ0→H⁡A∈Fin