Metamath Proof Explorer


Theorem dgrlem

Description: Lemma for dgrcl and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypothesis dgrval.1 𝐴 = ( coeff ‘ 𝐹 )
Assertion dgrlem ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )

Proof

Step Hyp Ref Expression
1 dgrval.1 𝐴 = ( coeff ‘ 𝐹 )
2 elply2 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
3 2 simprbi ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
4 simplrr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
5 simpll ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6 plybss ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
7 5 6 syl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑆 ⊆ ℂ )
8 0cnd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 0 ∈ ℂ )
9 8 snssd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → { 0 } ⊆ ℂ )
10 7 9 unssd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
11 cnex ℂ ∈ V
12 ssexg ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
13 10 11 12 sylancl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑆 ∪ { 0 } ) ∈ V )
14 nn0ex 0 ∈ V
15 elmapg ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ↔ 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
16 13 14 15 sylancl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ↔ 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
17 4 16 mpbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
18 simplrl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑛 ∈ ℕ0 )
19 17 10 fssd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 : ℕ0 ⟶ ℂ )
20 simprl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
21 simprr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) )
22 5 18 19 20 21 coeeq ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( coeff ‘ 𝐹 ) = 𝑎 )
23 1 22 eqtr2id ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝐴 )
24 23 feq1d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
25 17 24 mpbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
26 25 ex ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) → ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
27 26 rexlimdvva ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
28 3 27 mpd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
29 nn0ssz 0 ⊆ ℤ
30 ffn ( 𝑎 : ℕ0 ⟶ ℂ → 𝑎 Fn ℕ0 )
31 elpreima ( 𝑎 Fn ℕ0 → ( 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑎𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
32 19 30 31 3syl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑎𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
33 32 biimpa ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∧ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ) → ( 𝑥 ∈ ℕ0 ∧ ( 𝑎𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
34 eldifsni ( ( 𝑎𝑥 ) ∈ ( ℂ ∖ { 0 } ) → ( 𝑎𝑥 ) ≠ 0 )
35 33 34 simpl2im ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∧ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ) → ( 𝑎𝑥 ) ≠ 0 )
36 33 simpld ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∧ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ) → 𝑥 ∈ ℕ0 )
37 plyco0 ( ( 𝑛 ∈ ℕ0𝑎 : ℕ0 ⟶ ℂ ) → ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑎𝑥 ) ≠ 0 → 𝑥𝑛 ) ) )
38 18 19 37 syl2anc ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑎𝑥 ) ≠ 0 → 𝑥𝑛 ) ) )
39 20 38 mpbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ∀ 𝑥 ∈ ℕ0 ( ( 𝑎𝑥 ) ≠ 0 → 𝑥𝑛 ) )
40 39 r19.21bi ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑎𝑥 ) ≠ 0 → 𝑥𝑛 ) )
41 36 40 syldan ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∧ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ) → ( ( 𝑎𝑥 ) ≠ 0 → 𝑥𝑛 ) )
42 35 41 mpd ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ∧ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) ) → 𝑥𝑛 )
43 42 ralrimiva ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ∀ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 )
44 23 cnveqd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝐴 )
45 44 imaeq1d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( 𝑎 “ ( ℂ ∖ { 0 } ) ) = ( 𝐴 “ ( ℂ ∖ { 0 } ) ) )
46 45 raleqdv ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑎 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ↔ ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )
47 43 46 mpbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 )
48 47 ex ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) → ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )
49 48 expr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) → ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) ) )
50 49 rexlimdv ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )
51 50 reximdva ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) → ∃ 𝑛 ∈ ℕ0𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )
52 3 51 mpd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 )
53 ssrexv ( ℕ0 ⊆ ℤ → ( ∃ 𝑛 ∈ ℕ0𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 → ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )
54 29 52 53 mpsyl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 )
55 28 54 jca ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥𝑛 ) )