Metamath Proof Explorer


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 ) · ( 𝑧𝑘 ) ) ) )