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

Metamath Proof Explorer

Theorem hcau

Description: Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hcau ⊢ F ∈ Cauchy ↔ F : ℕ ⟶ ℋ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ f = F → f ⁡ y = F ⁡ y
2 fveq1 ⊢ f = F → f ⁡ z = F ⁡ z
3 1 2 oveq12d ⊢ f = F → f ⁡ y - ℎ f ⁡ z = F ⁡ y - ℎ F ⁡ z
4 3 fveq2d ⊢ f = F → norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z = norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z
5 4 breq1d ⊢ f = F → norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x ↔ norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x
6 5 rexralbidv ⊢ f = F → ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x ↔ ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x
7 6 ralbidv ⊢ f = F → ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x ↔ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x
8 df-hcau ⊢ Cauchy = f ∈ ℋ ℕ | ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x
9 7 8 elrab2 ⊢ F ∈ Cauchy ↔ F ∈ ℋ ℕ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x
10 ax-hilex ⊢ ℋ ∈ V
11 nnex ⊢ ℕ ∈ V
12 10 11 elmap ⊢ F ∈ ℋ ℕ ↔ F : ℕ ⟶ ℋ
13 12 anbi1i ⊢ F ∈ ℋ ℕ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x ↔ F : ℕ ⟶ ℋ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x
14 9 13 bitri ⊢ F ∈ Cauchy ↔ F : ℕ ⟶ ℋ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ y - ℎ F ⁡ z < x