Theorem ply1termlem

Description: Lemma for ply1term . (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Hypothesis	ply1term.1	⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
Assertion	ply1termlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1term.1	⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
2		simplr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
3		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4	2 3	eleqtrdi	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
5		fzss1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑁 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
6	4 5	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑁 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
7		elfz1eq	⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) → 𝑘 = 𝑁 )
8	7	adantl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → 𝑘 = 𝑁 )
9		iftrue	⊢ ( 𝑘 = 𝑁 → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) = 𝐴 )
10	8 9	syl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) = 𝐴 )
11		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ )
12	11	adantr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
13	10 12	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
14		simplr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → 𝑧 ∈ ℂ )
15	2	adantr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
16	8 15	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
17	14 16	expcld	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
18	13 17	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ) → ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
19		eldifn	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 𝑁 ... 𝑁 ) )
20	19	adantl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 𝑁 ... 𝑁 ) )
21	2	adantr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
22	21	nn0zd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → 𝑁 ∈ ℤ )
23		fzsn	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
24	23	eleq2d	⊢ ( 𝑁 ∈ ℤ → ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) ↔ 𝑘 ∈ { 𝑁 } ) )
25		elsn2g	⊢ ( 𝑁 ∈ ℤ → ( 𝑘 ∈ { 𝑁 } ↔ 𝑘 = 𝑁 ) )
26	24 25	bitrd	⊢ ( 𝑁 ∈ ℤ → ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) ↔ 𝑘 = 𝑁 ) )
27	22 26	syl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 𝑁 ... 𝑁 ) ↔ 𝑘 = 𝑁 ) )
28	20 27	mtbid	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ¬ 𝑘 = 𝑁 )
29	28	iffalsed	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) = 0 )
30	29	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
31		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
32		eldifi	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
33		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
34	32 33	syl	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
35		expcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
36	31 34 35	syl2an	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
37	36	mul02d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
38	30 37	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 𝑁 ... 𝑁 ) ) ) → ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
39		fzfid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
40	6 18 38 39	fsumss	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
41	2	nn0zd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℤ )
42	31 2	expcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ 𝑁 ) ∈ ℂ )
43	11 42	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) ∈ ℂ )
44		oveq2	⊢ ( 𝑘 = 𝑁 → ( 𝑧 ↑ 𝑘 ) = ( 𝑧 ↑ 𝑁 ) )
45	9 44	oveq12d	⊢ ( 𝑘 = 𝑁 → ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
46	45	fsum1	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
47	41 43 46	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
48	40 47	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
49	48	mpteq2dva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) ) )
50	1 49	eqtr4id	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) )