coeeu

Description: Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	coeeu	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
2	1	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
3		elply2	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) ↔ ( ℂ ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ₀ ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
4	3	simprbi	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ∃ 𝑛 ∈ ℕ₀ ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
5		rexcom	⊢ ( ∃ 𝑛 ∈ ℕ₀ ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
6	4 5	sylib	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
7	2 6	syl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
8		0cn	⊢ 0 ∈ ℂ
9		snssi	⊢ ( 0 ∈ ℂ → { 0 } ⊆ ℂ )
10	8 9	ax-mp	⊢ { 0 } ⊆ ℂ
11		ssequn2	⊢ ( { 0 } ⊆ ℂ ↔ ( ℂ ∪ { 0 } ) = ℂ )
12	10 11	mpbi	⊢ ( ℂ ∪ { 0 } ) = ℂ
13	12	oveq1i	⊢ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) = ( ℂ ↑_m ℕ₀ )
14	13	rexeqi	⊢ ( ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
15	7 14	sylib	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
16		reeanv	⊢ ( ∃ 𝑛 ∈ ℕ₀ ∃ 𝑚 ∈ ℕ₀ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
17		simp1l	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
18		simp1rl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) )
19		simp1rr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) )
20		simp2l	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑛 ∈ ℕ₀ )
21		simp2r	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑚 ∈ ℕ₀ )
22		simp3ll	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
23		simp3rl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } )
24		simp3lr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
25		oveq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 ↑ 𝑘 ) = ( 𝑤 ↑ 𝑘 ) )
26	25	oveq2d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
27	26	sumeq2sdv	⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
28		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑎 ‘ 𝑘 ) = ( 𝑎 ‘ 𝑗 ) )
29		oveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑤 ↑ 𝑘 ) = ( 𝑤 ↑ 𝑗 ) )
30	28 29	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
31	30	cbvsumv	⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) )
32	27 31	eqtrdi	⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
33	32	cbvmptv	⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
34	24 33	eqtrdi	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) )
35		simp3rr	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
36	25	oveq2d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
37	36	sumeq2sdv	⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) )
38		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑗 ) )
39	38 29	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
40	39	cbvsumv	⊢ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) )
41	37 40	eqtrdi	⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
42	41	cbvmptv	⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) )
43	35 42	eqtrdi	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) )
44	17 18 19 20 21 22 23 34 43	coeeulem	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ∧ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑎 = 𝑏 )
45	44	3expia	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) ∧ ( 𝑛 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀ ) ) → ( ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
46	45	rexlimdvva	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) → ( ∃ 𝑛 ∈ ℕ₀ ∃ 𝑚 ∈ ℕ₀ ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
47	16 46	syl5bir	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∧ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ) ) → ( ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
48	47	ralrimivva	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∀ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ( ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
49		imaeq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) )
50	49	eqeq1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) )
51		fveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑘 ) )
52	51	oveq1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
53	52	sumeq2sdv	⊢ ( 𝑎 = 𝑏 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
54	53	mpteq2dv	⊢ ( 𝑎 = 𝑏 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
55	54	eqeq2d	⊢ ( 𝑎 = 𝑏 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
56	50 55	anbi12d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
57	56	rexbidv	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
58		fvoveq1	⊢ ( 𝑛 = 𝑚 → ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) )
59	58	imaeq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) )
60	59	eqeq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ) )
61		oveq2	⊢ ( 𝑛 = 𝑚 → ( 0 ... 𝑛 ) = ( 0 ... 𝑚 ) )
62	61	sumeq1d	⊢ ( 𝑛 = 𝑚 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
63	62	mpteq2dv	⊢ ( 𝑛 = 𝑚 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
64	63	eqeq2d	⊢ ( 𝑛 = 𝑚 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
65	60 64	anbi12d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
66	65	cbvrexvw	⊢ ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
67	57 66	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
68	67	reu4	⊢ ( ∃! 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ∃ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∀ 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∀ 𝑏 ∈ ( ℂ ↑_m ℕ₀ ) ( ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑏 “ ( ℤ_≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) )
69	15 48 68	sylanbrc	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑_m ℕ₀ ) ∃ 𝑛 ∈ ℕ₀ ( ( 𝑎 “ ( ℤ_≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )

Metamath Proof Explorer

Theorem coeeu

Proof