This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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