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

Metamath Proof Explorer

Theorem cau3

Description: Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of j in the assertion, so it can be used with rexanuz and friends.) (Contributed by Mario Carneiro, 15-Feb-2014)

Ref Expression
Hypothesis cau3.1 ⊢ Z = ℤ ≥ M
Assertion cau3 ⊢ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ ∀ m ∈ ℤ ≥ k F ⁡ k − F ⁡ m < x

Proof

Step Hyp Ref Expression
1 cau3.1 ⊢ Z = ℤ ≥ M
2 uzssz ⊢ ℤ ≥ M ⊆ ℤ
3 1 2 eqsstri ⊢ Z ⊆ ℤ
4 id ⊢ F ⁡ k ∈ ℂ → F ⁡ k ∈ ℂ
5 eleq1 ⊢ F ⁡ k = F ⁡ j → F ⁡ k ∈ ℂ ↔ F ⁡ j ∈ ℂ
6 eleq1 ⊢ F ⁡ k = F ⁡ m → F ⁡ k ∈ ℂ ↔ F ⁡ m ∈ ℂ
7 abssub ⊢ F ⁡ j ∈ ℂ ∧ F ⁡ k ∈ ℂ → F ⁡ j − F ⁡ k = F ⁡ k − F ⁡ j
8 7 3adant1 ⊢ ⊤ ∧ F ⁡ j ∈ ℂ ∧ F ⁡ k ∈ ℂ → F ⁡ j − F ⁡ k = F ⁡ k − F ⁡ j
9 abssub ⊢ F ⁡ m ∈ ℂ ∧ F ⁡ j ∈ ℂ → F ⁡ m − F ⁡ j = F ⁡ j − F ⁡ m
10 9 3adant1 ⊢ ⊤ ∧ F ⁡ m ∈ ℂ ∧ F ⁡ j ∈ ℂ → F ⁡ m − F ⁡ j = F ⁡ j − F ⁡ m
11 abs3lem ⊢ F ⁡ k ∈ ℂ ∧ F ⁡ m ∈ ℂ ∧ F ⁡ j ∈ ℂ ∧ x ∈ ℝ → F ⁡ k − F ⁡ j < x 2 ∧ F ⁡ j − F ⁡ m < x 2 → F ⁡ k − F ⁡ m < x
12 11 3adant1 ⊢ ⊤ ∧ F ⁡ k ∈ ℂ ∧ F ⁡ m ∈ ℂ ∧ F ⁡ j ∈ ℂ ∧ x ∈ ℝ → F ⁡ k − F ⁡ j < x 2 ∧ F ⁡ j − F ⁡ m < x 2 → F ⁡ k − F ⁡ m < x
13 3 4 5 6 8 10 12 cau3lem ⊢ ⊤ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ ∀ m ∈ ℤ ≥ k F ⁡ k − F ⁡ m < x
14 13 mptru ⊢ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ F ⁡ k − F ⁡ j < x ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k ∈ ℂ ∧ ∀ m ∈ ℤ ≥ k F ⁡ k − F ⁡ m < x