Metamath Proof Explorer

Theorem caubnd

Description: A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005) (Revised by Mario Carneiro, 14-Feb-2014)

Ref Expression
Hypothesis cau3.1 ⊢Z=ℤ≥M
Assertion caubnd ⊢∀k∈ZF⁡k∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∃y∈ℝ∀k∈ZF⁡k<y

Proof

Step Hyp Ref Expression
1 cau3.1 ⊢Z=ℤ≥M
2 abscl ⊢F⁡k∈ℂ→F⁡k∈ℝ
3 2 ralimi ⊢∀k∈ZF⁡k∈ℂ→∀k∈ZF⁡k∈ℝ
4 1 r19.29uz ⊢∀k∈ZF⁡k∈ℂ∧∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x
5 4 ex ⊢∀k∈ZF⁡k∈ℂ→∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x
6 5 ralimdv ⊢∀k∈ZF⁡k∈ℂ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x
7 1 caubnd2 ⊢∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k∈ℂ∧F⁡k−F⁡j<x→∃z∈ℝ∃j∈Z∀k∈ℤ≥jF⁡k<z
8 6 7 syl6 ⊢∀k∈ZF⁡k∈ℂ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∃z∈ℝ∃j∈Z∀k∈ℤ≥jF⁡k<z
9 fzssuz ⊢M…j⊆ℤ≥M
10 9 1 sseqtrri ⊢M…j⊆Z
11 ssralv ⊢M…j⊆Z→∀k∈ZF⁡k∈ℝ→∀k∈M…jF⁡k∈ℝ
12 10 11 ax-mp ⊢∀k∈ZF⁡k∈ℝ→∀k∈M…jF⁡k∈ℝ
13 fzfi ⊢M…j∈Fin
14 fimaxre3 ⊢M…j∈Fin∧∀k∈M…jF⁡k∈ℝ→∃x∈ℝ∀k∈M…jF⁡k≤x
15 13 14 mpan ⊢∀k∈M…jF⁡k∈ℝ→∃x∈ℝ∀k∈M…jF⁡k≤x
16 peano2re ⊢x∈ℝ→x+1∈ℝ
17 16 adantl ⊢∀k∈M…jF⁡k∈ℝ∧x∈ℝ→x+1∈ℝ
18 ltp1 ⊢x∈ℝ→x<x+1
19 18 adantl ⊢F⁡k∈ℝ∧x∈ℝ→x<x+1
20 16 adantl ⊢F⁡k∈ℝ∧x∈ℝ→x+1∈ℝ
21 lelttr ⊢F⁡k∈ℝ∧x∈ℝ∧x+1∈ℝ→F⁡k≤x∧x<x+1→F⁡k<x+1
22 20 21 mpd3an3 ⊢F⁡k∈ℝ∧x∈ℝ→F⁡k≤x∧x<x+1→F⁡k<x+1
23 19 22 mpan2d ⊢F⁡k∈ℝ∧x∈ℝ→F⁡k≤x→F⁡k<x+1
24 23 expcom ⊢x∈ℝ→F⁡k∈ℝ→F⁡k≤x→F⁡k<x+1
25 24 ralimdv ⊢x∈ℝ→∀k∈M…jF⁡k∈ℝ→∀k∈M…jF⁡k≤x→F⁡k<x+1
26 25 impcom ⊢∀k∈M…jF⁡k∈ℝ∧x∈ℝ→∀k∈M…jF⁡k≤x→F⁡k<x+1
27 ralim ⊢∀k∈M…jF⁡k≤x→F⁡k<x+1→∀k∈M…jF⁡k≤x→∀k∈M…jF⁡k<x+1
28 26 27 syl ⊢∀k∈M…jF⁡k∈ℝ∧x∈ℝ→∀k∈M…jF⁡k≤x→∀k∈M…jF⁡k<x+1
29 brralrspcev ⊢x+1∈ℝ∧∀k∈M…jF⁡k<x+1→∃w∈ℝ∀k∈M…jF⁡k<w
30 17 28 29 syl6an ⊢∀k∈M…jF⁡k∈ℝ∧x∈ℝ→∀k∈M…jF⁡k≤x→∃w∈ℝ∀k∈M…jF⁡k<w
31 30 rexlimdva ⊢∀k∈M…jF⁡k∈ℝ→∃x∈ℝ∀k∈M…jF⁡k≤x→∃w∈ℝ∀k∈M…jF⁡k<w
32 15 31 mpd ⊢∀k∈M…jF⁡k∈ℝ→∃w∈ℝ∀k∈M…jF⁡k<w
33 12 32 syl ⊢∀k∈ZF⁡k∈ℝ→∃w∈ℝ∀k∈M…jF⁡k<w
34 max1 ⊢w∈ℝ∧z∈ℝ→w≤ifw≤zzw
35 34 3adant3 ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→w≤ifw≤zzw
36 simp3 ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→F⁡k∈ℝ
37 simp1 ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→w∈ℝ
38 ifcl ⊢z∈ℝ∧w∈ℝ→ifw≤zzw∈ℝ
39 38 ancoms ⊢w∈ℝ∧z∈ℝ→ifw≤zzw∈ℝ
40 39 3adant3 ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→ifw≤zzw∈ℝ
41 ltletr ⊢F⁡k∈ℝ∧w∈ℝ∧ifw≤zzw∈ℝ→F⁡k<w∧w≤ifw≤zzw→F⁡k<ifw≤zzw
42 36 37 40 41 syl3anc ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→F⁡k<w∧w≤ifw≤zzw→F⁡k<ifw≤zzw
43 35 42 mpan2d ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→F⁡k<w→F⁡k<ifw≤zzw
44 max2 ⊢w∈ℝ∧z∈ℝ→z≤ifw≤zzw
45 44 3adant3 ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→z≤ifw≤zzw
46 simp2 ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→z∈ℝ
47 ltletr ⊢F⁡k∈ℝ∧z∈ℝ∧ifw≤zzw∈ℝ→F⁡k<z∧z≤ifw≤zzw→F⁡k<ifw≤zzw
48 36 46 40 47 syl3anc ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→F⁡k<z∧z≤ifw≤zzw→F⁡k<ifw≤zzw
49 45 48 mpan2d ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→F⁡k<z→F⁡k<ifw≤zzw
50 43 49 jaod ⊢w∈ℝ∧z∈ℝ∧F⁡k∈ℝ→F⁡k<w∨F⁡k<z→F⁡k<ifw≤zzw
51 50 3expia ⊢w∈ℝ∧z∈ℝ→F⁡k∈ℝ→F⁡k<w∨F⁡k<z→F⁡k<ifw≤zzw
52 51 ralimdv ⊢w∈ℝ∧z∈ℝ→∀k∈ZF⁡k∈ℝ→∀k∈ZF⁡k<w∨F⁡k<z→F⁡k<ifw≤zzw
53 ralim ⊢∀k∈ZF⁡k<w∨F⁡k<z→F⁡k<ifw≤zzw→∀k∈ZF⁡k<w∨F⁡k<z→∀k∈ZF⁡k<ifw≤zzw
54 52 53 syl6 ⊢w∈ℝ∧z∈ℝ→∀k∈ZF⁡k∈ℝ→∀k∈ZF⁡k<w∨F⁡k<z→∀k∈ZF⁡k<ifw≤zzw
55 brralrspcev ⊢ifw≤zzw∈ℝ∧∀k∈ZF⁡k<ifw≤zzw→∃y∈ℝ∀k∈ZF⁡k<y
56 55 ex ⊢ifw≤zzw∈ℝ→∀k∈ZF⁡k<ifw≤zzw→∃y∈ℝ∀k∈ZF⁡k<y
57 39 56 syl ⊢w∈ℝ∧z∈ℝ→∀k∈ZF⁡k<ifw≤zzw→∃y∈ℝ∀k∈ZF⁡k<y
58 54 57 syl6d ⊢w∈ℝ∧z∈ℝ→∀k∈ZF⁡k∈ℝ→∀k∈ZF⁡k<w∨F⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
59 uzssz ⊢ℤ≥M⊆ℤ
60 1 59 eqsstri ⊢Z⊆ℤ
61 60 sseli ⊢k∈Z→k∈ℤ
62 60 sseli ⊢j∈Z→j∈ℤ
63 uztric ⊢k∈ℤ∧j∈ℤ→j∈ℤ≥k∨k∈ℤ≥j
64 61 62 63 syl2anr ⊢j∈Z∧k∈Z→j∈ℤ≥k∨k∈ℤ≥j
65 simpr ⊢j∈Z∧k∈Z→k∈Z
66 65 1 eleqtrdi ⊢j∈Z∧k∈Z→k∈ℤ≥M
67 elfzuzb ⊢k∈M…j↔k∈ℤ≥M∧j∈ℤ≥k
68 67 baib ⊢k∈ℤ≥M→k∈M…j↔j∈ℤ≥k
69 66 68 syl ⊢j∈Z∧k∈Z→k∈M…j↔j∈ℤ≥k
70 69 orbi1d ⊢j∈Z∧k∈Z→k∈M…j∨k∈ℤ≥j↔j∈ℤ≥k∨k∈ℤ≥j
71 64 70 mpbird ⊢j∈Z∧k∈Z→k∈M…j∨k∈ℤ≥j
72 71 ex ⊢j∈Z→k∈Z→k∈M…j∨k∈ℤ≥j
73 pm3.48 ⊢k∈M…j→F⁡k<w∧k∈ℤ≥j→F⁡k<z→k∈M…j∨k∈ℤ≥j→F⁡k<w∨F⁡k<z
74 72 73 syl9 ⊢j∈Z→k∈M…j→F⁡k<w∧k∈ℤ≥j→F⁡k<z→k∈Z→F⁡k<w∨F⁡k<z
75 74 alimdv ⊢j∈Z→∀kk∈M…j→F⁡k<w∧k∈ℤ≥j→F⁡k<z→∀kk∈Z→F⁡k<w∨F⁡k<z
76 df-ral ⊢∀k∈M…jF⁡k<w↔∀kk∈M…j→F⁡k<w
77 df-ral ⊢∀k∈ℤ≥jF⁡k<z↔∀kk∈ℤ≥j→F⁡k<z
78 76 77 anbi12i ⊢∀k∈M…jF⁡k<w∧∀k∈ℤ≥jF⁡k<z↔∀kk∈M…j→F⁡k<w∧∀kk∈ℤ≥j→F⁡k<z
79 19.26 ⊢∀kk∈M…j→F⁡k<w∧k∈ℤ≥j→F⁡k<z↔∀kk∈M…j→F⁡k<w∧∀kk∈ℤ≥j→F⁡k<z
80 78 79 bitr4i ⊢∀k∈M…jF⁡k<w∧∀k∈ℤ≥jF⁡k<z↔∀kk∈M…j→F⁡k<w∧k∈ℤ≥j→F⁡k<z
81 df-ral ⊢∀k∈ZF⁡k<w∨F⁡k<z↔∀kk∈Z→F⁡k<w∨F⁡k<z
82 75 80 81 3imtr4g ⊢j∈Z→∀k∈M…jF⁡k<w∧∀k∈ℤ≥jF⁡k<z→∀k∈ZF⁡k<w∨F⁡k<z
83 82 3impib ⊢j∈Z∧∀k∈M…jF⁡k<w∧∀k∈ℤ≥jF⁡k<z→∀k∈ZF⁡k<w∨F⁡k<z
84 83 imim1i ⊢∀k∈ZF⁡k<w∨F⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y→j∈Z∧∀k∈M…jF⁡k<w∧∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
85 84 3expd ⊢∀k∈ZF⁡k<w∨F⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y→j∈Z→∀k∈M…jF⁡k<w→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
86 58 85 syl6 ⊢w∈ℝ∧z∈ℝ→∀k∈ZF⁡k∈ℝ→j∈Z→∀k∈M…jF⁡k<w→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
87 86 com23 ⊢w∈ℝ∧z∈ℝ→j∈Z→∀k∈ZF⁡k∈ℝ→∀k∈M…jF⁡k<w→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
88 87 expimpd ⊢w∈ℝ→z∈ℝ∧j∈Z→∀k∈ZF⁡k∈ℝ→∀k∈M…jF⁡k<w→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
89 88 com3r ⊢∀k∈ZF⁡k∈ℝ→w∈ℝ→z∈ℝ∧j∈Z→∀k∈M…jF⁡k<w→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
90 89 com34 ⊢∀k∈ZF⁡k∈ℝ→w∈ℝ→∀k∈M…jF⁡k<w→z∈ℝ∧j∈Z→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
91 90 rexlimdv ⊢∀k∈ZF⁡k∈ℝ→∃w∈ℝ∀k∈M…jF⁡k<w→z∈ℝ∧j∈Z→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
92 33 91 mpd ⊢∀k∈ZF⁡k∈ℝ→z∈ℝ∧j∈Z→∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
93 92 rexlimdvv ⊢∀k∈ZF⁡k∈ℝ→∃z∈ℝ∃j∈Z∀k∈ℤ≥jF⁡k<z→∃y∈ℝ∀k∈ZF⁡k<y
94 3 8 93 sylsyld ⊢∀k∈ZF⁡k∈ℂ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∃y∈ℝ∀k∈ZF⁡k<y
95 94 imp ⊢∀k∈ZF⁡k∈ℂ∧∀x∈ℝ+∃j∈Z∀k∈ℤ≥jF⁡k−F⁡j<x→∃y∈ℝ∀k∈ZF⁡k<y