Metamath Proof Explorer

Theorem aannenlem1

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

Ref Expression
Hypothesis aannenlem.a ⊢ 𝐻 = ( 𝑎 ∈ ℕ0 ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } )
Assertion aannenlem1 ( 𝐴 ∈ ℕ0 → ( 𝐻 ‘ 𝐴 ) ∈ Fin )

Proof

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