Metamath Proof Explorer

Theorem climcau

Description: A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of Gleason p. 180 (necessity part). (Contributed by NM, 16-Apr-2005) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypothesis climcau.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion climcau ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )

Proof

Step Hyp Ref Expression
1 climcau.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 df-br ⊢ ( 𝐹 ⇝ 𝑦 ↔ ⟨ 𝐹 , 𝑦 ⟩ ∈ ⇝ )
3 simpll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
4 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
5 4 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
6 eqidd ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
7 simplr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ⇝ 𝑦 )
8 1 3 5 6 7 climi ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) )
9 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
10 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
11 9 10 syl ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
12 11 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
13 12 adantl ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
14 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
15 14 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) )
16 14 fvoveq1d ⊢ ( 𝑘 = 𝑗 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) )
17 16 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) )
18 15 17 anbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) )
19 18 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) )
20 13 19 syl ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) )
21 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
22 21 ad2antlr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑥 ∈ ℝ )
23 simpllr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝐹 ⇝ 𝑦 )
24 climcl ⊢ ( 𝐹 ⇝ 𝑦 → 𝑦 ∈ ℂ )
25 23 24 syl ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑦 ∈ ℂ )
26 simprl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
27 simplrl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
28 simpllr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → 𝑦 ∈ ℂ )
29 simplll ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → 𝑥 ∈ ℝ )
30 simprr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) )
31 28 27 abssubd ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( 𝑦 − ( 𝐹 ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) )
32 simplrr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) )
33 31 32 eqbrtrd ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( 𝑦 − ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) )
34 26 27 28 29 30 33 abs3lemd ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
35 34 ex ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
36 35 ralimdv ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
37 36 ex ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
38 37 com23 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℂ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
39 22 25 38 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
40 20 39 mpdd ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
41 40 reximdva ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑦 ) ) < ( 𝑥 / 2 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
42 8 41 mpd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
43 42 ralrimiva ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ⇝ 𝑦 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
44 43 ex ⊢ ( 𝑀 ∈ ℤ → ( 𝐹 ⇝ 𝑦 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
45 2 44 biimtrrid ⊢ ( 𝑀 ∈ ℤ → ( ⟨ 𝐹 , 𝑦 ⟩ ∈ ⇝ → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
46 45 exlimdv ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑦 ⟨ 𝐹 , 𝑦 ⟩ ∈ ⇝ → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
47 eldm2g ⊢ ( 𝐹 ∈ dom ⇝ → ( 𝐹 ∈ dom ⇝ ↔ ∃ 𝑦 ⟨ 𝐹 , 𝑦 ⟩ ∈ ⇝ ) )
48 47 ibi ⊢ ( 𝐹 ∈ dom ⇝ → ∃ 𝑦 ⟨ 𝐹 , 𝑦 ⟩ ∈ ⇝ )
49 46 48 impel ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )