Metamath Proof Explorer

Theorem aannenlem2

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

Ref Expression
Hypothesis aannenlem.a ⊢ 𝐻 = ( 𝑎 ∈ ℕ0 ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } )
Assertion aannenlem2 𝔸 = ∪ ran 𝐻

Proof

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