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 } ) ) 𝑥 ≤ 𝑛 ) )

Proof

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

Metamath Proof Explorer

Theorem dgrlem

Proof