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 ( + , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) = ( 𝑁 · 𝐴 ) )