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

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

Proof of Theorem aannenlem2
Dummy variables 𝑓 𝑔 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveqeq2 6834 . . . . . . . . . . 11 (𝑏 = 𝑔 → ((𝑐𝑏) = 0 ↔ (𝑐𝑔) = 0))
21rexbidv 3171 . . . . . . . . . 10 (𝑏 = 𝑔 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑔) = 0))
3 simp3 1137 . . . . . . . . . 10 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ ℂ)
4 neeq1 3003 . . . . . . . . . . . . 13 (𝑑 = → (𝑑 ≠ 0𝑝 ≠ 0𝑝))
5 fveq2 6825 . . . . . . . . . . . . . 14 (𝑑 = → (deg‘𝑑) = (deg‘))
65breq1d 5102 . . . . . . . . . . . . 13 (𝑑 = → ((deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ↔ (deg‘) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
7 fveq2 6825 . . . . . . . . . . . . . . . . 17 (𝑑 = → (coeff‘𝑑) = (coeff‘))
87fveq1d 6827 . . . . . . . . . . . . . . . 16 (𝑑 = → ((coeff‘𝑑)‘𝑒) = ((coeff‘)‘𝑒))
98fveq2d 6829 . . . . . . . . . . . . . . 15 (𝑑 = → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘)‘𝑒)))
109breq1d 5102 . . . . . . . . . . . . . 14 (𝑑 = → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ↔ (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
1110ralbidv 3170 . . . . . . . . . . . . 13 (𝑑 = → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
124, 6, 113anbi123d 1435 . . . . . . . . . . . 12 (𝑑 = → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )) ↔ ( ≠ 0𝑝 ∧ (deg‘) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))))
13 eldifi 4073 . . . . . . . . . . . . . 14 ( ∈ ((Poly‘ℤ) ∖ {0𝑝}) → ∈ (Poly‘ℤ))
1413adantr 481 . . . . . . . . . . . . 13 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → ∈ (Poly‘ℤ))
15143adant2 1130 . . . . . . . . . . . 12 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∈ (Poly‘ℤ))
16 eldifsni 4737 . . . . . . . . . . . . . . 15 ( ∈ ((Poly‘ℤ) ∖ {0𝑝}) → ≠ 0𝑝)
1716adantr 481 . . . . . . . . . . . . . 14 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → ≠ 0𝑝)
18 0nn0 12349 . . . . . . . . . . . . . . . . . 18 0 ∈ ℕ0
19 dgrcl 25500 . . . . . . . . . . . . . . . . . . 19 ( ∈ (Poly‘ℤ) → (deg‘) ∈ ℕ0)
2014, 19syl 17 . . . . . . . . . . . . . . . . . 18 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘) ∈ ℕ0)
21 prssi 4768 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℕ0 ∧ (deg‘) ∈ ℕ0) → {0, (deg‘)} ⊆ ℕ0)
2218, 20, 21sylancr 587 . . . . . . . . . . . . . . . . 17 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → {0, (deg‘)} ⊆ ℕ0)
23 ssrab2 4025 . . . . . . . . . . . . . . . . . 18 {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ⊆ ℕ0
2423a1i 11 . . . . . . . . . . . . . . . . 17 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ⊆ ℕ0)
2522, 24unssd 4133 . . . . . . . . . . . . . . . 16 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℕ0)
26 nn0ssre 12338 . . . . . . . . . . . . . . . . 17 0 ⊆ ℝ
27 ressxr 11120 . . . . . . . . . . . . . . . . 17 ℝ ⊆ ℝ*
2826, 27sstri 3941 . . . . . . . . . . . . . . . 16 0 ⊆ ℝ*
2925, 28sstrdi 3944 . . . . . . . . . . . . . . 15 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℝ*)
30 fvex 6838 . . . . . . . . . . . . . . . . 17 (deg‘) ∈ V
3130prid2 4711 . . . . . . . . . . . . . . . 16 (deg‘) ∈ {0, (deg‘)}
32 elun1 4123 . . . . . . . . . . . . . . . 16 ((deg‘) ∈ {0, (deg‘)} → (deg‘) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
3331, 32ax-mp 5 . . . . . . . . . . . . . . 15 (deg‘) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))})
34 supxrub 13159 . . . . . . . . . . . . . . 15 ((({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℝ* ∧ (deg‘) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))})) → (deg‘) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))
3529, 33, 34sylancl 586 . . . . . . . . . . . . . 14 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))
3629adantr 481 . . . . . . . . . . . . . . . 16 ((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) → ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℝ*)
37 fveq2 6825 . . . . . . . . . . . . . . . . . . . 20 (((coeff‘)‘𝑒) = 0 → (abs‘((coeff‘)‘𝑒)) = (abs‘0))
38 abs0 15096 . . . . . . . . . . . . . . . . . . . 20 (abs‘0) = 0
3937, 38eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 (((coeff‘)‘𝑒) = 0 → (abs‘((coeff‘)‘𝑒)) = 0)
40 c0ex 11070 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
4140prid1 4710 . . . . . . . . . . . . . . . . . . . 20 0 ∈ {0, (deg‘)}
42 elun1 4123 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ {0, (deg‘)} → 0 ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))})
4439, 43eqeltrdi 2845 . . . . . . . . . . . . . . . . . 18 (((coeff‘)‘𝑒) = 0 → (abs‘((coeff‘)‘𝑒)) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
4544adantl 482 . . . . . . . . . . . . . . . . 17 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) = 0) → (abs‘((coeff‘)‘𝑒)) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
46 eqeq1 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (abs‘((coeff‘)‘𝑒)) → (𝑔 = (abs‘((coeff‘)‘𝑖)) ↔ (abs‘((coeff‘)‘𝑒)) = (abs‘((coeff‘)‘𝑖))))
4746rexbidv 3171 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (abs‘((coeff‘)‘𝑒)) → (∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖)) ↔ ∃𝑖 ∈ (0...(deg‘))(abs‘((coeff‘)‘𝑒)) = (abs‘((coeff‘)‘𝑖))))
48 0z 12431 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℤ
49 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 (coeff‘) = (coeff‘)
5049coef2 25498 . . . . . . . . . . . . . . . . . . . . . . 23 (( ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘):ℕ0⟶ℤ)
5114, 48, 50sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → (coeff‘):ℕ0⟶ℤ)
5251ffvelcdmda 7017 . . . . . . . . . . . . . . . . . . . . 21 ((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) → ((coeff‘)‘𝑒) ∈ ℤ)
53 nn0abscl 15123 . . . . . . . . . . . . . . . . . . . . 21 (((coeff‘)‘𝑒) ∈ ℤ → (abs‘((coeff‘)‘𝑒)) ∈ ℕ0)
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . 20 ((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) → (abs‘((coeff‘)‘𝑒)) ∈ ℕ0)
5554adantr 481 . . . . . . . . . . . . . . . . . . 19 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → (abs‘((coeff‘)‘𝑒)) ∈ ℕ0)
56 simplr 766 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → 𝑒 ∈ ℕ0)
5720ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → (deg‘) ∈ ℕ0)
5814ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → ∈ (Poly‘ℤ))
59 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → ((coeff‘)‘𝑒) ≠ 0)
60 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (deg‘) = (deg‘)
6149, 60dgrub 25501 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ (Poly‘ℤ) ∧ 𝑒 ∈ ℕ0 ∧ ((coeff‘)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘))
6258, 56, 59, 61syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘))
63 elfz2nn0 13448 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (0...(deg‘)) ↔ (𝑒 ∈ ℕ0 ∧ (deg‘) ∈ ℕ0𝑒 ≤ (deg‘)))
6456, 57, 62, 63syl3anbrc 1342 . . . . . . . . . . . . . . . . . . . 20 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → 𝑒 ∈ (0...(deg‘)))
65 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (abs‘((coeff‘)‘𝑒)) = (abs‘((coeff‘)‘𝑒))
66 2fveq3 6830 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑒 → (abs‘((coeff‘)‘𝑖)) = (abs‘((coeff‘)‘𝑒)))
6766rspceeqv 3584 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 ∈ (0...(deg‘)) ∧ (abs‘((coeff‘)‘𝑒)) = (abs‘((coeff‘)‘𝑒))) → ∃𝑖 ∈ (0...(deg‘))(abs‘((coeff‘)‘𝑒)) = (abs‘((coeff‘)‘𝑖)))
6864, 65, 67sylancl 586 . . . . . . . . . . . . . . . . . . 19 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → ∃𝑖 ∈ (0...(deg‘))(abs‘((coeff‘)‘𝑒)) = (abs‘((coeff‘)‘𝑖)))
6947, 55, 68elrabd 3636 . . . . . . . . . . . . . . . . . 18 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → (abs‘((coeff‘)‘𝑒)) ∈ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))})
70 elun2 4124 . . . . . . . . . . . . . . . . . 18 ((abs‘((coeff‘)‘𝑒)) ∈ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} → (abs‘((coeff‘)‘𝑒)) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
7169, 70syl 17 . . . . . . . . . . . . . . . . 17 (((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) ∧ ((coeff‘)‘𝑒) ≠ 0) → (abs‘((coeff‘)‘𝑒)) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
7245, 71pm2.61dane 3029 . . . . . . . . . . . . . . . 16 ((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) → (abs‘((coeff‘)‘𝑒)) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
73 supxrub 13159 . . . . . . . . . . . . . . . 16 ((({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℝ* ∧ (abs‘((coeff‘)‘𝑒)) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))})) → (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))
7436, 72, 73syl2anc 584 . . . . . . . . . . . . . . 15 ((( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ0) → (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))
7574ralrimiva 3139 . . . . . . . . . . . . . 14 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))
7617, 35, 753jca 1127 . . . . . . . . . . . . 13 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → ( ≠ 0𝑝 ∧ (deg‘) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
77763adant2 1130 . . . . . . . . . . . 12 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ( ≠ 0𝑝 ∧ (deg‘) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
7812, 15, 77elrabd 3636 . . . . . . . . . . 11 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))})
79 simp2 1136 . . . . . . . . . . 11 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (𝑔) = 0)
80 fveq1 6824 . . . . . . . . . . . . 13 (𝑐 = → (𝑐𝑔) = (𝑔))
8180eqeq1d 2738 . . . . . . . . . . . 12 (𝑐 = → ((𝑐𝑔) = 0 ↔ (𝑔) = 0))
8281rspcev 3570 . . . . . . . . . . 11 (( ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} ∧ (𝑔) = 0) → ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑔) = 0)
8378, 79, 82syl2anc 584 . . . . . . . . . 10 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑔) = 0)
842, 3, 83elrabd 3636 . . . . . . . . 9 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0})
85 prfi 9187 . . . . . . . . . . . . . 14 {0, (deg‘)} ∈ Fin
86 fzfi 13793 . . . . . . . . . . . . . . . 16 (0...(deg‘)) ∈ Fin
87 abrexfi 9217 . . . . . . . . . . . . . . . 16 ((0...(deg‘)) ∈ Fin → {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ∈ Fin)
8886, 87ax-mp 5 . . . . . . . . . . . . . . 15 {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ∈ Fin
89 rabssab 4030 . . . . . . . . . . . . . . 15 {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}
90 ssfi 9038 . . . . . . . . . . . . . . 15 (({𝑔 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ∈ Fin ∧ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) → {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ∈ Fin)
9188, 89, 90mp2an 689 . . . . . . . . . . . . . 14 {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ∈ Fin
92 unfi 9037 . . . . . . . . . . . . . 14 (({0, (deg‘)} ∈ Fin ∧ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))} ∈ Fin) → ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ∈ Fin)
9385, 91, 92mp2an 689 . . . . . . . . . . . . 13 ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ∈ Fin
9433ne0ii 4284 . . . . . . . . . . . . 13 ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ≠ ∅
95 xrltso 12976 . . . . . . . . . . . . . 14 < Or ℝ*
96 fisupcl 9326 . . . . . . . . . . . . . 14 (( < Or ℝ* ∧ (({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ∈ Fin ∧ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ≠ ∅ ∧ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℝ*)) → sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
9795, 96mpan 687 . . . . . . . . . . . . 13 ((({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ∈ Fin ∧ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ≠ ∅ ∧ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}) ⊆ ℝ*) → sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
9893, 94, 29, 97mp3an12i 1464 . . . . . . . . . . . 12 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∈ ({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}))
9925, 98sseldd 3933 . . . . . . . . . . 11 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∈ ℕ0)
100993adant2 1130 . . . . . . . . . 10 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∈ ℕ0)
101 eqidd 2737 . . . . . . . . . 10 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0})
102 breq2 5096 . . . . . . . . . . . . . . 15 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
103 breq2 5096 . . . . . . . . . . . . . . . 16 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
104103ralbidv 3170 . . . . . . . . . . . . . . 15 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < )))
105102, 1043anbi23d 1438 . . . . . . . . . . . . . 14 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))))
106105rabbidv 3411 . . . . . . . . . . . . 13 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} = {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))})
107106rexeqdv 3310 . . . . . . . . . . . 12 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0))
108107rabbidv 3411 . . . . . . . . . . 11 (𝑎 = sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) → {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0})
109108rspceeqv 3584 . . . . . . . . . 10 ((sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∈ ℕ0 ∧ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0}) → ∃𝑎 ∈ ℕ0 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})
110100, 101, 109syl2anc 584 . . . . . . . . 9 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑎 ∈ ℕ0 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})
111 cnex 11053 . . . . . . . . . . 11 ℂ ∈ V
112111rabex 5276 . . . . . . . . . 10 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} ∈ V
113 eleq2 2825 . . . . . . . . . . 11 (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} → (𝑔𝑓𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0}))
114 eqeq1 2740 . . . . . . . . . . . 12 (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} → (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} ↔ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
115114rexbidv 3171 . . . . . . . . . . 11 (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} → (∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} ↔ ∃𝑎 ∈ ℕ0 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
116113, 115anbi12d 631 . . . . . . . . . 10 (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} → ((𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}) ↔ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} ∧ ∃𝑎 ∈ ℕ0 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})))
117112, 116spcev 3554 . . . . . . . . 9 ((𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} ∧ ∃𝑎 ∈ ℕ0 {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ) ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘)} ∪ {𝑔 ∈ ℕ0 ∣ ∃𝑖 ∈ (0...(deg‘))𝑔 = (abs‘((coeff‘)‘𝑖))}), ℝ*, < ))} (𝑐𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}) → ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
11884, 110, 117syl2anc 584 . . . . . . . 8 (( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
1191183exp 1118 . . . . . . 7 ( ∈ ((Poly‘ℤ) ∖ {0𝑝}) → ((𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))))
120119rexlimiv 3141 . . . . . 6 (∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})))
121120impcom 408 . . . . 5 ((𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0) → ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
122 eleq2 2825 . . . . . . . . 9 (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} → (𝑔𝑓𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
1231rexbidv 3171 . . . . . . . . . . 11 (𝑏 = 𝑔 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑔) = 0))
124123elrab 3634 . . . . . . . . . 10 (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} ↔ (𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑔) = 0))
125 simp1 1135 . . . . . . . . . . . . . . 15 (( ≠ 0𝑝 ∧ (deg‘) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ 𝑎) → ≠ 0𝑝)
126125anim2i 617 . . . . . . . . . . . . . 14 (( ∈ (Poly‘ℤ) ∧ ( ≠ 0𝑝 ∧ (deg‘) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ 𝑎)) → ( ∈ (Poly‘ℤ) ∧ ≠ 0𝑝))
1275breq1d 5102 . . . . . . . . . . . . . . . 16 (𝑑 = → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘) ≤ 𝑎))
1289breq1d 5102 . . . . . . . . . . . . . . . . 17 (𝑑 = → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘)‘𝑒)) ≤ 𝑎))
129128ralbidv 3170 . . . . . . . . . . . . . . . 16 (𝑑 = → (∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ 𝑎))
1304, 127, 1293anbi123d 1435 . . . . . . . . . . . . . . 15 (𝑑 = → ((𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ ( ≠ 0𝑝 ∧ (deg‘) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ 𝑎)))
131130elrab 3634 . . . . . . . . . . . . . 14 ( ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ↔ ( ∈ (Poly‘ℤ) ∧ ( ≠ 0𝑝 ∧ (deg‘) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘)‘𝑒)) ≤ 𝑎)))
132 eldifsn 4734 . . . . . . . . . . . . . 14 ( ∈ ((Poly‘ℤ) ∖ {0𝑝}) ↔ ( ∈ (Poly‘ℤ) ∧ ≠ 0𝑝))
133126, 131, 1323imtr4i 291 . . . . . . . . . . . . 13 ( ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} → ∈ ((Poly‘ℤ) ∖ {0𝑝}))
134133ssriv 3936 . . . . . . . . . . . 12 {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0𝑝})
135 ssrexv 3999 . . . . . . . . . . . . 13 ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑔) = 0 → ∃𝑐 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑐𝑔) = 0))
13681cbvrexvw 3222 . . . . . . . . . . . . 13 (∃𝑐 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑐𝑔) = 0 ↔ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0)
137135, 136syl6ib 250 . . . . . . . . . . . 12 ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑔) = 0 → ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0))
138134, 137ax-mp 5 . . . . . . . . . . 11 (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑔) = 0 → ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0)
139138anim2i 617 . . . . . . . . . 10 ((𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑔) = 0) → (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0))
140124, 139sylbi 216 . . . . . . . . 9 (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} → (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0))
141122, 140syl6bi 252 . . . . . . . 8 (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} → (𝑔𝑓 → (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0)))
142141rexlimivw 3144 . . . . . . 7 (∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0} → (𝑔𝑓 → (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0)))
143142impcom 408 . . . . . 6 ((𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0))
144143exlimiv 1932 . . . . 5 (∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0))
145121, 144impbii 208 . . . 4 ((𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0) ↔ ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
146 elaa 25582 . . . 4 (𝑔 ∈ 𝔸 ↔ (𝑔 ∈ ℂ ∧ ∃ ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑔) = 0))
147 eluniab 4867 . . . 4 (𝑔 {𝑓 ∣ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}} ↔ ∃𝑓(𝑔𝑓 ∧ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}))
148145, 146, 1473bitr4i 302 . . 3 (𝑔 ∈ 𝔸 ↔ 𝑔 {𝑓 ∣ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}})
149148eqriv 2733 . 2 𝔸 = {𝑓 ∣ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}}
150 aannenlem.a . . . 4 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0})
151150rnmpt 5896 . . 3 ran 𝐻 = {𝑓 ∣ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}}
152151unieqi 4865 . 2 ran 𝐻 = {𝑓 ∣ ∃𝑎 ∈ ℕ0 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐𝑏) = 0}}
153149, 152eqtr4i 2767 1 𝔸 = ran 𝐻
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  {cab 2713  wne 2940  wral 3061  wrex 3070  {crab 3403  cdif 3895  cun 3896  wss 3898  c0 4269  {csn 4573  {cpr 4575   cuni 4852   class class class wbr 5092  cmpt 5175   Or wor 5531  ran crn 5621  wf 6475  cfv 6479  (class class class)co 7337  Fincfn 8804  supcsup 9297  cc 10970  cr 10971  0cc0 10972  *cxr 11109   < clt 11110  cle 11111  0cn0 12334  cz 12420  ...cfz 13340  abscabs 15044  0𝑝c0p 24939  Polycply 25451  coeffccoe 25453  degcdgr 25454  𝔸caa 25580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-er 8569  df-map 8688  df-pm 8689  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-n0 12335  df-z 12421  df-uz 12684  df-rp 12832  df-fz 13341  df-fzo 13484  df-fl 13613  df-seq 13823  df-exp 13884  df-hash 14146  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-clim 15296  df-rlim 15297  df-sum 15497  df-0p 24940  df-ply 25455  df-coe 25457  df-dgr 25458  df-aa 25581
This theorem is referenced by:  aannenlem3  25596
  Copyright terms: Public domain W3C validator