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 23888

Description: Lemma for aannen 23890. (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 1056	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → 𝑔 ∈ ℂ)
2		eldifi 3694	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ℎ ∈ (Poly‘ℤ))
3	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ℎ ∈ (Poly‘ℤ))
4	3	3adant2 1073	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ℎ ∈ (Poly‘ℤ))
5		eldifsni 4261	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ℎ ≠ 0_𝑝)
6	5	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ℎ ≠ 0_𝑝)
7		0nn0 11184	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ₀
8		dgrcl 23793	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (Poly‘ℤ) → (deg‘ℎ) ∈ ℕ₀)
9	3, 8	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘ℎ) ∈ ℕ₀)
10		prssi 4293	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℕ₀ ∧ (deg‘ℎ) ∈ ℕ₀) → {0, (deg‘ℎ)} ⊆ ℕ₀)
11	7, 9, 10	sylancr 694	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → {0, (deg‘ℎ)} ⊆ ℕ₀)
12		ssrab2 3650	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ ℕ₀
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ ℕ₀)
14	11, 13	unssd 3751	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℕ₀)
15		nn0ssre 11173	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ ⊆ ℝ
16		ressxr 9962	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ⊆ ℝ^*
17	15, 16	sstri 3577	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ⊆ ℝ^*
18	14, 17	syl6ss 3580	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^*)
19		fvex 6113	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘ℎ) ∈ V
20	19	prid2 4242	. . . . . . . . . . . . . . . 16 ⊢ (deg‘ℎ) ∈ {0, (deg‘ℎ)}
21		elun1 3742	. . . . . . . . . . . . . . . 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 12026	. . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
25	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ⊆ ℝ^*)
26		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘0))
27		abs0 13873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘0) = 0
28	26, 27	syl6eq 2660	. . . . . . . . . . . . . . . . . . 19 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) = 0)
29		c0ex 9913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
30	29	prid1 4241	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ {0, (deg‘ℎ)}
31		elun1 3742	. . . . . . . . . . . . . . . . . . . 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 2696	. . . . . . . . . . . . . . . . . 18 ⊢ (((coeff‘ℎ)‘𝑒) = 0 → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
34	33	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) = 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
35		0z 11265	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℤ
36		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (coeff‘ℎ) = (coeff‘ℎ)
37	36	coef2 23791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘ℎ):ℕ₀⟶ℤ)
38	3, 35, 37	sylancl 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (coeff‘ℎ):ℕ₀⟶ℤ)
39	38	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → ((coeff‘ℎ)‘𝑒) ∈ ℤ)
40		nn0abscl 13900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((coeff‘ℎ)‘𝑒) ∈ ℤ → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
42	41	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀)
43		simplr 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ∈ ℕ₀)
44	9	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (deg‘ℎ) ∈ ℕ₀)
45	3	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ℎ ∈ (Poly‘ℤ))
46		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ((coeff‘ℎ)‘𝑒) ≠ 0)
47		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (deg‘ℎ) = (deg‘ℎ)
48	36, 47	dgrub 23794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ 𝑒 ∈ ℕ₀ ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘ℎ))
49	45, 43, 46, 48	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ≤ (deg‘ℎ))
50		elfz2nn0 12300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 ∈ (0...(deg‘ℎ)) ↔ (𝑒 ∈ ℕ₀ ∧ (deg‘ℎ) ∈ ℕ₀ ∧ 𝑒 ≤ (deg‘ℎ)))
51	43, 44, 49, 50	syl3anbrc 1239	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → 𝑒 ∈ (0...(deg‘ℎ)))
52		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))
53		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑒 → ((coeff‘ℎ)‘𝑖) = ((coeff‘ℎ)‘𝑒))
54	53	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑒 → (abs‘((coeff‘ℎ)‘𝑖)) = (abs‘((coeff‘ℎ)‘𝑒)))
55	54	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑒 → ((abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)) ↔ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))))
56	55	rspcev 3282	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ (0...(deg‘ℎ)) ∧ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒))) → ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)))
57	51, 52, 56	sylancl 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖)))
58		eqeq1 2614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (abs‘((coeff‘ℎ)‘𝑒)) → (𝑔 = (abs‘((coeff‘ℎ)‘𝑖)) ↔ (abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
59	58	rexbidv 3034	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (abs‘((coeff‘ℎ)‘𝑒)) → (∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖)) ↔ ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
60	59	elrab 3331	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ↔ ((abs‘((coeff‘ℎ)‘𝑒)) ∈ ℕ₀ ∧ ∃𝑖 ∈ (0...(deg‘ℎ))(abs‘((coeff‘ℎ)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑖))))
61	42, 57, 60	sylanbrc 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) ∧ ((coeff‘ℎ)‘𝑒) ≠ 0) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))})
62		elun2 3743	. . . . . . . . . . . . . . . . . 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 2869	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
65		supxrub 12026	. . . . . . . . . . . . . . . 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 691	. . . . . . . . . . . . . . 15 ⊢ (((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) ∧ 𝑒 ∈ ℕ₀) → (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
67	66	ralrimiva 2949	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ))
68	6, 24, 67	3jca 1235	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
69	68	3adant2 1073	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
70		neeq1 2844	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (𝑑 ≠ 0_𝑝 ↔ ℎ ≠ 0_𝑝))
71		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → (deg‘𝑑) = (deg‘ℎ))
72	71	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → ((deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ (deg‘ℎ) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
73		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = ℎ → (coeff‘𝑑) = (coeff‘ℎ))
74	73	fveq1d 6105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ℎ → ((coeff‘𝑑)‘𝑒) = ((coeff‘ℎ)‘𝑒))
75	74	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → (abs‘((coeff‘𝑑)‘𝑒)) = (abs‘((coeff‘ℎ)‘𝑒)))
76	75	breq1d 4593	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
77	76	ralbidv 2969	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
78	70, 72, 77	3anbi123d 1391	. . . . . . . . . . . . 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 3331	. . . . . . . . . . . 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 695	. . . . . . . . . . 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 1055	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → (ℎ‘𝑔) = 0)
82		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑐 = ℎ → (𝑐‘𝑔) = (ℎ‘𝑔))
83	82	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑐 = ℎ → ((𝑐‘𝑔) = 0 ↔ (ℎ‘𝑔) = 0))
84	83	rspcev 3282	. . . . . . . . . . 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 691	. . . . . . . . . 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 6103	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑔 → (𝑐‘𝑏) = (𝑐‘𝑔))
87	86	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑔 → ((𝑐‘𝑏) = 0 ↔ (𝑐‘𝑔) = 0))
88	87	rexbidv 3034	. . . . . . . . . . 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 3331	. . . . . . . . . 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 695	. . . . . . . . 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 8120	. . . . . . . . . . . . . . 15 ⊢ {0, (deg‘ℎ)} ∈ Fin
92		fzfi 12633	. . . . . . . . . . . . . . . . 17 ⊢ (0...(deg‘ℎ)) ∈ Fin
93		abrexfi 8149	. . . . . . . . . . . . . . . . 17 ⊢ ((0...(deg‘ℎ)) ∈ Fin → {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin)
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin
95		rabssab 3652	. . . . . . . . . . . . . . . 16 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}
96		ssfi 8065	. . . . . . . . . . . . . . . 16 ⊢ (({𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin ∧ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ⊆ {𝑔 ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) → {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin)
97	94, 95, 96	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin
98		unfi 8112	. . . . . . . . . . . . . . 15 ⊢ (({0, (deg‘ℎ)} ∈ Fin ∧ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))} ∈ Fin) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ∈ Fin)
99	91, 97, 98	mp2an 704	. . . . . . . . . . . . . 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 3882	. . . . . . . . . . . . . 14 ⊢ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅
102	101	a1i 11	. . . . . . . . . . . . 13 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}) ≠ ∅)
103		xrltso 11850	. . . . . . . . . . . . . 14 ⊢ < Or ℝ^*
104		fisupcl 8258	. . . . . . . . . . . . . 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 702	. . . . . . . . . . . . 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 1318	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}))
107	14, 106	sseldd 3569	. . . . . . . . . . 11 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ℕ₀)
108	107	3adant2 1073	. . . . . . . . . 10 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^*, < ) ∈ ℕ₀)
109		eqidd 2611	. . . . . . . . . 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 4587	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
111		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
112	111	ralbidv 2969	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < )))
113	110, 112	3anbi23d 1394	. . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . 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 3122	. . . . . . . . . . . . 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 3164	. . . . . . . . . . . 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 2620	. . . . . . . . . . 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 3282	. . . . . . . . . 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 691	. . . . . . . . 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 9896	. . . . . . . . . . 11 ⊢ ℂ ∈ V
121	120	rabex 4740	. . . . . . . . . 10 ⊢ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ) ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ sup(({0, (deg‘ℎ)} ∪ {𝑔 ∈ ℕ₀ ∣ ∃𝑖 ∈ (0...(deg‘ℎ))𝑔 = (abs‘((coeff‘ℎ)‘𝑖))}), ℝ^, < ))} (𝑐‘𝑏) = 0} ∈ V
122		eleq2 2677	. . . . . . . . . . 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 2614	. . . . . . . . . . . 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 3034	. . . . . . . . . . 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 743	. . . . . . . . . 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 3273	. . . . . . . . 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 691	. . . . . . . 8 ⊢ ((ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ∧ (ℎ‘𝑔) = 0 ∧ 𝑔 ∈ ℂ) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
128	127	3exp 1256	. . . . . . 7 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → ((ℎ‘𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))))
129	128	rexlimiv 3009	. . . . . 6 ⊢ (∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0 → (𝑔 ∈ ℂ → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})))
130	129	impcom 445	. . . . 5 ⊢ ((𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0) → ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
131		eleq2 2677	. . . . . . . . 9 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 ↔ 𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
132	87	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑔 → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0 ↔ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0))
133	132	elrab 3331	. . . . . . . . . 10 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} ↔ (𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0))
134		simp1 1054	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎) → ℎ ≠ 0_𝑝)
135	134	anim2i 591	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)) → (ℎ ∈ (Poly‘ℤ) ∧ ℎ ≠ 0_𝑝))
136	71	breq1d 4593	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → ((deg‘𝑑) ≤ 𝑎 ↔ (deg‘ℎ) ≤ 𝑎))
137	75	breq1d 4593	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ℎ → ((abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎))
138	137	ralbidv 2969	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ℎ → (∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎 ↔ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎))
139	70, 136, 138	3anbi123d 1391	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → ((𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎) ↔ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)))
140	139	elrab 3331	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ↔ (ℎ ∈ (Poly‘ℤ) ∧ (ℎ ≠ 0_𝑝 ∧ (deg‘ℎ) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘ℎ)‘𝑒)) ≤ 𝑎)))
141		eldifsn 4260	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}) ↔ (ℎ ∈ (Poly‘ℤ) ∧ ℎ ≠ 0_𝑝))
142	135, 140, 141	3imtr4i 280	. . . . . . . . . . . . 13 ⊢ (ℎ ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} → ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
143	142	ssriv 3572	. . . . . . . . . . . 12 ⊢ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝})
144		ssrexv 3630	. . . . . . . . . . . . 13 ⊢ ({𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} ⊆ ((Poly‘ℤ) ∖ {0_𝑝}) → (∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0 → ∃𝑐 ∈ ((Poly‘ℤ) ∖ {0_𝑝})(𝑐‘𝑔) = 0))
145	83	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ ((Poly‘ℤ) ∖ {0_𝑝})(𝑐‘𝑔) = 0 ↔ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)
146	144, 145	syl6ib 240	. . . . . . . . . . . 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 591	. . . . . . . . . 10 ⊢ ((𝑔 ∈ ℂ ∧ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑔) = 0) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
149	133, 148	sylbi 206	. . . . . . . . 9 ⊢ (𝑔 ∈ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
150	131, 149	syl6bi 242	. . . . . . . 8 ⊢ (𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)))
151	150	rexlimivw 3011	. . . . . . 7 ⊢ (∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} → (𝑔 ∈ 𝑓 → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0)))
152	151	impcom 445	. . . . . 6 ⊢ ((𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
153	152	exlimiv 1845	. . . . 5 ⊢ (∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) → (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
154	130, 153	impbii 198	. . . 4 ⊢ ((𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0) ↔ ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
155		elaa 23875	. . . 4 ⊢ (𝑔 ∈ 𝔸 ↔ (𝑔 ∈ ℂ ∧ ∃ℎ ∈ ((Poly‘ℤ) ∖ {0_𝑝})(ℎ‘𝑔) = 0))
156		eluniab 4383	. . . 4 ⊢ (𝑔 ∈ ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}} ↔ ∃𝑓(𝑔 ∈ 𝑓 ∧ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}))
157	154, 155, 156	3bitr4i 291	. . 3 ⊢ (𝑔 ∈ 𝔸 ↔ 𝑔 ∈ ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}})
158	157	eqriv 2607	. 2 ⊢ 𝔸 = ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
159		aannenlem.a	. . . 4 ⊢ 𝐻 = (𝑎 ∈ ℕ₀ ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})
160	159	rnmpt 5292	. . 3 ⊢ ran 𝐻 = {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
161	160	unieqi 4381	. 2 ⊢ ∪ ran 𝐻 = ∪ {𝑓 ∣ ∃𝑎 ∈ ℕ₀ 𝑓 = {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}}
162	158, 161	eqtr4i 2635	1 ⊢ 𝔸 = ∪ ran 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ∖ cdif 3537 ∪ cun 3538 ⊆ wss 3540 ∅c0 3874 {csn 4125 {cpr 4127 ∪ cuni 4372 class class class wbr 4583 ↦ cmpt 4643 Or wor 4958 ran crn 5039 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 supcsup 8229 ℂcc 9813 ℝcr 9814 0cc0 9815 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 ℕ₀cn0 11169 ℤcz 11254 ...cfz 12197 abscabs 13822 0_𝑝c0p 23242 Polycply 23744 coeffccoe 23746 degcdgr 23747 𝔸caa 23873

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-rlim 14068 df-sum 14265 df-0p 23243 df-ply 23748 df-coe 23750 df-dgr 23751 df-aa 23874

This theorem is referenced by: aannenlem3 23889

W3C validator