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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ 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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ 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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A
5 2 4 3anbi23d ⊢ a = A → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A
6 5 rabbidv ⊢ a = A → d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a = d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A
7 6 rexeqdv ⊢ a = A → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A c ⁡ b = 0
8 7 rabbidv ⊢ a = A → b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A c ⁡ b = 0
9 cnex ⊢ ℂ ∈ V
10 9 rabex ⊢ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A c ⁡ b = 0 ∈ V
11 8 1 10 fvmpt ⊢ A ∈ ℕ 0 → H ⁡ A = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A c ⁡ b = 0
12 iunrab ⊢ ⋃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A b ∈ ℂ | c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A c ⁡ b = 0
13 fzfi ⊢ − A … A ∈ Fin
14 fzfi ⊢ 0 … A ∈ Fin
15 mapfi ⊢ − A … A ∈ Fin ∧ 0 … A ∈ Fin → − A … A 0 … A ∈ Fin
16 13 14 15 mp2an ⊢ − A … A 0 … A ∈ Fin
17 16 a1i ⊢ A ∈ ℕ 0 → − A … A 0 … A ∈ Fin
18 ovex ⊢ − A … A 0 … 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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A
27 19 21 26 3anbi123d ⊢ d = a → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ a ≠ 0 𝑝 ∧ deg ⁡ a ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A
28 27 elrab ⊢ a ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ a ∈ Poly ⁡ ℤ ∧ a ≠ 0 𝑝 ∧ deg ⁡ a ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A
29 simp3 ⊢ a ≠ 0 𝑝 ∧ deg ⁡ a ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A
30 29 anim2i ⊢ a ∈ Poly ⁡ ℤ ∧ a ≠ 0 𝑝 ∧ deg ⁡ a ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A
31 28 30 sylbi ⊢ a ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A → a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ 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 ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → coeff ⁡ a : ℕ 0 ⟶ ℤ
37 36 ffnd ⊢ A ∈ ℕ 0 ∧ a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → coeff ⁡ a Fn ℕ 0
38 35 adantl ⊢ A ∈ ℕ 0 ∧ a ∈ Poly ⁡ ℤ → coeff ⁡ a : ℕ 0 ⟶ ℤ
39 38 ffvelrnda ⊢ 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 ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ∈ − A … A
52 51 impr ⊢ A ∈ ℕ 0 ∧ a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ∈ − A … A
53 fnfvrnss ⊢ coeff ⁡ a Fn ℕ 0 ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ∈ − A … A → ran ⁡ coeff ⁡ a ⊆ − A … A
54 37 52 53 syl2anc ⊢ A ∈ ℕ 0 ∧ a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → ran ⁡ coeff ⁡ a ⊆ − A … A
55 df-f ⊢ coeff ⁡ a : ℕ 0 ⟶ − A … A ↔ coeff ⁡ a Fn ℕ 0 ∧ ran ⁡ coeff ⁡ a ⊆ − A … A
56 37 54 55 sylanbrc ⊢ A ∈ ℕ 0 ∧ a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ 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 ∈ ℕ 0 coeff ⁡ 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 … A 0 … A ↔ coeff ⁡ a ↾ 0 … A : 0 … A ⟶ − A … A
63 59 62 sylibr ⊢ A ∈ ℕ 0 ∧ a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → coeff ⁡ a ↾ 0 … A ∈ − A … A 0 … A
64 63 ex ⊢ A ∈ ℕ 0 → a ∈ Poly ⁡ ℤ ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → coeff ⁡ a ↾ 0 … A ∈ − A … A 0 … A
65 31 64 syl5 ⊢ A ∈ ℕ 0 → a ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A → coeff ⁡ a ↾ 0 … A ∈ − A … A 0 … A
66 simp2 ⊢ a ≠ 0 𝑝 ∧ deg ⁡ a ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → deg ⁡ a ≤ A
67 66 anim2i ⊢ a ∈ Poly ⁡ ℤ ∧ a ≠ 0 𝑝 ∧ deg ⁡ a ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ a ⁡ e ≤ A → a ∈ Poly ⁡ ℤ ∧ deg ⁡ a ≤ A
68 28 67 sylbi ⊢ a ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ 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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ ∀ e ∈ ℕ 0 coeff ⁡ b ⁡ e ≤ A
77 69 71 76 3anbi123d ⊢ d = b → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ b ≠ 0 𝑝 ∧ deg ⁡ b ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ b ⁡ e ≤ A
78 77 elrab ⊢ b ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ b ∈ Poly ⁡ ℤ ∧ b ≠ 0 𝑝 ∧ deg ⁡ b ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ b ⁡ e ≤ A
79 simp2 ⊢ b ≠ 0 𝑝 ∧ deg ⁡ b ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ b ⁡ e ≤ A → deg ⁡ b ≤ A
80 79 anim2i ⊢ b ∈ Poly ⁡ ℤ ∧ b ≠ 0 𝑝 ∧ deg ⁡ b ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ b ⁡ e ≤ A → b ∈ Poly ⁡ ℤ ∧ deg ⁡ b ≤ A
81 78 80 sylbi ⊢ b ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ 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 : ℂ ⟶ ℂ → a Fn ℂ
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 → a Fn ℂ
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 : ℂ ⟶ ℂ → b Fn ℂ
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 → b Fn ℂ
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 ⁢ c d = coeff ⁡ b ⁡ d ⁢ c d
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 = 0 A coeff ⁡ a ⁡ d ⁢ c d = ∑ d = 0 A coeff ⁡ b ⁡ d ⁢ c d
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 = 0 A coeff ⁡ a ⁡ d ⁢ c d
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 = 0 A coeff ⁡ a ⁡ d ⁢ c d
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 = 0 A coeff ⁡ b ⁡ d ⁢ c d
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 = 0 A coeff ⁡ b ⁡ d ⁢ c d
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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ∧ b ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A → coeff ⁡ a ↾ 0 … A = coeff ⁡ b ↾ 0 … A ↔ a = b
136 65 135 dom2d ⊢ A ∈ ℕ 0 → − A … A 0 … A ∈ V → d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ≼ − A … A 0 … A
137 18 136 mpi ⊢ A ∈ ℕ 0 → d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ≼ − A … A 0 … A
138 domfi ⊢ − A … A 0 … A ∈ Fin ∧ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ≼ − A … A 0 … A → d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ∈ Fin
139 17 137 138 syl2anc ⊢ A ∈ ℕ 0 → d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ 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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ ∀ e ∈ ℕ 0 coeff ⁡ c ⁡ e ≤ A
148 140 142 147 3anbi123d ⊢ d = c → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ c ≠ 0 𝑝 ∧ deg ⁡ c ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ c ⁡ e ≤ A
149 148 elrab ⊢ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ↔ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 ∧ deg ⁡ c ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ c ⁡ e ≤ A
150 simp1 ⊢ c ≠ 0 𝑝 ∧ deg ⁡ c ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ c ⁡ e ≤ A → c ≠ 0 𝑝
151 150 anim2i ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 ∧ deg ⁡ c ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ c ⁡ e ≤ A → c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝
152 149 151 sylbi ⊢ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ 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 ⁡ ℤ → c Fn ℂ
157 156 adantr ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 → c Fn ℂ
158 fniniseg ⊢ c Fn ℂ → a ∈ c -1 0 ↔ a ∈ ℂ ∧ c ⁡ a = 0
159 157 158 syl ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 → a ∈ c -1 0 ↔ a ∈ ℂ ∧ c ⁡ a = 0
160 154 159 bitr4id ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 → a ∈ b ∈ ℂ | c ⁡ b = 0 ↔ a ∈ c -1 0
161 160 eqrdv ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 → b ∈ ℂ | c ⁡ b = 0 = c -1 0
162 eqid ⊢ c -1 0 = c -1 0
163 162 fta1 ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 → c -1 0 ∈ Fin ∧ c -1 0 ≤ deg ⁡ c
164 163 simpld ⊢ c ∈ Poly ⁡ ℤ ∧ c ≠ 0 𝑝 → c -1 0 ∈ 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 ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A → b ∈ ℂ | c ⁡ b = 0 ∈ Fin
168 167 ralrimiv ⊢ A ∈ ℕ 0 → ∀ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A b ∈ ℂ | c ⁡ b = 0 ∈ Fin
169 iunfi ⊢ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A ∈ Fin ∧ ∀ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A b ∈ ℂ | c ⁡ b = 0 ∈ Fin → ⋃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A b ∈ ℂ | c ⁡ b = 0 ∈ Fin
170 139 168 169 syl2anc ⊢ A ∈ ℕ 0 → ⋃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A b ∈ ℂ | c ⁡ b = 0 ∈ Fin
171 12 170 eqeltrrid ⊢ A ∈ ℕ 0 → b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ A ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ A c ⁡ b = 0 ∈ Fin
172 11 171 eqeltrd ⊢ A ∈ ℕ 0 → H ⁡ A ∈ Fin