Theorem climneg

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

	Ref	Expression
Hypotheses	climneg.1	$$⊢Ⅎk\phi$$
	climneg.2	$$⊢\underset{\_}{Ⅎ}kF$$
	climneg.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climneg.4	$$⊢\phi \to M\in \mathbb{Z}$$
	climneg.5	$$⊢\phi \to F⇝A$$
	climneg.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
Assertion	climneg	$$⊢\phi \to \left(k\in Z⟼-F\left(k\right)\right)⇝\left(-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climneg.1	$$⊢Ⅎk\phi$$
2		climneg.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		climneg.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		climneg.4	$$⊢\phi \to M\in \mathbb{Z}$$
5		climneg.5	$$⊢\phi \to F⇝A$$
6		climneg.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
7		nfmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in Z⟼-1\right)$$
8		nfmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in Z⟼-F\left(k\right)\right)$$
9	3	fvexi	$$⊢Z\in \mathrm{V}$$
10	9	mptex	$$⊢\left(k\in Z⟼-1\right)\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to \left(k\in Z⟼-1\right)\in \mathrm{V}$$
12		1cnd	$$⊢\phi \to 1\in ℂ$$
13	12	negcld	$$⊢\phi \to -1\in ℂ$$
14		eqidd	$$⊢j\in Z\to \left(k\in Z⟼-1\right)=\left(k\in Z⟼-1\right)$$
15		eqidd	$$⊢\left(j\in Z\wedge k=j\right)\to -1=-1$$
16		id	$$⊢j\in Z\to j\in Z$$
17		1cnd	$$⊢j\in Z\to 1\in ℂ$$
18	17	negcld	$$⊢j\in Z\to -1\in ℂ$$
19	14 15 16 18	fvmptd	$$⊢j\in Z\to \left(k\in Z⟼-1\right)\left(j\right)=-1$$
20	19	adantl	$$⊢\left(\phi \wedge j\in Z\right)\to \left(k\in Z⟼-1\right)\left(j\right)=-1$$
21	3 4 11 13 20	climconst	$$⊢\phi \to \left(k\in Z⟼-1\right)⇝-1$$
22	9	mptex	$$⊢\left(k\in Z⟼-F\left(k\right)\right)\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to \left(k\in Z⟼-F\left(k\right)\right)\in \mathrm{V}$$
24		neg1cn	$$⊢-1\in ℂ$$
25		eqid	$$⊢\left(k\in Z⟼-1\right)=\left(k\in Z⟼-1\right)$$
26	25	fvmpt2	$$⊢\left(k\in Z\wedge -1\in ℂ\right)\to \left(k\in Z⟼-1\right)\left(k\right)=-1$$
27	24 26	mpan2	$$⊢k\in Z\to \left(k\in Z⟼-1\right)\left(k\right)=-1$$
28	27 24	eqeltrdi	$$⊢k\in Z\to \left(k\in Z⟼-1\right)\left(k\right)\in ℂ$$
29	28	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼-1\right)\left(k\right)\in ℂ$$
30		simpr	$$⊢\left(\phi \wedge k\in Z\right)\to k\in Z$$
31	6	negcld	$$⊢\left(\phi \wedge k\in Z\right)\to -F\left(k\right)\in ℂ$$
32		eqid	$$⊢\left(k\in Z⟼-F\left(k\right)\right)=\left(k\in Z⟼-F\left(k\right)\right)$$
33	32	fvmpt2	$$⊢\left(k\in Z\wedge -F\left(k\right)\in ℂ\right)\to \left(k\in Z⟼-F\left(k\right)\right)\left(k\right)=-F\left(k\right)$$
34	30 31 33	syl2anc	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼-F\left(k\right)\right)\left(k\right)=-F\left(k\right)$$
35	6	mulm1d	$$⊢\left(\phi \wedge k\in Z\right)\to -1F\left(k\right)=-F\left(k\right)$$
36	27	eqcomd	$$⊢k\in Z\to -1=\left(k\in Z⟼-1\right)\left(k\right)$$
37	36	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to -1=\left(k\in Z⟼-1\right)\left(k\right)$$
38	37	oveq1d	$$⊢\left(\phi \wedge k\in Z\right)\to -1F\left(k\right)=\left(k\in Z⟼-1\right)\left(k\right)F\left(k\right)$$
39	34 35 38	3eqtr2d	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼-F\left(k\right)\right)\left(k\right)=\left(k\in Z⟼-1\right)\left(k\right)F\left(k\right)$$
40	1 7 2 8 3 4 21 23 5 29 6 39	climmulf	$$⊢\phi \to \left(k\in Z⟼-F\left(k\right)\right)⇝-1A$$
41		climcl	$$⊢F⇝A\to A\in ℂ$$
42	5 41	syl	$$⊢\phi \to A\in ℂ$$
43	42	mulm1d	$$⊢\phi \to -1A=-A$$
44	40 43	breqtrd	$$⊢\phi \to \left(k\in Z⟼-F\left(k\right)\right)⇝\left(-A\right)$$