aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 24297

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

**Hypothesis**
Ref	Expression
aannenlem.a	⊢ 𝐻 = (𝑎 ∈ ℕ₀ ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (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.

Step	Hyp	Ref	Expression
1		simp3 1161	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ ℂ)
2		eldifi 3931	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ℎ ∈ (Poly‘ℤ))
3	2	adantr 468	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ℎ ∈ (Poly‘ℤ))
4	3	3adant2 1154	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ℎ ∈ (Poly‘ℤ))
5		eldifsni 4512	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ℎ ≠ 0_𝑝)
6	5	adantr 468	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ℎ ≠ 0_𝑝)
7		0nn0 11570	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ₀
8		dgrcl 24202	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (Poly‘ℤ) → (deg‘ℎ) ∈ ℕ₀)
9	3, 8	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘ℎ) ∈ ℕ₀)
10		prssi 4542	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℕ₀ ∧ (deg‘ℎ) ∈ ℕ₀) → {0, (deg‘ℎ)} ⊆ ℕ₀)
11	7, 9, 10	sylancr 577	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → {0, (deg‘ℎ)} ⊆ ℕ₀)
12		ssrab2 3884	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ ℕ₀
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ ℕ₀)
14	11, 13	unssd 3988	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℕ₀)
15		nn0ssre 11559	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ ⊆ ℝ
16		ressxr 10364	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ⊆ ℝ^*
17	15, 16	sstri 3807	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ⊆ ℝ^*
18	14, 17	syl6ss 3810	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^*)
19		fvex 6417	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘ℎ) ∈ V
20	19	prid2 4489	. . . . . . . . . . . . . . . 16 ⊢ (deg‘ℎ) ∈ {0, (deg‘ℎ)}
21		elun1 3979	. . . . . . . . . . . . . . . 16 ⊢ ((deg‘ℎ) ∈ {0, (deg‘ℎ)} → (deg‘ℎ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (deg‘ℎ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})
23		supxrub 12368	. . . . . . . . . . . . . . 15 ⊢ ((({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^* ∧ (deg‘ℎ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})) → (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
24	18, 22, 23	sylancl 576	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
25	18	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^*)
26		fveq2 6404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘0))
27		abs0 14244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘0) = 0
28	26, 27	syl6eq 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) = 0)
29		c0ex 10315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
30	29	prid1 4488	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ {0, (deg‘ℎ)}
31		elun1 3979	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ {0, (deg‘ℎ)} → 0 ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
32	30, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})
33	28, 32	syl6eqel 2893	. . . . . . . . . . . . . . . . . 18 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
34	33	adantl 469	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) = 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
35		0z 11650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℤ
36		eqid 2806	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (coeff‘ℎ) = (coeff‘ℎ)
37	36	coef2 24200	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘ℎ):ℕ₀⟶ℤ)
38	3, 35, 37	sylancl 576	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (coeff‘ℎ):ℕ₀⟶ℤ)
39	38	ffvelrnda 6577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → ((coeff‘ℎ)‘𝑒) ∈ ℤ)
40		nn0abscl 14271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((coeff‘ℎ)‘𝑒) ∈ ℤ → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
42	41	adantr 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
43		simplr 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ∈ ℕ₀)
44	9	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (deg‘ℎ) ∈ ℕ₀)
45	3	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ℎ ∈ (Poly‘ℤ))
46		simpr 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ((coeff‘ℎ)‘𝑒) ≠ 0)
47		eqid 2806	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (deg‘ℎ) = (deg‘ℎ)
48	36, 47	dgrub 24203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ 𝑒 ∈ ℕ₀ ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘ℎ))
49	45, 43, 46, 48	syl3anc 1483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘ℎ))
50		elfz2nn0 12650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 ∈ (0...(deg‘ℎ)) ↔ (𝑒 ∈ ℕ₀ ∧ (deg‘ℎ) ∈ ℕ₀ ∧ 𝑒 ≤ (deg‘ℎ)))
51	43, 44, 49, 50	syl3anbrc 1436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ∈ (0...(deg‘ℎ)))
52		eqid 2806	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))
53		2fveq3 6409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑒 → (abs‘((coeff‘ℎ)‘𝑖)) = (abs‘((coeff‘ℎ)‘𝑒)))
54	53	rspceeqv 3520	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ (0...(deg‘ℎ)) ∧ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))) → ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)))
55	51, 52, 54	sylancl 576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)))
56		eqeq1 2810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (abs‘((coeff‘ℎ)‘𝑒)) → (𝑔 = (abs‘((coeff‘ℎ)‘𝑖)) ↔ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
57	56	rexbidv 3240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (abs‘((coeff‘ℎ)‘𝑒)) → (∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖)) ↔ ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
58	57	elrab 3559	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ↔ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀ ∧ ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
59	42, 55, 58	sylanbrc 574	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})
60		elun2 3980	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
61	59, 60	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
62	34, 61	pm2.61dane 3065	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
63		supxrub 12368	. . . . . . . . . . . . . . . 16 ⊢ ((({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^* ∧ (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})) → (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
64	25, 62, 63	syl2anc 575	. . . . . . . . . . . . . . 15 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
65	64	ralrimiva 3154	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
66	6, 24, 65	3jca 1151	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
67	66	3adant2 1154	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
68		neeq1 3040	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (𝑑 ≠ 0_𝑝 ↔ ℎ ≠ 0_𝑝))
69		fveq2 6404	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → (deg‘𝑑) = (deg‘ℎ))
70	69	breq1d 4854	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → ((deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
71		fveq2 6404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = ℎ → (coeff‘𝑑) = (coeff‘ℎ))
72	71	fveq1d 6406	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ℎ → ((coeff‘𝑑)‘𝑒) = ((coeff‘ℎ)‘𝑒))
73	72	fveq2d 6408	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒)))
74	73	breq1d 4854	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
75	74	ralbidv 3174	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
76	68, 70, 75	3anbi123d 1553	. . . . . . . . . . . . 13 ⊢ (𝑑 = ℎ → ((𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )) ↔ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))))
77	76	elrab 3559	. . . . . . . . . . . 12 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} ↔ (ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))))
78	4, 67, 77	sylanbrc 574	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))})
79		simp2 1160	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (ℎ‘𝑔) = 0)
80		fveq1 6403	. . . . . . . . . . . . 13 ⊢ (𝑐 = ℎ → (𝑐‘𝑔) = (ℎ‘𝑔))
81	80	eqeq1d 2808	. . . . . . . . . . . 12 ⊢ (𝑐 = ℎ → ((𝑐‘𝑔) = 0 ↔ (ℎ‘𝑔) = 0))
82	81	rspcev 3502	. . . . . . . . . . 11 ⊢ ((ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} ∧ (ℎ‘𝑔) = 0) → ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑔) = 0)
83	78, 79, 82	syl2anc 575	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑔) = 0)
84		fveqeq2 6413	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑔 → ((𝑐‘𝑏) = 0 ↔ (𝑐‘𝑔) = 0))
85	84	rexbidv 3240	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑔 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑔) = 0))
86	85	elrab 3559	. . . . . . . . . 10 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} ↔ (𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑔) = 0))
87	1, 83, 86	sylanbrc 574	. . . . . . . . 9 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0})
88		prfi 8470	. . . . . . . . . . . . . . 15 ⊢ {0, (deg‘ℎ)} ∈ Fin
89		fzfi 12991	. . . . . . . . . . . . . . . . 17 ⊢ (0...(deg‘ℎ)) ∈ Fin
90		abrexfi 8501	. . . . . . . . . . . . . . . . 17 ⊢ ((0...(deg‘ℎ)) ∈ Fin → {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin)
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin
92		rabssab 3888	. . . . . . . . . . . . . . . 16 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}
93		ssfi 8415	. . . . . . . . . . . . . . . 16 ⊢ (({𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin ∧ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) → {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin)
94	91, 92, 93	mp2an 675	. . . . . . . . . . . . . . 15 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin
95		unfi 8462	. . . . . . . . . . . . . . 15 ⊢ (({0, (deg‘ℎ)} ∈ Fin ∧ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin)
96	88, 94, 95	mp2an 675	. . . . . . . . . . . . . 14 ⊢ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin
97	96	a1i 11	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin)
98	22	ne0ii 4125	. . . . . . . . . . . . . 14 ⊢ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅
99	98	a1i 11	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅)
100		xrltso 12186	. . . . . . . . . . . . . 14 ⊢ < Or ℝ^*
101		fisupcl 8610	. . . . . . . . . . . . . 14 ⊢ (( < Or ℝ^* ∧ (({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin ∧ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅ ∧ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^)) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
102	100, 101	mpan 673	. . . . . . . . . . . . 13 ⊢ ((({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin ∧ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅ ∧ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
103	97, 99, 18, 102	syl3anc 1483	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
104	14, 103	sseldd 3799	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ℕ₀)
105	104	3adant2 1154	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ℕ₀)
106		eqidd 2807	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0})
107		breq2 4848	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
108		breq2 4848	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
109	108	ralbidv 3174	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
110	107, 109	3anbi23d 1556	. . . . . . . . . . . . . 14 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))))
111	110	rabbidv 3379	. . . . . . . . . . . . 13 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} = {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))})
112	111	rexeqdv 3334	. . . . . . . . . . . 12 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))} (𝑐‘𝑏) = 0))
113	112	rabbidv 3379	. . . . . . . . . . 11 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))} (𝑐‘𝑏) = 0})
114	113	rspceeqv 3520	. . . . . . . . . 10 ⊢ ((sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∈ ℕ₀ ∧ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0}) → ∃𝑎 ∈ ℕ₀ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})
115	105, 106, 114	syl2anc 575	. . . . . . . . 9 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑎 ∈ ℕ₀ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})
116		cnex 10298	. . . . . . . . . . 11 ⊢ ℂ ∈ V
117	116	rabex 5007	. . . . . . . . . 10 ⊢ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} ∈ V
118		eleq2 2874	. . . . . . . . . . 11 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 ↔ 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0}))
119		eqeq1 2810	. . . . . . . . . . . 12 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} → (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} ↔ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
120	119	rexbidv 3240	. . . . . . . . . . 11 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} → (∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} ↔ ∃𝑎 ∈ ℕ₀ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
121	118, 120	anbi12d 618	. . . . . . . . . 10 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} → ((𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) ↔ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} ∧ ∃𝑎 ∈ ℕ₀ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})))
122	117, 121	spcev 3493	. . . . . . . . 9 ⊢ ((𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} ∧ ∃𝑎 ∈ ℕ₀ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
123	87, 115, 122	syl2anc 575	. . . . . . . 8 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
124	123	3exp 1141	. . . . . . 7 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ((ℎ‘𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))))
125	124	rexlimiv 3215	. . . . . 6 ⊢ (∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})))
126	125	impcom 396	. . . . 5 ⊢ ((𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
127		eleq2 2874	. . . . . . . . 9 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 ↔ 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
128	84	rexbidv 3240	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑔 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0))
129	128	elrab 3559	. . . . . . . . . 10 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} ↔ (𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0))
130		simp1 1159	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎) → ℎ ≠ 0_𝑝)
131	130	anim2i 605	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)) → (ℎ ∈ (Poly‘ℤ) ∧ ℎ ≠ 0_𝑝))
132	69	breq1d 4854	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘ℎ) ≤ 𝑎))
133	73	breq1d 4854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ℎ → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎))
134	133	ralbidv 3174	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎))
135	68, 132, 134	3anbi123d 1553	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → ((𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)))
136	135	elrab 3559	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ↔ (ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)))
137		eldifsn 4508	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ↔ (ℎ ∈ (Poly‘ℤ) ∧ ℎ ≠ 0_𝑝))
138	131, 136, 137	3imtr4i 283	. . . . . . . . . . . . 13 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} → ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
139	138	ssriv 3802	. . . . . . . . . . . 12 ⊢ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝})
140		ssrexv 3864	. . . . . . . . . . . . 13 ⊢ ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃𝑐 ∈ ((Poly‘ℤ) ∖ {0_𝑝})(𝑐‘𝑔) = 0))
141	81	cbvrexv 3361	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ ((Poly‘ℤ) ∖ {0_𝑝})(𝑐‘𝑔) = 0 ↔ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)
142	140, 141	syl6ib 242	. . . . . . . . . . . 12 ⊢ ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
143	139, 142	ax-mp 5	. . . . . . . . . . 11 ⊢ (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)
144	143	anim2i 605	. . . . . . . . . 10 ⊢ ((𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
145	129, 144	sylbi 208	. . . . . . . . 9 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
146	127, 145	syl6bi 244	. . . . . . . 8 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)))
147	146	rexlimivw 3217	. . . . . . 7 ⊢ (∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)))
148	147	impcom 396	. . . . . 6 ⊢ ((𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
149	148	exlimiv 2021	. . . . 5 ⊢ (∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
150	126, 149	impbii 200	. . . 4 ⊢ ((𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0) ↔ ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
151		elaa 24284	. . . 4 ⊢ (𝑔 ∈ 𝔸 ↔ (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
152		eluniab 4641	. . . 4 ⊢ (𝑔 ∈ ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}} ↔ ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
153	150, 151, 152	3bitr4i 294	. . 3 ⊢ (𝑔 ∈ 𝔸 ↔ 𝑔 ∈ ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}})
154	153	eqriv 2803	. 2 ⊢ 𝔸 = ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
155		aannenlem.a	. . . 4 ⊢ 𝐻 = (𝑎 ∈ ℕ₀ ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})
156	155	rnmpt 5572	. . 3 ⊢ ran 𝐻 = {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
157	156	unieqi 4639	. 2 ⊢ ∪ ran 𝐻 = ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
158	154, 157	eqtr4i 2831	1 ⊢ 𝔸 = ∪ ran 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1100 = wceq 1637 ∃wex 1859 ∈ wcel 2156 {cab 2792 ≠ wne 2978 ∀wral 3096 ∃wrex 3097 {crab 3100 ∖ cdif 3766 ∪ cun 3767 ⊆ wss 3769 ∅c0 4116 {csn 4370 {cpr 4372 ∪ cuni 4630 class class class wbr 4844 ↦ cmpt 4923 Or wor 5231 ran crn 5312 ⟶wf 6093 ‘cfv 6097 (class class class)co 6870 Fincfn 8188 supcsup 8581 ℂcc 10215 ℝcr 10216 0cc0 10217 ℝ^*cxr 10354 < clt 10355 ≤ cle 10356 ℕ₀cn0 11555 ℤcz 11639 ...cfz 12545 abscabs 14193 0_𝑝c0p 23649 Polycply 24153 coeffccoe 24155 degcdgr 24156 𝔸caa 24282

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2068 ax-7 2104 ax-8 2158 ax-9 2165 ax-10 2185 ax-11 2201 ax-12 2214 ax-13 2420 ax-ext 2784 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5096 ax-un 7175 ax-inf2 8781 ax-cnex 10273 ax-resscn 10274 ax-1cn 10275 ax-icn 10276 ax-addcl 10277 ax-addrcl 10278 ax-mulcl 10279 ax-mulrcl 10280 ax-mulcom 10281 ax-addass 10282 ax-mulass 10283 ax-distr 10284 ax-i2m1 10285 ax-1ne0 10286 ax-1rid 10287 ax-rnegex 10288 ax-rrecex 10289 ax-cnre 10290 ax-pre-lttri 10291 ax-pre-lttrn 10292 ax-pre-ltadd 10293 ax-pre-mulgt0 10294 ax-pre-sup 10295 ax-addf 10296

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2061 df-eu 2634 df-mo 2635 df-clab 2793 df-cleq 2799 df-clel 2802 df-nfc 2937 df-ne 2979 df-nel 3082 df-ral 3101 df-rex 3102 df-reu 3103 df-rmo 3104 df-rab 3105 df-v 3393 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4117 df-if 4280 df-pw 4353 df-sn 4371 df-pr 4373 df-tp 4375 df-op 4377 df-uni 4631 df-int 4670 df-iun 4714 df-br 4845 df-opab 4907 df-mpt 4924 df-tr 4947 df-id 5219 df-eprel 5224 df-po 5232 df-so 5233 df-fr 5270 df-se 5271 df-we 5272 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-pred 5893 df-ord 5939 df-on 5940 df-lim 5941 df-suc 5942 df-iota 6060 df-fun 6099 df-fn 6100 df-f 6101 df-f1 6102 df-fo 6103 df-f1o 6104 df-fv 6105 df-isom 6106 df-riota 6831 df-ov 6873 df-oprab 6874 df-mpt2 6875 df-of 7123 df-om 7292 df-1st 7394 df-2nd 7395 df-wrecs 7638 df-recs 7700 df-rdg 7738 df-1o 7792 df-oadd 7796 df-er 7975 df-map 8090 df-pm 8091 df-en 8189 df-dom 8190 df-sdom 8191 df-fin 8192 df-sup 8583 df-inf 8584 df-oi 8650 df-card 9044 df-pnf 10357 df-mnf 10358 df-xr 10359 df-ltxr 10360 df-le 10361 df-sub 10549 df-neg 10550 df-div 10966 df-nn 11302 df-2 11360 df-3 11361 df-n0 11556 df-z 11640 df-uz 11901 df-rp 12043 df-fz 12546 df-fzo 12686 df-fl 12813 df-seq 13021 df-exp 13080 df-hash 13334 df-cj 14058 df-re 14059 df-im 14060 df-sqrt 14194 df-abs 14195 df-clim 14438 df-rlim 14439 df-sum 14636 df-0p 23650 df-ply 24157 df-coe 24159 df-dgr 24160 df-aa 24283

This theorem is referenced by: aannenlem3 24298

W3C validator