Metamath Proof Explorer


Theorem cau4

Description: Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Hypotheses cau3.1 𝑍 = ( ℤ𝑀 )
cau4.2 𝑊 = ( ℤ𝑁 )
Assertion cau4 ( 𝑁𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 cau3.1 𝑍 = ( ℤ𝑀 )
2 cau4.2 𝑊 = ( ℤ𝑁 )
3 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
4 1 rexuz3 ( 𝑀 ∈ ℤ → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
5 3 4 syl ( 𝑁 ∈ ( ℤ𝑀 ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
6 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
7 2 rexuz3 ( 𝑁 ∈ ℤ → ( ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
8 6 7 syl ( 𝑁 ∈ ( ℤ𝑀 ) → ( ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
9 5 8 bitr4d ( 𝑁 ∈ ( ℤ𝑀 ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
10 9 1 eleq2s ( 𝑁𝑍 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
11 10 ralbidv ( 𝑁𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) ) )
12 1 cau3 ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) )
13 2 cau3 ( ∀ 𝑥 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ( ℤ𝑘 ) ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑦 ) ) ) < 𝑥 ) )
14 11 12 13 3bitr4g ( 𝑁𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) )