Metamath Proof Explorer

Theorem 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ 𝑋 )
53 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐺 : 𝑊 ⟶ 𝑋 )
54 53 24 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 )
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 ‘ 𝐷 ) )