MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  caubnd Structured version   Visualization version   GIF version

Theorem caubnd 14954
Description: A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 14-Feb-2014.)
Hypothesis
Ref Expression
cau3.1 𝑍 = (ℤ𝑀)
Assertion
Ref Expression
caubnd ((∀𝑘𝑍 (𝐹𝑘) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)
Distinct variable groups:   𝑗,𝑘,𝑥,𝑦,𝐹   𝑗,𝑀,𝑘,𝑥   𝑗,𝑍,𝑘,𝑥,𝑦
Allowed substitution hint:   𝑀(𝑦)

Proof of Theorem caubnd
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 abscl 14874 . . . 4 ((𝐹𝑘) ∈ ℂ → (abs‘(𝐹𝑘)) ∈ ℝ)
21ralimi 3087 . . 3 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → ∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ)
3 cau3.1 . . . . . . 7 𝑍 = (ℤ𝑀)
43r19.29uz 14946 . . . . . 6 ((∀𝑘𝑍 (𝐹𝑘) ∈ ℂ ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥))
54ex 416 . . . . 5 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥)))
65ralimdv 3104 . . . 4 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥)))
73caubnd2 14953 . . . 4 (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥) → ∃𝑧 ∈ ℝ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧)
86, 7syl6 35 . . 3 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥 → ∃𝑧 ∈ ℝ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧))
9 fzssuz 13182 . . . . . . . 8 (𝑀...𝑗) ⊆ (ℤ𝑀)
109, 3sseqtrri 3954 . . . . . . 7 (𝑀...𝑗) ⊆ 𝑍
11 ssralv 3983 . . . . . . 7 ((𝑀...𝑗) ⊆ 𝑍 → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ))
1210, 11ax-mp 5 . . . . . 6 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ)
13 fzfi 13576 . . . . . . . 8 (𝑀...𝑗) ∈ Fin
14 fimaxre3 11807 . . . . . . . 8 (((𝑀...𝑗) ∈ Fin ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ≤ 𝑥)
1513, 14mpan 690 . . . . . . 7 (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ≤ 𝑥)
16 peano2re 11034 . . . . . . . . . 10 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
1716adantl 485 . . . . . . . . 9 ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ)
18 ltp1 11701 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1))
1918adantl 485 . . . . . . . . . . . . . 14 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → 𝑥 < (𝑥 + 1))
2016adantl 485 . . . . . . . . . . . . . . 15 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ)
21 lelttr 10952 . . . . . . . . . . . . . . 15 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) → (((abs‘(𝐹𝑘)) ≤ 𝑥𝑥 < (𝑥 + 1)) → (abs‘(𝐹𝑘)) < (𝑥 + 1)))
2220, 21mpd3an3 1464 . . . . . . . . . . . . . 14 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘(𝐹𝑘)) ≤ 𝑥𝑥 < (𝑥 + 1)) → (abs‘(𝐹𝑘)) < (𝑥 + 1)))
2319, 22mpan2d 694 . . . . . . . . . . . . 13 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹𝑘)) ≤ 𝑥 → (abs‘(𝐹𝑘)) < (𝑥 + 1)))
2423expcom 417 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((abs‘(𝐹𝑘)) ∈ ℝ → ((abs‘(𝐹𝑘)) ≤ 𝑥 → (abs‘(𝐹𝑘)) < (𝑥 + 1))))
2524ralimdv 3104 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹𝑘)) ≤ 𝑥 → (abs‘(𝐹𝑘)) < (𝑥 + 1))))
2625impcom 411 . . . . . . . . . 10 ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹𝑘)) ≤ 𝑥 → (abs‘(𝐹𝑘)) < (𝑥 + 1)))
27 ralim 3083 . . . . . . . . . 10 (∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹𝑘)) ≤ 𝑥 → (abs‘(𝐹𝑘)) < (𝑥 + 1)) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ≤ 𝑥 → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < (𝑥 + 1)))
2826, 27syl 17 . . . . . . . . 9 ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ≤ 𝑥 → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < (𝑥 + 1)))
29 brralrspcev 5129 . . . . . . . . 9 (((𝑥 + 1) ∈ ℝ ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < (𝑥 + 1)) → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤)
3017, 28, 29syl6an 684 . . . . . . . 8 ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ≤ 𝑥 → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤))
3130rexlimdva 3213 . . . . . . 7 (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ → (∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ≤ 𝑥 → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤))
3215, 31mpd 15 . . . . . 6 (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) ∈ ℝ → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤)
3312, 32syl 17 . . . . 5 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤)
34 max1 12804 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤𝑧, 𝑧, 𝑤))
35343adant3 1134 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → 𝑤 ≤ if(𝑤𝑧, 𝑧, 𝑤))
36 simp3 1140 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → (abs‘(𝐹𝑘)) ∈ ℝ)
37 simp1 1138 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → 𝑤 ∈ ℝ)
38 ifcl 4500 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ) → if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ)
3938ancoms 462 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ)
40393adant3 1134 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ)
41 ltletr 10953 . . . . . . . . . . . . . . . . . 18 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ) → (((abs‘(𝐹𝑘)) < 𝑤𝑤 ≤ if(𝑤𝑧, 𝑧, 𝑤)) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
4236, 37, 40, 41syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → (((abs‘(𝐹𝑘)) < 𝑤𝑤 ≤ if(𝑤𝑧, 𝑧, 𝑤)) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
4335, 42mpan2d 694 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → ((abs‘(𝐹𝑘)) < 𝑤 → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
44 max2 12806 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ≤ if(𝑤𝑧, 𝑧, 𝑤))
45443adant3 1134 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → 𝑧 ≤ if(𝑤𝑧, 𝑧, 𝑤))
46 simp2 1139 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → 𝑧 ∈ ℝ)
47 ltletr 10953 . . . . . . . . . . . . . . . . . 18 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ) → (((abs‘(𝐹𝑘)) < 𝑧𝑧 ≤ if(𝑤𝑧, 𝑧, 𝑤)) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
4836, 46, 40, 47syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → (((abs‘(𝐹𝑘)) < 𝑧𝑧 ≤ if(𝑤𝑧, 𝑧, 𝑤)) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
4945, 48mpan2d 694 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → ((abs‘(𝐹𝑘)) < 𝑧 → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
5043, 49jaod 859 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (abs‘(𝐹𝑘)) ∈ ℝ) → (((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
51503expia 1123 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((abs‘(𝐹𝑘)) ∈ ℝ → (((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤))))
5251ralimdv 3104 . . . . . . . . . . . . 13 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → ∀𝑘𝑍 (((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤))))
53 ralim 3083 . . . . . . . . . . . . 13 (∀𝑘𝑍 (((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)) → (∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → ∀𝑘𝑍 (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)))
5452, 53syl6 35 . . . . . . . . . . . 12 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → ∀𝑘𝑍 (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤))))
55 brralrspcev 5129 . . . . . . . . . . . . . 14 ((if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ ∧ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤)) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)
5655ex 416 . . . . . . . . . . . . 13 (if(𝑤𝑧, 𝑧, 𝑤) ∈ ℝ → (∀𝑘𝑍 (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))
5739, 56syl 17 . . . . . . . . . . . 12 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (∀𝑘𝑍 (abs‘(𝐹𝑘)) < if(𝑤𝑧, 𝑧, 𝑤) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))
5854, 57syl6d 75 . . . . . . . . . . 11 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))
59 uzssz 12488 . . . . . . . . . . . . . . . . . . . . . 22 (ℤ𝑀) ⊆ ℤ
603, 59eqsstri 3951 . . . . . . . . . . . . . . . . . . . . 21 𝑍 ⊆ ℤ
6160sseli 3913 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝑍𝑘 ∈ ℤ)
6260sseli 3913 . . . . . . . . . . . . . . . . . . . 20 (𝑗𝑍𝑗 ∈ ℤ)
63 uztric 12491 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑗)))
6461, 62, 63syl2anr 600 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑍𝑘𝑍) → (𝑗 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑗)))
65 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗𝑍𝑘𝑍) → 𝑘𝑍)
6665, 3eleqtrdi 2850 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝑍𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
67 elfzuzb 13135 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (𝑀...𝑗) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑗 ∈ (ℤ𝑘)))
6867baib 539 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (ℤ𝑀) → (𝑘 ∈ (𝑀...𝑗) ↔ 𝑗 ∈ (ℤ𝑘)))
6966, 68syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑍𝑘𝑍) → (𝑘 ∈ (𝑀...𝑗) ↔ 𝑗 ∈ (ℤ𝑘)))
7069orbi1d 917 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑍𝑘𝑍) → ((𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ𝑗)) ↔ (𝑗 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑗))))
7164, 70mpbird 260 . . . . . . . . . . . . . . . . . 18 ((𝑗𝑍𝑘𝑍) → (𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ𝑗)))
7271ex 416 . . . . . . . . . . . . . . . . 17 (𝑗𝑍 → (𝑘𝑍 → (𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ𝑗))))
73 pm3.48 964 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)) → ((𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ𝑗)) → ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧)))
7472, 73syl9 77 . . . . . . . . . . . . . . . 16 (𝑗𝑍 → (((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)) → (𝑘𝑍 → ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧))))
7574alimdv 1924 . . . . . . . . . . . . . . 15 (𝑗𝑍 → (∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)) → ∀𝑘(𝑘𝑍 → ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧))))
76 df-ral 3069 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 ↔ ∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤))
77 df-ral 3069 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 ↔ ∀𝑘(𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧))
7876, 77anbi12i 630 . . . . . . . . . . . . . . . 16 ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧) ↔ (∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ ∀𝑘(𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)))
79 19.26 1878 . . . . . . . . . . . . . . . 16 (∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)) ↔ (∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ ∀𝑘(𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)))
8078, 79bitr4i 281 . . . . . . . . . . . . . . 15 ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧) ↔ ∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ𝑗) → (abs‘(𝐹𝑘)) < 𝑧)))
81 df-ral 3069 . . . . . . . . . . . . . . 15 (∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) ↔ ∀𝑘(𝑘𝑍 → ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧)))
8275, 80, 813imtr4g 299 . . . . . . . . . . . . . 14 (𝑗𝑍 → ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧) → ∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧)))
83823impib 1118 . . . . . . . . . . . . 13 ((𝑗𝑍 ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧) → ∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧))
8483imim1i 63 . . . . . . . . . . . 12 ((∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦) → ((𝑗𝑍 ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))
85843expd 1355 . . . . . . . . . . 11 ((∀𝑘𝑍 ((abs‘(𝐹𝑘)) < 𝑤 ∨ (abs‘(𝐹𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦) → (𝑗𝑍 → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))))
8658, 85syl6 35 . . . . . . . . . 10 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (𝑗𝑍 → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))))
8786com23 86 . . . . . . . . 9 ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑗𝑍 → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))))
8887expimpd 457 . . . . . . . 8 (𝑤 ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗𝑍) → (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))))
8988com3r 87 . . . . . . 7 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (𝑤 ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗𝑍) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))))
9089com34 91 . . . . . 6 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (𝑤 ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → ((𝑧 ∈ ℝ ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))))
9190rexlimdv 3212 . . . . 5 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹𝑘)) < 𝑤 → ((𝑧 ∈ ℝ ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))))
9233, 91mpd 15 . . . 4 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)))
9392rexlimdvv 3222 . . 3 (∀𝑘𝑍 (abs‘(𝐹𝑘)) ∈ ℝ → (∃𝑧 ∈ ℝ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(𝐹𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))
942, 8, 93sylsyld 61 . 2 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦))
9594imp 410 1 ((∀𝑘𝑍 (𝐹𝑘) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑘𝑍 (abs‘(𝐹𝑘)) < 𝑦)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3a 1089  wal 1541   = wceq 1543  wcel 2112  wral 3064  wrex 3065  wss 3883  ifcif 4455   class class class wbr 5069  cfv 6400  (class class class)co 7234  Fincfn 8649  cc 10756  cr 10757  1c1 10759   + caddc 10761   < clt 10896  cle 10897  cmin 11091  cz 12205  cuz 12467  +crp 12615  ...cfz 13124  abscabs 14829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835  ax-pre-sup 10836
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-1st 7782  df-2nd 7783  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-1o 8225  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-fin 8653  df-sup 9087  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-div 11519  df-nn 11860  df-2 11922  df-3 11923  df-n0 12120  df-z 12206  df-uz 12468  df-rp 12616  df-fz 13125  df-seq 13606  df-exp 13667  df-cj 14694  df-re 14695  df-im 14696  df-sqrt 14830  df-abs 14831
This theorem is referenced by:  climbdd  15267
  Copyright terms: Public domain W3C validator