Metamath Proof Explorer


Theorem climaddc1

Description: Limit of a constant C added to each term of a sequence. (Contributed by NM, 24-Sep-2005) (Revised by Mario Carneiro, 3-Feb-2014)

Ref Expression
Hypotheses climadd.1 𝑍 = ( ℤ𝑀 )
climadd.2 ( 𝜑𝑀 ∈ ℤ )
climadd.4 ( 𝜑𝐹𝐴 )
climaddc1.5 ( 𝜑𝐶 ∈ ℂ )
climaddc1.6 ( 𝜑𝐺𝑊 )
climaddc1.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
climaddc1.h ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( ( 𝐹𝑘 ) + 𝐶 ) )
Assertion climaddc1 ( 𝜑𝐺 ⇝ ( 𝐴 + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 climadd.1 𝑍 = ( ℤ𝑀 )
2 climadd.2 ( 𝜑𝑀 ∈ ℤ )
3 climadd.4 ( 𝜑𝐹𝐴 )
4 climaddc1.5 ( 𝜑𝐶 ∈ ℂ )
5 climaddc1.6 ( 𝜑𝐺𝑊 )
6 climaddc1.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
7 climaddc1.h ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( ( 𝐹𝑘 ) + 𝐶 ) )
8 0z 0 ∈ ℤ
9 uzssz ( ℤ ‘ 0 ) ⊆ ℤ
10 zex ℤ ∈ V
11 9 10 climconst2 ( ( 𝐶 ∈ ℂ ∧ 0 ∈ ℤ ) → ( ℤ × { 𝐶 } ) ⇝ 𝐶 )
12 4 8 11 sylancl ( 𝜑 → ( ℤ × { 𝐶 } ) ⇝ 𝐶 )
13 eluzelz ( 𝑘 ∈ ( ℤ𝑀 ) → 𝑘 ∈ ℤ )
14 13 1 eleq2s ( 𝑘𝑍𝑘 ∈ ℤ )
15 fvconst2g ( ( 𝐶 ∈ ℂ ∧ 𝑘 ∈ ℤ ) → ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) = 𝐶 )
16 4 14 15 syl2an ( ( 𝜑𝑘𝑍 ) → ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) = 𝐶 )
17 4 adantr ( ( 𝜑𝑘𝑍 ) → 𝐶 ∈ ℂ )
18 16 17 eqeltrd ( ( 𝜑𝑘𝑍 ) → ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) ∈ ℂ )
19 16 oveq2d ( ( 𝜑𝑘𝑍 ) → ( ( 𝐹𝑘 ) + ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) ) = ( ( 𝐹𝑘 ) + 𝐶 ) )
20 7 19 eqtr4d ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( ( 𝐹𝑘 ) + ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) ) )
21 1 2 3 5 12 6 18 20 climadd ( 𝜑𝐺 ⇝ ( 𝐴 + 𝐶 ) )