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 ⊢A∈ℂ∧N∈ℕ→seq1+ℕ×A⁡N=N⁢A

Proof

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