This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscau

Description: Express the property " F is a Cauchy sequence of metric D ". Part of Definition 1.4-3 of Kreyszig p. 28. The condition F C_ ( CC X. X ) allows to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion iscau ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 caufval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( Cau ‘ 𝐷 ) = { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) } )
2 1 eleq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) } ) )
3 reseq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
4 eqidd ⊢ ( 𝑓 = 𝐹 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑘 ) )
5 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
6 5 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) = ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) )
7 3 4 6 feq123d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ) )
8 7 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ) )
9 8 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ) )
10 9 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) } ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ) )
11 2 10 bitrdi ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )