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 24084

Description: Lemma for aannen 24086. (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 1063	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ ℂ)
2		eldifi 3732	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ℎ ∈ (Poly‘ℤ))
3	2	adantr 481	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ℎ ∈ (Poly‘ℤ))
4	3	3adant2 1080	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ℎ ∈ (Poly‘ℤ))
5		eldifsni 4320	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ℎ ≠ 0_𝑝)
6	5	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ℎ ≠ 0_𝑝)
7		0nn0 11307	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ₀
8		dgrcl 23989	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (Poly‘ℤ) → (deg‘ℎ) ∈ ℕ₀)
9	3, 8	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘ℎ) ∈ ℕ₀)
10		prssi 4353	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℕ₀ ∧ (deg‘ℎ) ∈ ℕ₀) → {0, (deg‘ℎ)} ⊆ ℕ₀)
11	7, 9, 10	sylancr 695	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → {0, (deg‘ℎ)} ⊆ ℕ₀)
12		ssrab2 3687	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ ℕ₀
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ ℕ₀)
14	11, 13	unssd 3789	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℕ₀)
15		nn0ssre 11296	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ ⊆ ℝ
16		ressxr 10083	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ⊆ ℝ^*
17	15, 16	sstri 3612	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ⊆ ℝ^*
18	14, 17	syl6ss 3615	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^*)
19		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘ℎ) ∈ V
20	19	prid2 4298	. . . . . . . . . . . . . . . 16 ⊢ (deg‘ℎ) ∈ {0, (deg‘ℎ)}
21		elun1 3780	. . . . . . . . . . . . . . . 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 12154	. . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
25	18	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^*)
26		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘0))
27		abs0 14025	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘0) = 0
28	26, 27	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) = 0)
29		c0ex 10034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
30	29	prid1 4297	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ {0, (deg‘ℎ)}
31		elun1 3780	. . . . . . . . . . . . . . . . . . . 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 2709	. . . . . . . . . . . . . . . . . 18 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
34	33	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) = 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
35		0z 11388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℤ
36		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (coeff‘ℎ) = (coeff‘ℎ)
37	36	coef2 23987	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘ℎ):ℕ₀⟶ℤ)
38	3, 35, 37	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (coeff‘ℎ):ℕ₀⟶ℤ)
39	38	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → ((coeff‘ℎ)‘𝑒) ∈ ℤ)
40		nn0abscl 14052	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((coeff‘ℎ)‘𝑒) ∈ ℤ → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
42	41	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
43		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ∈ ℕ₀)
44	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (deg‘ℎ) ∈ ℕ₀)
45	3	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ℎ ∈ (Poly‘ℤ))
46		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ((coeff‘ℎ)‘𝑒) ≠ 0)
47		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (deg‘ℎ) = (deg‘ℎ)
48	36, 47	dgrub 23990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ 𝑒 ∈ ℕ₀ ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘ℎ))
49	45, 43, 46, 48	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘ℎ))
50		elfz2nn0 12431	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 ∈ (0...(deg‘ℎ)) ↔ (𝑒 ∈ ℕ₀ ∧ (deg‘ℎ) ∈ ℕ₀ ∧ 𝑒 ≤ (deg‘ℎ)))
51	43, 44, 49, 50	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ∈ (0...(deg‘ℎ)))
52		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))
53		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑒 → ((coeff‘ℎ)‘𝑖) = ((coeff‘ℎ)‘𝑒))
54	53	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑒 → (abs‘((coeff‘ℎ)‘𝑖)) = (abs‘((coeff‘ℎ)‘𝑒)))
55	54	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑒 → ((abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)) ↔ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))))
56	55	rspcev 3309	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ (0...(deg‘ℎ)) ∧ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))) → ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)))
57	51, 52, 56	sylancl 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)))
58		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (abs‘((coeff‘ℎ)‘𝑒)) → (𝑔 = (abs‘((coeff‘ℎ)‘𝑖)) ↔ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
59	58	rexbidv 3052	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (abs‘((coeff‘ℎ)‘𝑒)) → (∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖)) ↔ ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
60	59	elrab 3363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ↔ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀ ∧ ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
61	42, 57, 60	sylanbrc 698	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})
62		elun2 3781	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
63	61, 62	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
64	34, 63	pm2.61dane 2881	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
65		supxrub 12154	. . . . . . . . . . . . . . . 16 ⊢ ((({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^* ∧ (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})) → (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
66	25, 64, 65	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
67	66	ralrimiva 2966	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
68	6, 24, 67	3jca 1242	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
69	68	3adant2 1080	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
70		neeq1 2856	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (𝑑 ≠ 0_𝑝 ↔ ℎ ≠ 0_𝑝))
71		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → (deg‘𝑑) = (deg‘ℎ))
72	71	breq1d 4663	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → ((deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
73		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = ℎ → (coeff‘𝑑) = (coeff‘ℎ))
74	73	fveq1d 6193	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ℎ → ((coeff‘𝑑)‘𝑒) = ((coeff‘ℎ)‘𝑒))
75	74	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒)))
76	75	breq1d 4663	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
77	76	ralbidv 2986	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
78	70, 72, 77	3anbi123d 1399	. . . . . . . . . . . . 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‘ℎ)‘𝑖))}), ℝ^, < ))))
79	78	elrab 3363	. . . . . . . . . . . 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‘ℎ)‘𝑖))}), ℝ^, < ))))
80	4, 69, 79	sylanbrc 698	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))})
81		simp2 1062	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (ℎ‘𝑔) = 0)
82		fveq1 6190	. . . . . . . . . . . . 13 ⊢ (𝑐 = ℎ → (𝑐‘𝑔) = (ℎ‘𝑔))
83	82	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑐 = ℎ → ((𝑐‘𝑔) = 0 ↔ (ℎ‘𝑔) = 0))
84	83	rspcev 3309	. . . . . . . . . . 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)
85	80, 81, 84	syl2anc 693	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑔) = 0)
86		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑔 → (𝑐‘𝑏) = (𝑐‘𝑔))
87	86	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑔 → ((𝑐‘𝑏) = 0 ↔ (𝑐‘𝑔) = 0))
88	87	rexbidv 3052	. . . . . . . . . . 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))
89	88	elrab 3363	. . . . . . . . . 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))
90	1, 85, 89	sylanbrc 698	. . . . . . . . 9 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0})
91		prfi 8235	. . . . . . . . . . . . . . 15 ⊢ {0, (deg‘ℎ)} ∈ Fin
92		fzfi 12771	. . . . . . . . . . . . . . . . 17 ⊢ (0...(deg‘ℎ)) ∈ Fin
93		abrexfi 8266	. . . . . . . . . . . . . . . . 17 ⊢ ((0...(deg‘ℎ)) ∈ Fin → {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin)
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin
95		rabssab 3690	. . . . . . . . . . . . . . . 16 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}
96		ssfi 8180	. . . . . . . . . . . . . . . 16 ⊢ (({𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin ∧ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) → {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin)
97	94, 95, 96	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin
98		unfi 8227	. . . . . . . . . . . . . . 15 ⊢ (({0, (deg‘ℎ)} ∈ Fin ∧ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin)
99	91, 97, 98	mp2an 708	. . . . . . . . . . . . . 14 ⊢ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin
100	99	a1i 11	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin)
101	22	ne0ii 3923	. . . . . . . . . . . . . 14 ⊢ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅
102	101	a1i 11	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅)
103		xrltso 11974	. . . . . . . . . . . . . 14 ⊢ < Or ℝ^*
104		fisupcl 8375	. . . . . . . . . . . . . 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‘ℎ)‘𝑖))}))
105	103, 104	mpan 706	. . . . . . . . . . . . 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‘ℎ)‘𝑖))}))
106	100, 102, 18, 105	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
107	14, 106	sseldd 3604	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ℕ₀)
108	107	3adant2 1080	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ℕ₀)
109		eqidd 2623	. . . . . . . . . 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})
110		breq2 4657	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
111		breq2 4657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
112	111	ralbidv 2986	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
113	110, 112	3anbi23d 1402	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 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‘ℎ)‘𝑖))}), ℝ^*, < ))))
114	113	rabbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 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‘ℎ)‘𝑖))}), ℝ^*, < ))})
115	114	rexeqdv 3145	. . . . . . . . . . . . 13 ⊢ (𝑎 = 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))
116	115	rabbidv 3189	. . . . . . . . . . . 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})
117	116	eqeq2d 2632	. . . . . . . . . . 11 ⊢ (𝑎 = 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‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (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}))
118	117	rspcev 3309	. . . . . . . . . 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})
119	108, 109, 118	syl2anc 693	. . . . . . . . 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})
120		cnex 10017	. . . . . . . . . . 11 ⊢ ℂ ∈ V
121	120	rabex 4813	. . . . . . . . . 10 ⊢ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} ∈ V
122		eleq2 2690	. . . . . . . . . . 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}))
123		eqeq1 2626	. . . . . . . . . . . 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}))
124	123	rexbidv 3052	. . . . . . . . . . 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}))
125	122, 124	anbi12d 747	. . . . . . . . . 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})))
126	121, 125	spcev 3300	. . . . . . . . 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}))
127	90, 119, 126	syl2anc 693	. . . . . . . 8 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
128	127	3exp 1264	. . . . . . 7 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ((ℎ‘𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))))
129	128	rexlimiv 3027	. . . . . 6 ⊢ (∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})))
130	129	impcom 446	. . . . 5 ⊢ ((𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
131		eleq2 2690	. . . . . . . . 9 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 ↔ 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
132	87	rexbidv 3052	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑔 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0))
133	132	elrab 3363	. . . . . . . . . 10 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} ↔ (𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0))
134		simp1 1061	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎) → ℎ ≠ 0_𝑝)
135	134	anim2i 593	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)) → (ℎ ∈ (Poly‘ℤ) ∧ ℎ ≠ 0_𝑝))
136	71	breq1d 4663	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘ℎ) ≤ 𝑎))
137	75	breq1d 4663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ℎ → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎))
138	137	ralbidv 2986	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎))
139	70, 136, 138	3anbi123d 1399	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → ((𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)))
140	139	elrab 3363	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ↔ (ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)))
141		eldifsn 4317	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ↔ (ℎ ∈ (Poly‘ℤ) ∧ ℎ ≠ 0_𝑝))
142	135, 140, 141	3imtr4i 281	. . . . . . . . . . . . 13 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} → ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
143	142	ssriv 3607	. . . . . . . . . . . 12 ⊢ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝})
144		ssrexv 3667	. . . . . . . . . . . . 13 ⊢ ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃𝑐 ∈ ((Poly‘ℤ) ∖ {0_𝑝})(𝑐‘𝑔) = 0))
145	83	cbvrexv 3172	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ ((Poly‘ℤ) ∖ {0_𝑝})(𝑐‘𝑔) = 0 ↔ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)
146	144, 145	syl6ib 241	. . . . . . . . . . . 12 ⊢ ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
147	143, 146	ax-mp 5	. . . . . . . . . . 11 ⊢ (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)
148	147	anim2i 593	. . . . . . . . . 10 ⊢ ((𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
149	133, 148	sylbi 207	. . . . . . . . 9 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
150	131, 149	syl6bi 243	. . . . . . . 8 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)))
151	150	rexlimivw 3029	. . . . . . 7 ⊢ (∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)))
152	151	impcom 446	. . . . . 6 ⊢ ((𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
153	152	exlimiv 1858	. . . . 5 ⊢ (∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
154	130, 153	impbii 199	. . . 4 ⊢ ((𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0) ↔ ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
155		elaa 24071	. . . 4 ⊢ (𝑔 ∈ 𝔸 ↔ (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
156		eluniab 4447	. . . 4 ⊢ (𝑔 ∈ ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}} ↔ ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
157	154, 155, 156	3bitr4i 292	. . 3 ⊢ (𝑔 ∈ 𝔸 ↔ 𝑔 ∈ ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}})
158	157	eqriv 2619	. 2 ⊢ 𝔸 = ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
159		aannenlem.a	. . . 4 ⊢ 𝐻 = (𝑎 ∈ ℕ₀ ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})
160	159	rnmpt 5371	. . 3 ⊢ ran 𝐻 = {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
161	160	unieqi 4445	. 2 ⊢ ∪ ran 𝐻 = ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
162	158, 161	eqtr4i 2647	1 ⊢ 𝔸 = ∪ ran 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 {cab 2608 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 ∖ cdif 3571 ∪ cun 3572 ⊆ wss 3574 ∅c0 3915 {csn 4177 {cpr 4179 ∪ cuni 4436 class class class wbr 4653 ↦ cmpt 4729 Or wor 5034 ran crn 5115 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 supcsup 8346 ℂcc 9934 ℝcr 9935 0cc0 9936 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 ℕ₀cn0 11292 ℤcz 11377 ...cfz 12326 abscabs 13974 0_𝑝c0p 23436 Polycply 23940 coeffccoe 23942 degcdgr 23943 𝔸caa 24069

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-0p 23437 df-ply 23944 df-coe 23946 df-dgr 23947 df-aa 24070

This theorem is referenced by: aannenlem3 24085

W3C validator