climshft

Description: A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

		Ref	Expression
	Assertion	climshft	$⊢ (M \in ℤ \land F \in V) \to ((F shift M) ⇝ A \leftrightarrow F ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ f = F \to f shift M = F shift M$
2	1	breq1d	$⊢ f = F \to ((f shift M) ⇝ A \leftrightarrow (F shift M) ⇝ A)$
3		breq1	$⊢ f = F \to (f ⇝ A \leftrightarrow F ⇝ A)$
4	2 3	bibi12d	$⊢ f = F \to (((f shift M) ⇝ A \leftrightarrow f ⇝ A) \leftrightarrow ((F shift M) ⇝ A \leftrightarrow F ⇝ A))$
5	4	imbi2d	$⊢ f = F \to ((M \in ℤ \to ((f shift M) ⇝ A \leftrightarrow f ⇝ A)) \leftrightarrow (M \in ℤ \to ((F shift M) ⇝ A \leftrightarrow F ⇝ A)))$
6		znegcl	$⊢ M \in ℤ \to - M \in ℤ$
7		ovex	$⊢ f shift M \in V$
8	7	climshftlem	$⊢ - M \in ℤ \to ((f shift M) ⇝ A \to ((f shift M) shift -M) ⇝ A)$
9	6 8	syl	$⊢ M \in ℤ \to ((f shift M) ⇝ A \to ((f shift M) shift -M) ⇝ A)$
10		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
11		ovexd	$⊢ M \in ℤ \to (f shift M) shift -M \in V$
12		vex	$⊢ f \in V$
13	12	a1i	$⊢ M \in ℤ \to f \in V$
14		id	$⊢ M \in ℤ \to M \in ℤ$
15		zcn	$⊢ M \in ℤ \to M \in ℂ$
16		eluzelcn	$⊢ k \in ℤ_{\geq M} \to k \in ℂ$
17	12	shftcan1	$⊢ (M \in ℂ \land k \in ℂ) \to ((f shift M) shift -M) (k) = f (k)$
18	15 16 17	syl2an	$⊢ (M \in ℤ \land k \in ℤ_{\geq M}) \to ((f shift M) shift -M) (k) = f (k)$
19	10 11 13 14 18	climeq	$⊢ M \in ℤ \to (((f shift M) shift -M) ⇝ A \leftrightarrow f ⇝ A)$
20	9 19	sylibd	$⊢ M \in ℤ \to ((f shift M) ⇝ A \to f ⇝ A)$
21	12	climshftlem	$⊢ M \in ℤ \to (f ⇝ A \to (f shift M) ⇝ A)$
22	20 21	impbid	$⊢ M \in ℤ \to ((f shift M) ⇝ A \leftrightarrow f ⇝ A)$
23	5 22	vtoclg	$⊢ F \in V \to (M \in ℤ \to ((F shift M) ⇝ A \leftrightarrow F ⇝ A))$
24	23	impcom	$⊢ (M \in ℤ \land F \in V) \to ((F shift M) ⇝ A \leftrightarrow F ⇝ A)$

Metamath Proof Explorer

Theorem climshft

Proof