climshftlem

Description: A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013)

		Ref	Expression
	Hypothesis	climshft.1	$⊢ F \in V$
	Assertion	climshftlem	$⊢ M \in ℤ \to (F ⇝ A \to (F shift M) ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		climshft.1	$⊢ F \in V$
2		zaddcl	$⊢ (k \in ℤ \land M \in ℤ) \to k + M \in ℤ$
3	2	ancoms	$⊢ (M \in ℤ \land k \in ℤ) \to k + M \in ℤ$
4		eluzsub	$⊢ (k \in ℤ \land M \in ℤ \land n \in ℤ_{\geq (k + M)}) \to n - M \in ℤ_{\geq k}$
5	4	3com12	$⊢ (M \in ℤ \land k \in ℤ \land n \in ℤ_{\geq (k + M)}) \to n - M \in ℤ_{\geq k}$
6	5	3expa	$⊢ ((M \in ℤ \land k \in ℤ) \land n \in ℤ_{\geq (k + M)}) \to n - M \in ℤ_{\geq k}$
7		fveq2	$⊢ m = n - M \to F (m) = F (n - M)$
8	7	eleq1d	$⊢ m = n - M \to (F (m) \in ℂ \leftrightarrow F (n - M) \in ℂ)$
9	7	fvoveq1d	$⊢ m = n - M \to \|F (m) - A\| = \|F (n - M) - A\|$
10	9	breq1d	$⊢ m = n - M \to (\|F (m) - A\| < x \leftrightarrow \|F (n - M) - A\| < x)$
11	8 10	anbi12d	$⊢ m = n - M \to ((F (m) \in ℂ \land \|F (m) - A\| < x) \leftrightarrow (F (n - M) \in ℂ \land \|F (n - M) - A\| < x))$
12	11	rspcv	$⊢ n - M \in ℤ_{\geq k} \to (\forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to (F (n - M) \in ℂ \land \|F (n - M) - A\| < x))$
13	6 12	syl	$⊢ ((M \in ℤ \land k \in ℤ) \land n \in ℤ_{\geq (k + M)}) \to (\forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to (F (n - M) \in ℂ \land \|F (n - M) - A\| < x))$
14		zcn	$⊢ M \in ℤ \to M \in ℂ$
15		eluzelcn	$⊢ n \in ℤ_{\geq (k + M)} \to n \in ℂ$
16	1	shftval	$⊢ (M \in ℂ \land n \in ℂ) \to (F shift M) (n) = F (n - M)$
17	16	eleq1d	$⊢ (M \in ℂ \land n \in ℂ) \to ((F shift M) (n) \in ℂ \leftrightarrow F (n - M) \in ℂ)$
18	16	fvoveq1d	$⊢ (M \in ℂ \land n \in ℂ) \to \|(F shift M) (n) - A\| = \|F (n - M) - A\|$
19	18	breq1d	$⊢ (M \in ℂ \land n \in ℂ) \to (\|(F shift M) (n) - A\| < x \leftrightarrow \|F (n - M) - A\| < x)$
20	17 19	anbi12d	$⊢ (M \in ℂ \land n \in ℂ) \to (((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x) \leftrightarrow (F (n - M) \in ℂ \land \|F (n - M) - A\| < x))$
21	14 15 20	syl2an	$⊢ (M \in ℤ \land n \in ℤ_{\geq (k + M)}) \to (((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x) \leftrightarrow (F (n - M) \in ℂ \land \|F (n - M) - A\| < x))$
22	21	adantlr	$⊢ ((M \in ℤ \land k \in ℤ) \land n \in ℤ_{\geq (k + M)}) \to (((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x) \leftrightarrow (F (n - M) \in ℂ \land \|F (n - M) - A\| < x))$
23	13 22	sylibrd	$⊢ ((M \in ℤ \land k \in ℤ) \land n \in ℤ_{\geq (k + M)}) \to (\forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x))$
24	23	ralrimdva	$⊢ (M \in ℤ \land k \in ℤ) \to (\forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to \forall n \in ℤ_{\geq (k + M)} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x))$
25		fveq2	$⊢ m = k + M \to ℤ_{\geq m} = ℤ_{\geq (k + M)}$
26	25	raleqdv	$⊢ m = k + M \to (\forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x) \leftrightarrow \forall n \in ℤ_{\geq (k + M)} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x))$
27	26	rspcev	$⊢ (k + M \in ℤ \land \forall n \in ℤ_{\geq (k + M)} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x)) \to \exists m \in ℤ \forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x)$
28	3 24 27	syl6an	$⊢ (M \in ℤ \land k \in ℤ) \to (\forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to \exists m \in ℤ \forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x))$
29	28	rexlimdva	$⊢ M \in ℤ \to (\exists k \in ℤ \forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to \exists m \in ℤ \forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x))$
30	29	ralimdv	$⊢ M \in ℤ \to (\forall x \in ℝ^{+} \exists k \in ℤ \forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x) \to \forall x \in ℝ^{+} \exists m \in ℤ \forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x))$
31	30	anim2d	$⊢ M \in ℤ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists k \in ℤ \forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x)) \to (A \in ℂ \land \forall x \in ℝ^{+} \exists m \in ℤ \forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x)))$
32	1	a1i	$⊢ M \in ℤ \to F \in V$
33		eqidd	$⊢ (M \in ℤ \land m \in ℤ) \to F (m) = F (m)$
34	32 33	clim	$⊢ M \in ℤ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists k \in ℤ \forall m \in ℤ_{\geq k} (F (m) \in ℂ \land \|F (m) - A\| < x)))$
35		ovexd	$⊢ M \in ℤ \to F shift M \in V$
36		eqidd	$⊢ (M \in ℤ \land n \in ℤ) \to (F shift M) (n) = (F shift M) (n)$
37	35 36	clim	$⊢ M \in ℤ \to ((F shift M) ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists m \in ℤ \forall n \in ℤ_{\geq m} ((F shift M) (n) \in ℂ \land \|(F shift M) (n) - A\| < x)))$
38	31 34 37	3imtr4d	$⊢ M \in ℤ \to (F ⇝ A \to (F shift M) ⇝ A)$

Metamath Proof Explorer

Theorem climshftlem

Proof