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	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ - 𝐴 )