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

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion caubnd ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑦 )

Proof

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