Metamath Proof Explorer


Theorem climsubc2

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

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

Proof

Step Hyp Ref Expression
1 climadd.1 𝑍 = ( ℤ𝑀 )
2 climadd.2 ( 𝜑𝑀 ∈ ℤ )
3 climadd.4 ( 𝜑𝐹𝐴 )
4 climaddc1.5 ( 𝜑𝐶 ∈ ℂ )
5 climaddc1.6 ( 𝜑𝐺𝑊 )
6 climaddc1.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
7 climsubc2.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 oveq1d ( ( 𝜑𝑘𝑍 ) → ( ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) − ( 𝐹𝑘 ) ) = ( 𝐶 − ( 𝐹𝑘 ) ) )
20 7 19 eqtr4d ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( ( ( ℤ × { 𝐶 } ) ‘ 𝑘 ) − ( 𝐹𝑘 ) ) )
21 1 2 12 5 3 18 6 20 climsub ( 𝜑𝐺 ⇝ ( 𝐶𝐴 ) )