caushft

Description: A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	caures.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	caures.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	caures.4	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
	caushft.4	⊢ 𝑊 = ( ℤ_≥ ‘ ( 𝑀 + 𝑁 ) )
	caushft.5	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	caushft.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) )
	caushft.8	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
	caushft.9	⊢ ( 𝜑 → 𝐺 : 𝑊 ⟶ 𝑋 )
Assertion	caushft	⊢ ( 𝜑 → 𝐺 ∈ ( Cau ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		caures.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		caures.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		caures.4	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
4		caushft.4	⊢ 𝑊 = ( ℤ_≥ ‘ ( 𝑀 + 𝑁 ) )
5		caushft.5	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6		caushft.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) )
7		caushft.8	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
8		caushft.9	⊢ ( 𝜑 → 𝐺 : 𝑊 ⟶ 𝑋 )
9		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
10	3 9	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) )
12		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
13		fvoveq1	⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
14	12 13	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ↔ ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) )
15	14	rspccva	⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
16	11 15	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
17	1 10 2 6 16	iscau4	⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑_pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) ) ) )
18	7 17	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ↑_pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) ) )
19	18	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
20	1	eleq2i	⊢ ( 𝑗 ∈ 𝑍 ↔ 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) )
21	20	biimpi	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) )
22		eluzadd	⊢ ( ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑗 + 𝑁 ) ∈ ( ℤ_≥ ‘ ( 𝑀 + 𝑁 ) ) )
23	21 5 22	syl2anr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑗 + 𝑁 ) ∈ ( ℤ_≥ ‘ ( 𝑀 + 𝑁 ) ) )
24	23 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑗 + 𝑁 ) ∈ 𝑊 )
25		simplr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑗 ∈ 𝑍 )
26	25 1	eleqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) )
27		eluzelz	⊢ ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
28	26 27	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑗 ∈ ℤ )
29	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑁 ∈ ℤ )
30		simpr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) )
31		eluzsub	⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝑚 − 𝑁 ) ∈ ( ℤ_≥ ‘ 𝑗 ) )
32	28 29 30 31	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝑚 − 𝑁 ) ∈ ( ℤ_≥ ‘ 𝑗 ) )
33		simp3	⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 )
34	33	ralimi	⊢ ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 )
35		fvoveq1	⊢ ( 𝑘 = ( 𝑚 − 𝑁 ) → ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) = ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) )
36	35	oveq1d	⊢ ( 𝑘 = ( 𝑚 − 𝑁 ) → ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) )
37	36	breq1d	⊢ ( 𝑘 = ( 𝑚 − 𝑁 ) → ( ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ↔ ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
38	37	rspcv	⊢ ( ( 𝑚 − 𝑁 ) ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 → ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
39	32 34 38	syl2im	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
40		eluzelz	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) → 𝑚 ∈ ℤ )
41	40	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ ℤ )
42	41	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ ℂ )
43	5	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
44	43	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑁 ∈ ℂ )
45	42 44	npcand	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝑚 − 𝑁 ) + 𝑁 ) = 𝑚 )
46	45	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) = ( 𝐺 ‘ 𝑚 ) )
47	46	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ 𝑚 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) )
48	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
49	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝐺 : 𝑊 ⟶ 𝑋 )
50	4	uztrn2	⊢ ( ( ( 𝑗 + 𝑁 ) ∈ 𝑊 ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ 𝑊 )
51	24 50	sylan	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ 𝑊 )
52	49 51	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ 𝑋 )
53	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐺 : 𝑊 ⟶ 𝑋 )
54	53 24	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 )
55	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 )
56		metsym	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐺 ‘ 𝑚 ) ∈ 𝑋 ∧ ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑚 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) )
57	48 52 55 56	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝐺 ‘ 𝑚 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) )
58	47 57	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) )
59	58	breq1d	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( ( 𝐺 ‘ ( ( 𝑚 − 𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ↔ ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
60	39 59	sylibd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
61	60	ralrimdva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
62		fveq2	⊢ ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ℤ_≥ ‘ 𝑛 ) = ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) )
63		fveq2	⊢ ( 𝑛 = ( 𝑗 + 𝑁 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
64	63	oveq1d	⊢ ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) )
65	64	breq1d	⊢ ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ↔ ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
66	62 65	raleqbidv	⊢ ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
67	66	rspcev	⊢ ( ( ( 𝑗 + 𝑁 ) ∈ 𝑊 ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ ( 𝑗 + 𝑁 ) ) ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑊 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 )
68	24 61 67	syl6an	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑊 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
69	68	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑊 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
70	69	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑛 ∈ 𝑊 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
71	19 70	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑛 ∈ 𝑊 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 )
72	2 5	zaddcld	⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℤ )
73		eqidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
74		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
75	4 10 72 73 74 8	iscauf	⊢ ( 𝜑 → ( 𝐺 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑛 ∈ 𝑊 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 𝐺 ‘ 𝑛 ) 𝐷 ( 𝐺 ‘ 𝑚 ) ) < 𝑥 ) )
76	71 75	mpbird	⊢ ( 𝜑 → 𝐺 ∈ ( Cau ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem caushft

Proof