Metamath Proof Explorer

Theorem aannenlem2

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

Ref Expression
Hypothesis aannenlem.a ⊢ H = a ∈ ℕ 0 ⟼ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
Assertion aannenlem2 ⊢ 𝔸 = ⋃ ran ⁡ H

Proof

Step Hyp Ref Expression
1 aannenlem.a ⊢ H = a ∈ ℕ 0 ⟼ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
2 fveqeq2 ⊢ b = g → c ⁡ b = 0 ↔ c ⁡ g = 0
3 2 rexbidv ⊢ b = g → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 ↔ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ g = 0
4 simp3 ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → g ∈ ℂ
5 neeq1 ⊢ d = h → d ≠ 0 𝑝 ↔ h ≠ 0 𝑝
6 fveq2 ⊢ d = h → deg ⁡ d = deg ⁡ h
7 6 breq1d ⊢ d = h → deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ↔ deg ⁡ h ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
8 fveq2 ⊢ d = h → coeff ⁡ d = coeff ⁡ h
9 8 fveq1d ⊢ d = h → coeff ⁡ d ⁡ e = coeff ⁡ h ⁡ e
10 9 fveq2d ⊢ d = h → coeff ⁡ d ⁡ e = coeff ⁡ h ⁡ e
11 10 breq1d ⊢ d = h → coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ↔ coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
12 11 ralbidv ⊢ d = h → ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ↔ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
13 5 7 12 3anbi123d ⊢ d = h → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ↔ h ≠ 0 𝑝 ∧ deg ⁡ h ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
14 eldifi ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 → h ∈ Poly ⁡ ℤ
15 14 adantr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → h ∈ Poly ⁡ ℤ
16 15 3adant2 ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → h ∈ Poly ⁡ ℤ
17 eldifsni ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 → h ≠ 0 𝑝
18 17 adantr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → h ≠ 0 𝑝
19 0nn0 ⊢ 0 ∈ ℕ 0
20 dgrcl ⊢ h ∈ Poly ⁡ ℤ → deg ⁡ h ∈ ℕ 0
21 15 20 syl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → deg ⁡ h ∈ ℕ 0
22 prssi ⊢ 0 ∈ ℕ 0 ∧ deg ⁡ h ∈ ℕ 0 → 0 deg ⁡ h ⊆ ℕ 0
23 19 21 22 sylancr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → 0 deg ⁡ h ⊆ ℕ 0
24 ssrab2 ⊢ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℕ 0
25 24 a1i ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℕ 0
26 23 25 unssd ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℕ 0
27 nn0ssre ⊢ ℕ 0 ⊆ ℝ
28 ressxr ⊢ ℝ ⊆ ℝ *
29 27 28 sstri ⊢ ℕ 0 ⊆ ℝ *
30 26 29 sstrdi ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℝ *
31 fvex ⊢ deg ⁡ h ∈ V
32 31 prid2 ⊢ deg ⁡ h ∈ 0 deg ⁡ h
33 elun1 ⊢ deg ⁡ h ∈ 0 deg ⁡ h → deg ⁡ h ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
34 32 33 ax-mp ⊢ deg ⁡ h ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
35 supxrub ⊢ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℝ * ∧ deg ⁡ h ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i → deg ⁡ h ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
36 30 34 35 sylancl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → deg ⁡ h ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
37 30 adantr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 → 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℝ *
38 fveq2 ⊢ coeff ⁡ h ⁡ e = 0 → coeff ⁡ h ⁡ e = 0
39 abs0 ⊢ 0 = 0
40 38 39 eqtrdi ⊢ coeff ⁡ h ⁡ e = 0 → coeff ⁡ h ⁡ e = 0
41 c0ex ⊢ 0 ∈ V
42 41 prid1 ⊢ 0 ∈ 0 deg ⁡ h
43 elun1 ⊢ 0 ∈ 0 deg ⁡ h → 0 ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
44 42 43 ax-mp ⊢ 0 ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
45 40 44 eqeltrdi ⊢ coeff ⁡ h ⁡ e = 0 → coeff ⁡ h ⁡ e ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
46 45 adantl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e = 0 → coeff ⁡ h ⁡ e ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
47 eqeq1 ⊢ g = coeff ⁡ h ⁡ e → g = coeff ⁡ h ⁡ i ↔ coeff ⁡ h ⁡ e = coeff ⁡ h ⁡ i
48 47 rexbidv ⊢ g = coeff ⁡ h ⁡ e → ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ↔ ∃ i ∈ 0 … deg ⁡ h coeff ⁡ h ⁡ e = coeff ⁡ h ⁡ i
49 0z ⊢ 0 ∈ ℤ
50 eqid ⊢ coeff ⁡ h = coeff ⁡ h
51 50 coef2 ⊢ h ∈ Poly ⁡ ℤ ∧ 0 ∈ ℤ → coeff ⁡ h : ℕ 0 ⟶ ℤ
52 15 49 51 sylancl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → coeff ⁡ h : ℕ 0 ⟶ ℤ
53 52 ffvelcdmda ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 → coeff ⁡ h ⁡ e ∈ ℤ
54 nn0abscl ⊢ coeff ⁡ h ⁡ e ∈ ℤ → coeff ⁡ h ⁡ e ∈ ℕ 0
55 53 54 syl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 → coeff ⁡ h ⁡ e ∈ ℕ 0
56 55 adantr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → coeff ⁡ h ⁡ e ∈ ℕ 0
57 simplr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → e ∈ ℕ 0
58 21 ad2antrr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → deg ⁡ h ∈ ℕ 0
59 15 ad2antrr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → h ∈ Poly ⁡ ℤ
60 simpr ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → coeff ⁡ h ⁡ e ≠ 0
61 eqid ⊢ deg ⁡ h = deg ⁡ h
62 50 61 dgrub ⊢ h ∈ Poly ⁡ ℤ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → e ≤ deg ⁡ h
63 59 57 60 62 syl3anc ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → e ≤ deg ⁡ h
64 elfz2nn0 ⊢ e ∈ 0 … deg ⁡ h ↔ e ∈ ℕ 0 ∧ deg ⁡ h ∈ ℕ 0 ∧ e ≤ deg ⁡ h
65 57 58 63 64 syl3anbrc ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → e ∈ 0 … deg ⁡ h
66 eqid ⊢ coeff ⁡ h ⁡ e = coeff ⁡ h ⁡ e
67 2fveq3 ⊢ i = e → coeff ⁡ h ⁡ i = coeff ⁡ h ⁡ e
68 67 rspceeqv ⊢ e ∈ 0 … deg ⁡ h ∧ coeff ⁡ h ⁡ e = coeff ⁡ h ⁡ e → ∃ i ∈ 0 … deg ⁡ h coeff ⁡ h ⁡ e = coeff ⁡ h ⁡ i
69 65 66 68 sylancl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → ∃ i ∈ 0 … deg ⁡ h coeff ⁡ h ⁡ e = coeff ⁡ h ⁡ i
70 48 56 69 elrabd ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → coeff ⁡ h ⁡ e ∈ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
71 elun2 ⊢ coeff ⁡ h ⁡ e ∈ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i → coeff ⁡ h ⁡ e ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
72 70 71 syl ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 ∧ coeff ⁡ h ⁡ e ≠ 0 → coeff ⁡ h ⁡ e ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
73 46 72 pm2.61dane ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 → coeff ⁡ h ⁡ e ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
74 supxrub ⊢ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℝ * ∧ coeff ⁡ h ⁡ e ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i → coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
75 37 73 74 syl2anc ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ ∧ e ∈ ℕ 0 → coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
76 75 ralrimiva ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
77 18 36 76 3jca ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → h ≠ 0 𝑝 ∧ deg ⁡ h ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
78 77 3adant2 ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → h ≠ 0 𝑝 ∧ deg ⁡ h ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
79 13 16 78 elrabd ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → h ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
80 simp2 ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → h ⁡ g = 0
81 fveq1 ⊢ c = h → c ⁡ g = h ⁡ g
82 81 eqeq1d ⊢ c = h → c ⁡ g = 0 ↔ h ⁡ g = 0
83 82 rspcev ⊢ h ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ h ⁡ g = 0 → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ g = 0
84 79 80 83 syl2anc ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ g = 0
85 3 4 84 elrabd ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0
86 prfi ⊢ 0 deg ⁡ h ∈ Fin
87 fzfi ⊢ 0 … deg ⁡ h ∈ Fin
88 abrexfi ⊢ 0 … deg ⁡ h ∈ Fin → g | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin
89 87 88 ax-mp ⊢ g | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin
90 rabssab ⊢ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ g | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
91 ssfi ⊢ g | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin ∧ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ g | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i → g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin
92 89 90 91 mp2an ⊢ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin
93 unfi ⊢ 0 deg ⁡ h ∈ Fin ∧ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin → 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin
94 86 92 93 mp2an ⊢ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin
95 34 ne0ii ⊢ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ≠ ∅
96 xrltso ⊢ < Or ℝ *
97 fisupcl ⊢ < Or ℝ * ∧ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin ∧ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ≠ ∅ ∧ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℝ * → sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
98 96 97 mpan ⊢ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ∈ Fin ∧ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ≠ ∅ ∧ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ⊆ ℝ * → sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
99 94 95 30 98 mp3an12i ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∈ 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i
100 26 99 sseldd ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ g ∈ ℂ → sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∈ ℕ 0
101 100 3adant2 ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∈ ℕ 0
102 eqidd ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0
103 breq2 ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → deg ⁡ d ≤ a ↔ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
104 breq2 ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → coeff ⁡ d ⁡ e ≤ a ↔ coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
105 104 ralbidv ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
106 103 105 3anbi23d ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
107 106 rabbidv ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a = d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * <
108 107 rexeqdv ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0
109 108 rabbidv ⊢ a = sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < → b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0
110 109 rspceeqv ⊢ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∈ ℕ 0 ∧ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 → ∃ a ∈ ℕ 0 b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
111 101 102 110 syl2anc ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → ∃ a ∈ ℕ 0 b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
112 cnex ⊢ ℂ ∈ V
113 112 rabex ⊢ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 ∈ V
114 eleq2 ⊢ f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 → g ∈ f ↔ g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0
115 eqeq1 ⊢ f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 → f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
116 115 rexbidv ⊢ f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 → ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ ∃ a ∈ ℕ 0 b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
117 114 116 anbi12d ⊢ f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 → g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 ∧ ∃ a ∈ ℕ 0 b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
118 113 117 spcev ⊢ g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 ∧ ∃ a ∈ ℕ 0 b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ sup 0 deg ⁡ h ∪ g ∈ ℕ 0 | ∃ i ∈ 0 … deg ⁡ h g = coeff ⁡ h ⁡ i ℝ * < c ⁡ b = 0 = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
119 85 111 118 syl2anc ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ∧ h ⁡ g = 0 ∧ g ∈ ℂ → ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
120 119 3exp ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 → h ⁡ g = 0 → g ∈ ℂ → ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
121 120 rexlimiv ⊢ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0 → g ∈ ℂ → ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
122 121 impcom ⊢ g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0 → ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
123 eleq2 ⊢ f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → g ∈ f ↔ g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
124 2 rexbidv ⊢ b = g → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ g = 0
125 124 elrab ⊢ g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ g ∈ ℂ ∧ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ g = 0
126 simp1 ⊢ h ≠ 0 𝑝 ∧ deg ⁡ h ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ a → h ≠ 0 𝑝
127 126 anim2i ⊢ h ∈ Poly ⁡ ℤ ∧ h ≠ 0 𝑝 ∧ deg ⁡ h ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ a → h ∈ Poly ⁡ ℤ ∧ h ≠ 0 𝑝
128 6 breq1d ⊢ d = h → deg ⁡ d ≤ a ↔ deg ⁡ h ≤ a
129 10 breq1d ⊢ d = h → coeff ⁡ d ⁡ e ≤ a ↔ coeff ⁡ h ⁡ e ≤ a
130 129 ralbidv ⊢ d = h → ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ a
131 5 128 130 3anbi123d ⊢ d = h → d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ h ≠ 0 𝑝 ∧ deg ⁡ h ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ a
132 131 elrab ⊢ h ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ↔ h ∈ Poly ⁡ ℤ ∧ h ≠ 0 𝑝 ∧ deg ⁡ h ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ h ⁡ e ≤ a
133 eldifsn ⊢ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 ↔ h ∈ Poly ⁡ ℤ ∧ h ≠ 0 𝑝
134 127 132 133 3imtr4i ⊢ h ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a → h ∈ Poly ⁡ ℤ ∖ 0 𝑝
135 134 ssriv ⊢ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ⊆ Poly ⁡ ℤ ∖ 0 𝑝
136 ssrexv ⊢ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ⊆ Poly ⁡ ℤ ∖ 0 𝑝 → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ g = 0 → ∃ c ∈ Poly ⁡ ℤ ∖ 0 𝑝 c ⁡ g = 0
137 82 cbvrexvw ⊢ ∃ c ∈ Poly ⁡ ℤ ∖ 0 𝑝 c ⁡ g = 0 ↔ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
138 136 137 imbitrdi ⊢ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a ⊆ Poly ⁡ ℤ ∖ 0 𝑝 → ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ g = 0 → ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
139 135 138 ax-mp ⊢ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ g = 0 → ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
140 139 anim2i ⊢ g ∈ ℂ ∧ ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ g = 0 → g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
141 125 140 sylbi ⊢ g ∈ b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
142 123 141 biimtrdi ⊢ f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → g ∈ f → g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
143 142 rexlimivw ⊢ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → g ∈ f → g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
144 143 impcom ⊢ g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
145 144 exlimiv ⊢ ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 → g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
146 122 145 impbii ⊢ g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0 ↔ ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
147 elaa ⊢ g ∈ 𝔸 ↔ g ∈ ℂ ∧ ∃ h ∈ Poly ⁡ ℤ ∖ 0 𝑝 h ⁡ g = 0
148 eluniab ⊢ g ∈ ⋃ f | ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0 ↔ ∃ f g ∈ f ∧ ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
149 146 147 148 3bitr4i ⊢ g ∈ 𝔸 ↔ g ∈ ⋃ f | ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
150 149 eqriv ⊢ 𝔸 = ⋃ f | ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
151 1 rnmpt ⊢ ran ⁡ H = f | ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
152 151 unieqi ⊢ ⋃ ran ⁡ H = ⋃ f | ∃ a ∈ ℕ 0 f = b ∈ ℂ | ∃ c ∈ d ∈ Poly ⁡ ℤ | d ≠ 0 𝑝 ∧ deg ⁡ d ≤ a ∧ ∀ e ∈ ℕ 0 coeff ⁡ d ⁡ e ≤ a c ⁡ b = 0
153 150 152 eqtr4i ⊢ 𝔸 = ⋃ ran ⁡ H