Metamath Proof Explorer


Theorem climneg

Description: Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climneg.1 𝑘 𝜑
climneg.2 𝑘 𝐹
climneg.3 𝑍 = ( ℤ𝑀 )
climneg.4 ( 𝜑𝑀 ∈ ℤ )
climneg.5 ( 𝜑𝐹𝐴 )
climneg.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
Assertion climneg ( 𝜑 → ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ⇝ - 𝐴 )

Proof

Step Hyp Ref Expression
1 climneg.1 𝑘 𝜑
2 climneg.2 𝑘 𝐹
3 climneg.3 𝑍 = ( ℤ𝑀 )
4 climneg.4 ( 𝜑𝑀 ∈ ℤ )
5 climneg.5 ( 𝜑𝐹𝐴 )
6 climneg.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
7 nfmpt1 𝑘 ( 𝑘𝑍 ↦ - 1 )
8 nfmpt1 𝑘 ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) )
9 3 fvexi 𝑍 ∈ V
10 9 mptex ( 𝑘𝑍 ↦ - 1 ) ∈ V
11 10 a1i ( 𝜑 → ( 𝑘𝑍 ↦ - 1 ) ∈ V )
12 1cnd ( 𝜑 → 1 ∈ ℂ )
13 12 negcld ( 𝜑 → - 1 ∈ ℂ )
14 eqidd ( 𝑗𝑍 → ( 𝑘𝑍 ↦ - 1 ) = ( 𝑘𝑍 ↦ - 1 ) )
15 eqidd ( ( 𝑗𝑍𝑘 = 𝑗 ) → - 1 = - 1 )
16 id ( 𝑗𝑍𝑗𝑍 )
17 1cnd ( 𝑗𝑍 → 1 ∈ ℂ )
18 17 negcld ( 𝑗𝑍 → - 1 ∈ ℂ )
19 14 15 16 18 fvmptd ( 𝑗𝑍 → ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑗 ) = - 1 )
20 19 adantl ( ( 𝜑𝑗𝑍 ) → ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑗 ) = - 1 )
21 3 4 11 13 20 climconst ( 𝜑 → ( 𝑘𝑍 ↦ - 1 ) ⇝ - 1 )
22 9 mptex ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ∈ V
23 22 a1i ( 𝜑 → ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ∈ V )
24 neg1cn - 1 ∈ ℂ
25 eqid ( 𝑘𝑍 ↦ - 1 ) = ( 𝑘𝑍 ↦ - 1 )
26 25 fvmpt2 ( ( 𝑘𝑍 ∧ - 1 ∈ ℂ ) → ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) = - 1 )
27 24 26 mpan2 ( 𝑘𝑍 → ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) = - 1 )
28 27 24 eqeltrdi ( 𝑘𝑍 → ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) ∈ ℂ )
29 28 adantl ( ( 𝜑𝑘𝑍 ) → ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) ∈ ℂ )
30 simpr ( ( 𝜑𝑘𝑍 ) → 𝑘𝑍 )
31 6 negcld ( ( 𝜑𝑘𝑍 ) → - ( 𝐹𝑘 ) ∈ ℂ )
32 eqid ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) = ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) )
33 32 fvmpt2 ( ( 𝑘𝑍 ∧ - ( 𝐹𝑘 ) ∈ ℂ ) → ( ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ‘ 𝑘 ) = - ( 𝐹𝑘 ) )
34 30 31 33 syl2anc ( ( 𝜑𝑘𝑍 ) → ( ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ‘ 𝑘 ) = - ( 𝐹𝑘 ) )
35 6 mulm1d ( ( 𝜑𝑘𝑍 ) → ( - 1 · ( 𝐹𝑘 ) ) = - ( 𝐹𝑘 ) )
36 27 eqcomd ( 𝑘𝑍 → - 1 = ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) )
37 36 adantl ( ( 𝜑𝑘𝑍 ) → - 1 = ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) )
38 37 oveq1d ( ( 𝜑𝑘𝑍 ) → ( - 1 · ( 𝐹𝑘 ) ) = ( ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) · ( 𝐹𝑘 ) ) )
39 34 35 38 3eqtr2d ( ( 𝜑𝑘𝑍 ) → ( ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ‘ 𝑘 ) = ( ( ( 𝑘𝑍 ↦ - 1 ) ‘ 𝑘 ) · ( 𝐹𝑘 ) ) )
40 1 7 2 8 3 4 21 23 5 29 6 39 climmulf ( 𝜑 → ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ⇝ ( - 1 · 𝐴 ) )
41 climcl ( 𝐹𝐴𝐴 ∈ ℂ )
42 5 41 syl ( 𝜑𝐴 ∈ ℂ )
43 42 mulm1d ( 𝜑 → ( - 1 · 𝐴 ) = - 𝐴 )
44 40 43 breqtrd ( 𝜑 → ( 𝑘𝑍 ↦ - ( 𝐹𝑘 ) ) ⇝ - 𝐴 )