Metamath Proof Explorer

Theorem ser1const

Description: Value of the partial series sum of a constant function. (Contributed by NM, 8-Aug-2005) (Revised by Mario Carneiro, 16-Feb-2014)

Ref Expression
Assertion ser1const ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) = ( 𝑁 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑗 = 1 → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 1 ) )
2 oveq1 ⊢ ( 𝑗 = 1 → ( 𝑗 · 𝐴 ) = ( 1 · 𝐴 ) )
3 1 2 eqeq12d ⊢ ( 𝑗 = 1 → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ↔ ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 1 ) = ( 1 · 𝐴 ) ) )
4 3 imbi2d ⊢ ( 𝑗 = 1 → ( ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ) ↔ ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 1 ) = ( 1 · 𝐴 ) ) ) )
5 fveq2 ⊢ ( 𝑗 = 𝑘 → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) )
6 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 · 𝐴 ) = ( 𝑘 · 𝐴 ) )
7 5 6 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ↔ ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) = ( 𝑘 · 𝐴 ) ) )
8 7 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ) ↔ ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) = ( 𝑘 · 𝐴 ) ) ) )
9 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) )
10 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 · 𝐴 ) = ( ( 𝑘 + 1 ) · 𝐴 ) )
11 9 10 eqeq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ↔ ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 𝐴 ) ) )
12 11 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ) ↔ ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 𝐴 ) ) ) )
13 fveq2 ⊢ ( 𝑗 = 𝑁 → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
14 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 · 𝐴 ) = ( 𝑁 · 𝐴 ) )
15 13 14 eqeq12d ⊢ ( 𝑗 = 𝑁 → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ↔ ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) = ( 𝑁 · 𝐴 ) ) )
16 15 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑗 ) = ( 𝑗 · 𝐴 ) ) ↔ ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) = ( 𝑁 · 𝐴 ) ) ) )
17 1z ⊢ 1 ∈ ℤ
18 1nn ⊢ 1 ∈ ℕ
19 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ 1 ) = 𝐴 )
20 18 19 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( ( ℕ × { 𝐴 } ) ‘ 1 ) = 𝐴 )
21 mullid ⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
22 20 21 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( ℕ × { 𝐴 } ) ‘ 1 ) = ( 1 · 𝐴 ) )
23 17 22 seq1i ⊢ ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 1 ) = ( 1 · 𝐴 ) )
24 oveq1 ⊢ ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) = ( 𝑘 · 𝐴 ) → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + 𝐴 ) = ( ( 𝑘 · 𝐴 ) + 𝐴 ) )
25 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + ( ( ℕ × { 𝐴 } ) ‘ ( 𝑘 + 1 ) ) ) )
26 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
27 25 26 eleq2s ⊢ ( 𝑘 ∈ ℕ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + ( ( ℕ × { 𝐴 } ) ‘ ( 𝑘 + 1 ) ) ) )
28 27 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + ( ( ℕ × { 𝐴 } ) ‘ ( 𝑘 + 1 ) ) ) )
29 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
30 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ ( 𝑘 + 1 ) ) = 𝐴 )
31 29 30 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ ( 𝑘 + 1 ) ) = 𝐴 )
32 31 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + ( ( ℕ × { 𝐴 } ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + 𝐴 ) )
33 28 32 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + 𝐴 ) )
34 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
35 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
36 ax-1cn ⊢ 1 ∈ ℂ
37 adddir ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑘 + 1 ) · 𝐴 ) = ( ( 𝑘 · 𝐴 ) + ( 1 · 𝐴 ) ) )
38 36 37 mp3an2 ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑘 + 1 ) · 𝐴 ) = ( ( 𝑘 · 𝐴 ) + ( 1 · 𝐴 ) ) )
39 34 35 38 syl2anr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) · 𝐴 ) = ( ( 𝑘 · 𝐴 ) + ( 1 · 𝐴 ) ) )
40 21 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( 1 · 𝐴 ) = 𝐴 )
41 40 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · 𝐴 ) + ( 1 · 𝐴 ) ) = ( ( 𝑘 · 𝐴 ) + 𝐴 ) )
42 39 41 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) · 𝐴 ) = ( ( 𝑘 · 𝐴 ) + 𝐴 ) )
43 33 42 eqeq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 𝐴 ) ↔ ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) + 𝐴 ) = ( ( 𝑘 · 𝐴 ) + 𝐴 ) ) )
44 24 43 imbitrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) = ( 𝑘 · 𝐴 ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 𝐴 ) ) )
45 44 expcom ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ∈ ℂ → ( ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) = ( 𝑘 · 𝐴 ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 𝐴 ) ) ) )
46 45 a2d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑘 ) = ( 𝑘 · 𝐴 ) ) → ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 𝐴 ) ) ) )
47 4 8 12 16 23 46 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ℂ → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) = ( 𝑁 · 𝐴 ) ) )
48 47 impcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) = ( 𝑁 · 𝐴 ) )