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 ⊢Ⅎkφ
climneg.2 ⊢Ⅎ_kF
climneg.3 ⊢Z=ℤ≥M
climneg.4 ⊢φ→M∈ℤ
climneg.5 ⊢φ→F⇝A
climneg.6 ⊢φ∧k∈Z→F⁡k∈ℂ
Assertion climneg ⊢φ→k∈Z⟼−F⁡k⇝−A

Proof

Step Hyp Ref Expression
1 climneg.1 ⊢Ⅎkφ
2 climneg.2 ⊢Ⅎ_kF
3 climneg.3 ⊢Z=ℤ≥M
4 climneg.4 ⊢φ→M∈ℤ
5 climneg.5 ⊢φ→F⇝A
6 climneg.6 ⊢φ∧k∈Z→F⁡k∈ℂ
7 nfmpt1 ⊢Ⅎ_kk∈Z⟼−1
8 nfmpt1 ⊢Ⅎ_kk∈Z⟼−F⁡k
9 3 fvexi ⊢Z∈V
10 9 mptex ⊢k∈Z⟼−1∈V
11 10 a1i ⊢φ→k∈Z⟼−1∈V
12 1cnd ⊢φ→1∈ℂ
13 12 negcld ⊢φ→−1∈ℂ
14 eqidd ⊢j∈Z→k∈Z⟼−1=k∈Z⟼−1
15 eqidd ⊢j∈Z∧k=j→−1=−1
16 id ⊢j∈Z→j∈Z
17 1cnd ⊢j∈Z→1∈ℂ
18 17 negcld ⊢j∈Z→−1∈ℂ
19 14 15 16 18 fvmptd ⊢j∈Z→k∈Z⟼−1⁡j=−1
20 19 adantl ⊢φ∧j∈Z→k∈Z⟼−1⁡j=−1
21 3 4 11 13 20 climconst ⊢φ→k∈Z⟼−1⇝-1
22 9 mptex ⊢k∈Z⟼−F⁡k∈V
23 22 a1i ⊢φ→k∈Z⟼−F⁡k∈V
24 neg1cn ⊢−1∈ℂ
25 eqid ⊢k∈Z⟼−1=k∈Z⟼−1
26 25 fvmpt2 ⊢k∈Z∧−1∈ℂ→k∈Z⟼−1⁡k=−1
27 24 26 mpan2 ⊢k∈Z→k∈Z⟼−1⁡k=−1
28 27 24 eqeltrdi ⊢k∈Z→k∈Z⟼−1⁡k∈ℂ
29 28 adantl ⊢φ∧k∈Z→k∈Z⟼−1⁡k∈ℂ
30 simpr ⊢φ∧k∈Z→k∈Z
31 6 negcld ⊢φ∧k∈Z→−F⁡k∈ℂ
32 eqid ⊢k∈Z⟼−F⁡k=k∈Z⟼−F⁡k
33 32 fvmpt2 ⊢k∈Z∧−F⁡k∈ℂ→k∈Z⟼−F⁡k⁡k=−F⁡k
34 30 31 33 syl2anc ⊢φ∧k∈Z→k∈Z⟼−F⁡k⁡k=−F⁡k
35 6 mulm1d ⊢φ∧k∈Z→-1⁢F⁡k=−F⁡k
36 27 eqcomd ⊢k∈Z→−1=k∈Z⟼−1⁡k
37 36 adantl ⊢φ∧k∈Z→−1=k∈Z⟼−1⁡k
38 37 oveq1d ⊢φ∧k∈Z→-1⁢F⁡k=k∈Z⟼−1⁡k⁢F⁡k
39 34 35 38 3eqtr2d ⊢φ∧k∈Z→k∈Z⟼−F⁡k⁡k=k∈Z⟼−1⁡k⁢F⁡k
40 1 7 2 8 3 4 21 23 5 29 6 39 climmulf ⊢φ→k∈Z⟼−F⁡k⇝-1⁢A
41 climcl ⊢F⇝A→A∈ℂ
42 5 41 syl ⊢φ→A∈ℂ
43 42 mulm1d ⊢φ→-1⁢A=−A
44 40 43 breqtrd ⊢φ→k∈Z⟼−F⁡k⇝−A