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 ∈ ℕ → seq 1 + ℕ × A ⁡ N = N ⁢ A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ j = 1 → seq 1 + ℕ × A ⁡ j = seq 1 + ℕ × A ⁡ 1
2 oveq1 ⊢ j = 1 → j ⁢ A = 1 ⁢ A
3 1 2 eqeq12d ⊢ j = 1 → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ seq 1 + ℕ × A ⁡ 1 = 1 ⁢ A
4 3 imbi2d ⊢ j = 1 → A ∈ ℂ → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ A ∈ ℂ → seq 1 + ℕ × A ⁡ 1 = 1 ⁢ A
5 fveq2 ⊢ j = k → seq 1 + ℕ × A ⁡ j = seq 1 + ℕ × A ⁡ k
6 oveq1 ⊢ j = k → j ⁢ A = k ⁢ A
7 5 6 eqeq12d ⊢ j = k → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ seq 1 + ℕ × A ⁡ k = k ⁢ A
8 7 imbi2d ⊢ j = k → A ∈ ℂ → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ A ∈ ℂ → seq 1 + ℕ × A ⁡ k = k ⁢ A
9 fveq2 ⊢ j = k + 1 → seq 1 + ℕ × A ⁡ j = seq 1 + ℕ × A ⁡ k + 1
10 oveq1 ⊢ j = k + 1 → j ⁢ A = k + 1 ⁢ A
11 9 10 eqeq12d ⊢ j = k + 1 → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ seq 1 + ℕ × A ⁡ k + 1 = k + 1 ⁢ A
12 11 imbi2d ⊢ j = k + 1 → A ∈ ℂ → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ A ∈ ℂ → seq 1 + ℕ × A ⁡ k + 1 = k + 1 ⁢ A
13 fveq2 ⊢ j = N → seq 1 + ℕ × A ⁡ j = seq 1 + ℕ × A ⁡ N
14 oveq1 ⊢ j = N → j ⁢ A = N ⁢ A
15 13 14 eqeq12d ⊢ j = N → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ seq 1 + ℕ × A ⁡ N = N ⁢ A
16 15 imbi2d ⊢ j = N → A ∈ ℂ → seq 1 + ℕ × A ⁡ j = j ⁢ A ↔ A ∈ ℂ → seq 1 + ℕ × 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 ∈ ℂ → seq 1 + ℕ × A ⁡ 1 = 1 ⁢ A
24 oveq1 ⊢ seq 1 + ℕ × A ⁡ k = k ⁢ A → seq 1 + ℕ × A ⁡ k + A = k ⁢ A + A
25 seqp1 ⊢ k ∈ ℤ ≥ 1 → seq 1 + ℕ × A ⁡ k + 1 = seq 1 + ℕ × A ⁡ k + ℕ × A ⁡ k + 1
26 nnuz ⊢ ℕ = ℤ ≥ 1
27 25 26 eleq2s ⊢ k ∈ ℕ → seq 1 + ℕ × A ⁡ k + 1 = seq 1 + ℕ × A ⁡ k + ℕ × A ⁡ k + 1
28 27 adantl ⊢ A ∈ ℂ ∧ k ∈ ℕ → seq 1 + ℕ × A ⁡ k + 1 = seq 1 + ℕ × 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 ∈ ℕ → seq 1 + ℕ × A ⁡ k + ℕ × A ⁡ k + 1 = seq 1 + ℕ × A ⁡ k + A
33 28 32 eqtrd ⊢ A ∈ ℂ ∧ k ∈ ℕ → seq 1 + ℕ × A ⁡ k + 1 = seq 1 + ℕ × 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 ∈ ℕ → seq 1 + ℕ × A ⁡ k + 1 = k + 1 ⁢ A ↔ seq 1 + ℕ × A ⁡ k + A = k ⁢ A + A
44 24 43 imbitrrid ⊢ A ∈ ℂ ∧ k ∈ ℕ → seq 1 + ℕ × A ⁡ k = k ⁢ A → seq 1 + ℕ × A ⁡ k + 1 = k + 1 ⁢ A
45 44 expcom ⊢ k ∈ ℕ → A ∈ ℂ → seq 1 + ℕ × A ⁡ k = k ⁢ A → seq 1 + ℕ × A ⁡ k + 1 = k + 1 ⁢ A
46 45 a2d ⊢ k ∈ ℕ → A ∈ ℂ → seq 1 + ℕ × A ⁡ k = k ⁢ A → A ∈ ℂ → seq 1 + ℕ × A ⁡ k + 1 = k + 1 ⁢ A
47 4 8 12 16 23 46 nnind ⊢ N ∈ ℕ → A ∈ ℂ → seq 1 + ℕ × A ⁡ N = N ⁢ A
48 47 impcom ⊢ A ∈ ℂ ∧ N ∈ ℕ → seq 1 + ℕ × A ⁡ N = N ⁢ A