Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  aannenlem1 Structured version   Visualization version   GIF version

Theorem aannenlem1 24282
 Description: Lemma for aannen 24285. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Hypothesis
Ref Expression
aannenlem.a 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})
Assertion
Ref Expression
aannenlem1 (𝐴 ∈ ℕ0 → (𝐻𝐴) ∈ Fin)
Distinct variable group:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒
Allowed substitution hints:   𝐻(𝑒,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem aannenlem1
StepHypRef Expression
1 breq2 4808 . . . . . . 7 (𝑎 = 𝐴 → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘𝑑) ≤ 𝐴))
2 breq2 4808 . . . . . . . 8 (𝑎 = 𝐴 → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴))
32ralbidv 3124 . . . . . . 7 (𝑎 = 𝐴 → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴))
41, 33anbi23d 1551 . . . . . 6 (𝑎 = 𝐴 → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)))
54rabbidv 3329 . . . . 5 (𝑎 = 𝐴 → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} = {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)})
65rexeqdv 3284 . . . 4 (𝑎 = 𝐴 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} (𝑐𝑏) = 0))
76rabbidv 3329 . . 3 (𝑎 = 𝐴 → {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} (𝑐𝑏) = 0})
8 aannenlem.a . . 3 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})
9 cnex 10209 . . . 4 ℂ ∈ V
109rabex 4964 . . 3 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} (𝑐𝑏) = 0} ∈ V
117, 8, 10fvmpt 6444 . 2 (𝐴 ∈ ℕ0 → (𝐻𝐴) = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} (𝑐𝑏) = 0})
12 iunrab 4719 . . 3 𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} (𝑐𝑏) = 0}
13 fzfi 12965 . . . . . . 7 (-𝐴...𝐴) ∈ Fin
14 fzfi 12965 . . . . . . 7 (0...𝐴) ∈ Fin
15 mapfi 8427 . . . . . . 7 (((-𝐴...𝐴) ∈ Fin ∧ (0...𝐴) ∈ Fin) → ((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ∈ Fin)
1613, 14, 15mp2an 710 . . . . . 6 ((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ∈ Fin
1716a1i 11 . . . . 5 (𝐴 ∈ ℕ0 → ((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ∈ Fin)
18 ovex 6841 . . . . . 6 ((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ∈ V
19 neeq1 2994 . . . . . . . . . . 11 (𝑑 = 𝑎 → (𝑑 ≠ 0𝑝𝑎 ≠ 0𝑝))
20 fveq2 6352 . . . . . . . . . . . 12 (𝑑 = 𝑎 → (deg‘𝑑) = (deg‘𝑎))
2120breq1d 4814 . . . . . . . . . . 11 (𝑑 = 𝑎 → ((deg‘𝑑) ≤ 𝐴 ↔ (deg‘𝑎) ≤ 𝐴))
22 fveq2 6352 . . . . . . . . . . . . . . 15 (𝑑 = 𝑎 → (coeff‘𝑑) = (coeff‘𝑎))
2322fveq1d 6354 . . . . . . . . . . . . . 14 (𝑑 = 𝑎 → ((coeff‘𝑑)‘𝑒) = ((coeff‘𝑎)‘𝑒))
2423fveq2d 6356 . . . . . . . . . . . . 13 (𝑑 = 𝑎 → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘𝑎)‘𝑒)))
2524breq1d 4814 . . . . . . . . . . . 12 (𝑑 = 𝑎 → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴 ↔ (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴))
2625ralbidv 3124 . . . . . . . . . . 11 (𝑑 = 𝑎 → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴 ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴))
2719, 21, 263anbi123d 1548 . . . . . . . . . 10 (𝑑 = 𝑎 → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴) ↔ (𝑎 ≠ 0𝑝 ∧ (deg‘𝑎) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)))
2827elrab 3504 . . . . . . . . 9 (𝑎 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ↔ (𝑎 ∈ (Poly‘ℤ) ∧ (𝑎 ≠ 0𝑝 ∧ (deg‘𝑎) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)))
29 simp3 1133 . . . . . . . . . 10 ((𝑎 ≠ 0𝑝 ∧ (deg‘𝑎) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴) → ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)
3029anim2i 594 . . . . . . . . 9 ((𝑎 ∈ (Poly‘ℤ) ∧ (𝑎 ≠ 0𝑝 ∧ (deg‘𝑎) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴))
3128, 30sylbi 207 . . . . . . . 8 (𝑎 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} → (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴))
32 0z 11580 . . . . . . . . . . . . . . 15 0 ∈ ℤ
33 eqid 2760 . . . . . . . . . . . . . . . 16 (coeff‘𝑎) = (coeff‘𝑎)
3433coef2 24186 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘𝑎):ℕ0⟶ℤ)
3532, 34mpan2 709 . . . . . . . . . . . . . 14 (𝑎 ∈ (Poly‘ℤ) → (coeff‘𝑎):ℕ0⟶ℤ)
3635ad2antrl 766 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → (coeff‘𝑎):ℕ0⟶ℤ)
3736ffnd 6207 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → (coeff‘𝑎) Fn ℕ0)
3835adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) → (coeff‘𝑎):ℕ0⟶ℤ)
3938ffvelrnda 6522 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → ((coeff‘𝑎)‘𝑒) ∈ ℤ)
4039zred 11674 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → ((coeff‘𝑎)‘𝑒) ∈ ℝ)
41 nn0re 11493 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
4241ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → 𝐴 ∈ ℝ)
4340, 42absled 14368 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → ((abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴 ↔ (-𝐴 ≤ ((coeff‘𝑎)‘𝑒) ∧ ((coeff‘𝑎)‘𝑒) ≤ 𝐴)))
44 nn0z 11592 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℕ0𝐴 ∈ ℤ)
4544ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → 𝐴 ∈ ℤ)
4645znegcld 11676 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → -𝐴 ∈ ℤ)
47 elfz 12525 . . . . . . . . . . . . . . . . . 18 ((((coeff‘𝑎)‘𝑒) ∈ ℤ ∧ -𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴) ↔ (-𝐴 ≤ ((coeff‘𝑎)‘𝑒) ∧ ((coeff‘𝑎)‘𝑒) ≤ 𝐴)))
4839, 46, 45, 47syl3anc 1477 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → (((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴) ↔ (-𝐴 ≤ ((coeff‘𝑎)‘𝑒) ∧ ((coeff‘𝑎)‘𝑒) ≤ 𝐴)))
4943, 48bitr4d 271 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → ((abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴 ↔ ((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴)))
5049biimpd 219 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) ∧ 𝑒 ∈ ℕ0) → ((abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴 → ((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴)))
5150ralimdva 3100 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ0𝑎 ∈ (Poly‘ℤ)) → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴 → ∀𝑒 ∈ ℕ0 ((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴)))
5251impr 650 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → ∀𝑒 ∈ ℕ0 ((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴))
53 fnfvrnss 6553 . . . . . . . . . . . . 13 (((coeff‘𝑎) Fn ℕ0 ∧ ∀𝑒 ∈ ℕ0 ((coeff‘𝑎)‘𝑒) ∈ (-𝐴...𝐴)) → ran (coeff‘𝑎) ⊆ (-𝐴...𝐴))
5437, 52, 53syl2anc 696 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → ran (coeff‘𝑎) ⊆ (-𝐴...𝐴))
55 df-f 6053 . . . . . . . . . . . 12 ((coeff‘𝑎):ℕ0⟶(-𝐴...𝐴) ↔ ((coeff‘𝑎) Fn ℕ0 ∧ ran (coeff‘𝑎) ⊆ (-𝐴...𝐴)))
5637, 54, 55sylanbrc 701 . . . . . . . . . . 11 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → (coeff‘𝑎):ℕ0⟶(-𝐴...𝐴))
57 fz0ssnn0 12628 . . . . . . . . . . 11 (0...𝐴) ⊆ ℕ0
58 fssres 6231 . . . . . . . . . . 11 (((coeff‘𝑎):ℕ0⟶(-𝐴...𝐴) ∧ (0...𝐴) ⊆ ℕ0) → ((coeff‘𝑎) ↾ (0...𝐴)):(0...𝐴)⟶(-𝐴...𝐴))
5956, 57, 58sylancl 697 . . . . . . . . . 10 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → ((coeff‘𝑎) ↾ (0...𝐴)):(0...𝐴)⟶(-𝐴...𝐴))
60 ovex 6841 . . . . . . . . . . 11 (-𝐴...𝐴) ∈ V
61 ovex 6841 . . . . . . . . . . 11 (0...𝐴) ∈ V
6260, 61elmap 8052 . . . . . . . . . 10 (((coeff‘𝑎) ↾ (0...𝐴)) ∈ ((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ↔ ((coeff‘𝑎) ↾ (0...𝐴)):(0...𝐴)⟶(-𝐴...𝐴))
6359, 62sylibr 224 . . . . . . . . 9 ((𝐴 ∈ ℕ0 ∧ (𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → ((coeff‘𝑎) ↾ (0...𝐴)) ∈ ((-𝐴...𝐴) ↑𝑚 (0...𝐴)))
6463ex 449 . . . . . . . 8 (𝐴 ∈ ℕ0 → ((𝑎 ∈ (Poly‘ℤ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴) → ((coeff‘𝑎) ↾ (0...𝐴)) ∈ ((-𝐴...𝐴) ↑𝑚 (0...𝐴))))
6531, 64syl5 34 . . . . . . 7 (𝐴 ∈ ℕ0 → (𝑎 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} → ((coeff‘𝑎) ↾ (0...𝐴)) ∈ ((-𝐴...𝐴) ↑𝑚 (0...𝐴))))
66 simp2 1132 . . . . . . . . . 10 ((𝑎 ≠ 0𝑝 ∧ (deg‘𝑎) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴) → (deg‘𝑎) ≤ 𝐴)
6766anim2i 594 . . . . . . . . 9 ((𝑎 ∈ (Poly‘ℤ) ∧ (𝑎 ≠ 0𝑝 ∧ (deg‘𝑎) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑎)‘𝑒)) ≤ 𝐴)) → (𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴))
6828, 67sylbi 207 . . . . . . . 8 (𝑎 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} → (𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴))
69 neeq1 2994 . . . . . . . . . . 11 (𝑑 = 𝑏 → (𝑑 ≠ 0𝑝𝑏 ≠ 0𝑝))
70 fveq2 6352 . . . . . . . . . . . 12 (𝑑 = 𝑏 → (deg‘𝑑) = (deg‘𝑏))
7170breq1d 4814 . . . . . . . . . . 11 (𝑑 = 𝑏 → ((deg‘𝑑) ≤ 𝐴 ↔ (deg‘𝑏) ≤ 𝐴))
72 fveq2 6352 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 → (coeff‘𝑑) = (coeff‘𝑏))
7372fveq1d 6354 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 → ((coeff‘𝑑)‘𝑒) = ((coeff‘𝑏)‘𝑒))
7473fveq2d 6356 . . . . . . . . . . . . 13 (𝑑 = 𝑏 → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘𝑏)‘𝑒)))
7574breq1d 4814 . . . . . . . . . . . 12 (𝑑 = 𝑏 → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴 ↔ (abs‘((coeff‘𝑏)‘𝑒)) ≤ 𝐴))
7675ralbidv 3124 . . . . . . . . . . 11 (𝑑 = 𝑏 → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴 ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑏)‘𝑒)) ≤ 𝐴))
7769, 71, 763anbi123d 1548 . . . . . . . . . 10 (𝑑 = 𝑏 → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴) ↔ (𝑏 ≠ 0𝑝 ∧ (deg‘𝑏) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑏)‘𝑒)) ≤ 𝐴)))
7877elrab 3504 . . . . . . . . 9 (𝑏 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ↔ (𝑏 ∈ (Poly‘ℤ) ∧ (𝑏 ≠ 0𝑝 ∧ (deg‘𝑏) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑏)‘𝑒)) ≤ 𝐴)))
79 simp2 1132 . . . . . . . . . 10 ((𝑏 ≠ 0𝑝 ∧ (deg‘𝑏) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑏)‘𝑒)) ≤ 𝐴) → (deg‘𝑏) ≤ 𝐴)
8079anim2i 594 . . . . . . . . 9 ((𝑏 ∈ (Poly‘ℤ) ∧ (𝑏 ≠ 0𝑝 ∧ (deg‘𝑏) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑏)‘𝑒)) ≤ 𝐴)) → (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴))
8178, 80sylbi 207 . . . . . . . 8 (𝑏 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} → (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴))
82 simplll 815 . . . . . . . . . . . . 13 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) → 𝑎 ∈ (Poly‘ℤ))
83 plyf 24153 . . . . . . . . . . . . 13 (𝑎 ∈ (Poly‘ℤ) → 𝑎:ℂ⟶ℂ)
84 ffn 6206 . . . . . . . . . . . . 13 (𝑎:ℂ⟶ℂ → 𝑎 Fn ℂ)
8582, 83, 843syl 18 . . . . . . . . . . . 12 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) → 𝑎 Fn ℂ)
86 simplrl 819 . . . . . . . . . . . . 13 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) → 𝑏 ∈ (Poly‘ℤ))
87 plyf 24153 . . . . . . . . . . . . 13 (𝑏 ∈ (Poly‘ℤ) → 𝑏:ℂ⟶ℂ)
88 ffn 6206 . . . . . . . . . . . . 13 (𝑏:ℂ⟶ℂ → 𝑏 Fn ℂ)
8986, 87, 883syl 18 . . . . . . . . . . . 12 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) → 𝑏 Fn ℂ)
90 simplrr 820 . . . . . . . . . . . . . . . . . 18 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))
9190adantr 472 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) ∧ 𝑑 ∈ (0...𝐴)) → ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))
9291fveq1d 6354 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) ∧ 𝑑 ∈ (0...𝐴)) → (((coeff‘𝑎) ↾ (0...𝐴))‘𝑑) = (((coeff‘𝑏) ↾ (0...𝐴))‘𝑑))
93 fvres 6368 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (0...𝐴) → (((coeff‘𝑎) ↾ (0...𝐴))‘𝑑) = ((coeff‘𝑎)‘𝑑))
9493adantl 473 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) ∧ 𝑑 ∈ (0...𝐴)) → (((coeff‘𝑎) ↾ (0...𝐴))‘𝑑) = ((coeff‘𝑎)‘𝑑))
95 fvres 6368 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (0...𝐴) → (((coeff‘𝑏) ↾ (0...𝐴))‘𝑑) = ((coeff‘𝑏)‘𝑑))
9695adantl 473 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) ∧ 𝑑 ∈ (0...𝐴)) → (((coeff‘𝑏) ↾ (0...𝐴))‘𝑑) = ((coeff‘𝑏)‘𝑑))
9792, 94, 963eqtr3d 2802 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) ∧ 𝑑 ∈ (0...𝐴)) → ((coeff‘𝑎)‘𝑑) = ((coeff‘𝑏)‘𝑑))
9897oveq1d 6828 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) ∧ 𝑑 ∈ (0...𝐴)) → (((coeff‘𝑎)‘𝑑) · (𝑐𝑑)) = (((coeff‘𝑏)‘𝑑) · (𝑐𝑑)))
9998sumeq2dv 14632 . . . . . . . . . . . . 13 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → Σ𝑑 ∈ (0...𝐴)(((coeff‘𝑎)‘𝑑) · (𝑐𝑑)) = Σ𝑑 ∈ (0...𝐴)(((coeff‘𝑏)‘𝑑) · (𝑐𝑑)))
100 simp-4l 825 . . . . . . . . . . . . . 14 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝑎 ∈ (Poly‘ℤ))
101 simp-4r 827 . . . . . . . . . . . . . . 15 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (deg‘𝑎) ≤ 𝐴)
102 dgrcl 24188 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (Poly‘ℤ) → (deg‘𝑎) ∈ ℕ0)
103 nn0z 11592 . . . . . . . . . . . . . . . . 17 ((deg‘𝑎) ∈ ℕ0 → (deg‘𝑎) ∈ ℤ)
104100, 102, 1033syl 18 . . . . . . . . . . . . . . . 16 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (deg‘𝑎) ∈ ℤ)
105 simplrl 819 . . . . . . . . . . . . . . . . 17 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝐴 ∈ ℕ0)
106105nn0zd 11672 . . . . . . . . . . . . . . . 16 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝐴 ∈ ℤ)
107 eluz 11893 . . . . . . . . . . . . . . . 16 (((deg‘𝑎) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ‘(deg‘𝑎)) ↔ (deg‘𝑎) ≤ 𝐴))
108104, 106, 107syl2anc 696 . . . . . . . . . . . . . . 15 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (𝐴 ∈ (ℤ‘(deg‘𝑎)) ↔ (deg‘𝑎) ≤ 𝐴))
109101, 108mpbird 247 . . . . . . . . . . . . . 14 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝐴 ∈ (ℤ‘(deg‘𝑎)))
110 simpr 479 . . . . . . . . . . . . . 14 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝑐 ∈ ℂ)
111 eqid 2760 . . . . . . . . . . . . . . 15 (deg‘𝑎) = (deg‘𝑎)
11233, 111coeid3 24195 . . . . . . . . . . . . . 14 ((𝑎 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ (ℤ‘(deg‘𝑎)) ∧ 𝑐 ∈ ℂ) → (𝑎𝑐) = Σ𝑑 ∈ (0...𝐴)(((coeff‘𝑎)‘𝑑) · (𝑐𝑑)))
113100, 109, 110, 112syl3anc 1477 . . . . . . . . . . . . 13 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (𝑎𝑐) = Σ𝑑 ∈ (0...𝐴)(((coeff‘𝑎)‘𝑑) · (𝑐𝑑)))
114 simp1rl 1305 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴))) ∧ 𝑐 ∈ ℂ) → 𝑏 ∈ (Poly‘ℤ))
1151143expa 1112 . . . . . . . . . . . . . 14 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝑏 ∈ (Poly‘ℤ))
116 simplrr 820 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) → (deg‘𝑏) ≤ 𝐴)
117116adantr 472 . . . . . . . . . . . . . . 15 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (deg‘𝑏) ≤ 𝐴)
118 dgrcl 24188 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (Poly‘ℤ) → (deg‘𝑏) ∈ ℕ0)
119 nn0z 11592 . . . . . . . . . . . . . . . . 17 ((deg‘𝑏) ∈ ℕ0 → (deg‘𝑏) ∈ ℤ)
120115, 118, 1193syl 18 . . . . . . . . . . . . . . . 16 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (deg‘𝑏) ∈ ℤ)
121 eluz 11893 . . . . . . . . . . . . . . . 16 (((deg‘𝑏) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ‘(deg‘𝑏)) ↔ (deg‘𝑏) ≤ 𝐴))
122120, 106, 121syl2anc 696 . . . . . . . . . . . . . . 15 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (𝐴 ∈ (ℤ‘(deg‘𝑏)) ↔ (deg‘𝑏) ≤ 𝐴))
123117, 122mpbird 247 . . . . . . . . . . . . . 14 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → 𝐴 ∈ (ℤ‘(deg‘𝑏)))
124 eqid 2760 . . . . . . . . . . . . . . 15 (coeff‘𝑏) = (coeff‘𝑏)
125 eqid 2760 . . . . . . . . . . . . . . 15 (deg‘𝑏) = (deg‘𝑏)
126124, 125coeid3 24195 . . . . . . . . . . . . . 14 ((𝑏 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ (ℤ‘(deg‘𝑏)) ∧ 𝑐 ∈ ℂ) → (𝑏𝑐) = Σ𝑑 ∈ (0...𝐴)(((coeff‘𝑏)‘𝑑) · (𝑐𝑑)))
127115, 123, 110, 126syl3anc 1477 . . . . . . . . . . . . 13 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (𝑏𝑐) = Σ𝑑 ∈ (0...𝐴)(((coeff‘𝑏)‘𝑑) · (𝑐𝑑)))
12899, 113, 1273eqtr4d 2804 . . . . . . . . . . . 12 (((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) ∧ 𝑐 ∈ ℂ) → (𝑎𝑐) = (𝑏𝑐))
12985, 89, 128eqfnfvd 6477 . . . . . . . . . . 11 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ (𝐴 ∈ ℕ0 ∧ ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))) → 𝑎 = 𝑏)
130129expr 644 . . . . . . . . . 10 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ 𝐴 ∈ ℕ0) → (((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)) → 𝑎 = 𝑏))
131 fveq2 6352 . . . . . . . . . . 11 (𝑎 = 𝑏 → (coeff‘𝑎) = (coeff‘𝑏))
132131reseq1d 5550 . . . . . . . . . 10 (𝑎 = 𝑏 → ((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)))
133130, 132impbid1 215 . . . . . . . . 9 ((((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) ∧ 𝐴 ∈ ℕ0) → (((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)) ↔ 𝑎 = 𝑏))
134133expcom 450 . . . . . . . 8 (𝐴 ∈ ℕ0 → (((𝑎 ∈ (Poly‘ℤ) ∧ (deg‘𝑎) ≤ 𝐴) ∧ (𝑏 ∈ (Poly‘ℤ) ∧ (deg‘𝑏) ≤ 𝐴)) → (((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)) ↔ 𝑎 = 𝑏)))
13568, 81, 134syl2ani 691 . . . . . . 7 (𝐴 ∈ ℕ0 → ((𝑎 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ∧ 𝑏 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)}) → (((coeff‘𝑎) ↾ (0...𝐴)) = ((coeff‘𝑏) ↾ (0...𝐴)) ↔ 𝑎 = 𝑏)))
13665, 135dom2d 8162 . . . . . 6 (𝐴 ∈ ℕ0 → (((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ∈ V → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ≼ ((-𝐴...𝐴) ↑𝑚 (0...𝐴))))
13718, 136mpi 20 . . . . 5 (𝐴 ∈ ℕ0 → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ≼ ((-𝐴...𝐴) ↑𝑚 (0...𝐴)))
138 domfi 8346 . . . . 5 ((((-𝐴...𝐴) ↑𝑚 (0...𝐴)) ∈ Fin ∧ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ≼ ((-𝐴...𝐴) ↑𝑚 (0...𝐴))) → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ∈ Fin)
13917, 137, 138syl2anc 696 . . . 4 (𝐴 ∈ ℕ0 → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ∈ Fin)
140 neeq1 2994 . . . . . . . . 9 (𝑑 = 𝑐 → (𝑑 ≠ 0𝑝𝑐 ≠ 0𝑝))
141 fveq2 6352 . . . . . . . . . 10 (𝑑 = 𝑐 → (deg‘𝑑) = (deg‘𝑐))
142141breq1d 4814 . . . . . . . . 9 (𝑑 = 𝑐 → ((deg‘𝑑) ≤ 𝐴 ↔ (deg‘𝑐) ≤ 𝐴))
143 fveq2 6352 . . . . . . . . . . . . 13 (𝑑 = 𝑐 → (coeff‘𝑑) = (coeff‘𝑐))
144143fveq1d 6354 . . . . . . . . . . . 12 (𝑑 = 𝑐 → ((coeff‘𝑑)‘𝑒) = ((coeff‘𝑐)‘𝑒))
145144fveq2d 6356 . . . . . . . . . . 11 (𝑑 = 𝑐 → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘𝑐)‘𝑒)))
146145breq1d 4814 . . . . . . . . . 10 (𝑑 = 𝑐 → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴 ↔ (abs‘((coeff‘𝑐)‘𝑒)) ≤ 𝐴))
147146ralbidv 3124 . . . . . . . . 9 (𝑑 = 𝑐 → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴 ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑐)‘𝑒)) ≤ 𝐴))
148140, 142, 1473anbi123d 1548 . . . . . . . 8 (𝑑 = 𝑐 → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴) ↔ (𝑐 ≠ 0𝑝 ∧ (deg‘𝑐) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑐)‘𝑒)) ≤ 𝐴)))
149148elrab 3504 . . . . . . 7 (𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ↔ (𝑐 ∈ (Poly‘ℤ) ∧ (𝑐 ≠ 0𝑝 ∧ (deg‘𝑐) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑐)‘𝑒)) ≤ 𝐴)))
150 simp1 1131 . . . . . . . 8 ((𝑐 ≠ 0𝑝 ∧ (deg‘𝑐) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑐)‘𝑒)) ≤ 𝐴) → 𝑐 ≠ 0𝑝)
151150anim2i 594 . . . . . . 7 ((𝑐 ∈ (Poly‘ℤ) ∧ (𝑐 ≠ 0𝑝 ∧ (deg‘𝑐) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑐)‘𝑒)) ≤ 𝐴)) → (𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝))
152149, 151sylbi 207 . . . . . 6 (𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} → (𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝))
153 plyf 24153 . . . . . . . . . . . . 13 (𝑐 ∈ (Poly‘ℤ) → 𝑐:ℂ⟶ℂ)
154153ffnd 6207 . . . . . . . . . . . 12 (𝑐 ∈ (Poly‘ℤ) → 𝑐 Fn ℂ)
155154adantr 472 . . . . . . . . . . 11 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → 𝑐 Fn ℂ)
156 fniniseg 6501 . . . . . . . . . . 11 (𝑐 Fn ℂ → (𝑎 ∈ (𝑐 “ {0}) ↔ (𝑎 ∈ ℂ ∧ (𝑐𝑎) = 0)))
157155, 156syl 17 . . . . . . . . . 10 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → (𝑎 ∈ (𝑐 “ {0}) ↔ (𝑎 ∈ ℂ ∧ (𝑐𝑎) = 0)))
158 fveq2 6352 . . . . . . . . . . . 12 (𝑏 = 𝑎 → (𝑐𝑏) = (𝑐𝑎))
159158eqeq1d 2762 . . . . . . . . . . 11 (𝑏 = 𝑎 → ((𝑐𝑏) = 0 ↔ (𝑐𝑎) = 0))
160159elrab 3504 . . . . . . . . . 10 (𝑎 ∈ {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ↔ (𝑎 ∈ ℂ ∧ (𝑐𝑎) = 0))
161157, 160syl6rbbr 279 . . . . . . . . 9 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → (𝑎 ∈ {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ↔ 𝑎 ∈ (𝑐 “ {0})))
162161eqrdv 2758 . . . . . . . 8 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} = (𝑐 “ {0}))
163 eqid 2760 . . . . . . . . . 10 (𝑐 “ {0}) = (𝑐 “ {0})
164163fta1 24262 . . . . . . . . 9 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → ((𝑐 “ {0}) ∈ Fin ∧ (♯‘(𝑐 “ {0})) ≤ (deg‘𝑐)))
165164simpld 477 . . . . . . . 8 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → (𝑐 “ {0}) ∈ Fin)
166162, 165eqeltrd 2839 . . . . . . 7 ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin)
167166a1i 11 . . . . . 6 (𝐴 ∈ ℕ0 → ((𝑐 ∈ (Poly‘ℤ) ∧ 𝑐 ≠ 0𝑝) → {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin))
168152, 167syl5 34 . . . . 5 (𝐴 ∈ ℕ0 → (𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} → {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin))
169168ralrimiv 3103 . . . 4 (𝐴 ∈ ℕ0 → ∀𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin)
170 iunfi 8419 . . . 4 (({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} ∈ Fin ∧ ∀𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin) → 𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin)
171139, 169, 170syl2anc 696 . . 3 (𝐴 ∈ ℕ0 𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} {𝑏 ∈ ℂ ∣ (𝑐𝑏) = 0} ∈ Fin)
17212, 171syl5eqelr 2844 . 2 (𝐴 ∈ ℕ0 → {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝐴 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝐴)} (𝑐𝑏) = 0} ∈ Fin)
17311, 172eqeltrd 2839 1 (𝐴 ∈ ℕ0 → (𝐻𝐴) ∈ Fin)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  {crab 3054  Vcvv 3340   ⊆ wss 3715  {csn 4321  ∪ ciun 4672   class class class wbr 4804   ↦ cmpt 4881  ◡ccnv 5265  ran crn 5267   ↾ cres 5268   “ cima 5269   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813   ↑𝑚 cmap 8023   ≼ cdom 8119  Fincfn 8121  ℂcc 10126  ℝcr 10127  0cc0 10128   · cmul 10133   ≤ cle 10267  -cneg 10459  ℕ0cn0 11484  ℤcz 11569  ℤ≥cuz 11879  ...cfz 12519  ↑cexp 13054  ♯chash 13311  abscabs 14173  Σcsu 14615  0𝑝c0p 23635  Polycply 24139  coeffccoe 24141  degcdgr 24142 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-xnn0 11556  df-z 11570  df-uz 11880  df-rp 12026  df-fz 12520  df-fzo 12660  df-fl 12787  df-seq 12996  df-exp 13055  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-rlim 14419  df-sum 14616  df-0p 23636  df-ply 24143  df-idp 24144  df-coe 24145  df-dgr 24146  df-quot 24245 This theorem is referenced by:  aannenlem3  24284
 Copyright terms: Public domain W3C validator