Metamath Proof Explorer


Theorem rlimo1

Description: Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion rlimo1 ( 𝐹𝑟 𝐴𝐹 ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rlimf ( 𝐹𝑟 𝐴𝐹 : dom 𝐹 ⟶ ℂ )
2 1 ffvelrnda ( ( 𝐹𝑟 𝐴𝑧 ∈ dom 𝐹 ) → ( 𝐹𝑧 ) ∈ ℂ )
3 2 ralrimiva ( 𝐹𝑟 𝐴 → ∀ 𝑧 ∈ dom 𝐹 ( 𝐹𝑧 ) ∈ ℂ )
4 1rp 1 ∈ ℝ+
5 4 a1i ( 𝐹𝑟 𝐴 → 1 ∈ ℝ+ )
6 1 feqmptd ( 𝐹𝑟 𝐴𝐹 = ( 𝑧 ∈ dom 𝐹 ↦ ( 𝐹𝑧 ) ) )
7 id ( 𝐹𝑟 𝐴𝐹𝑟 𝐴 )
8 6 7 eqbrtrrd ( 𝐹𝑟 𝐴 → ( 𝑧 ∈ dom 𝐹 ↦ ( 𝐹𝑧 ) ) ⇝𝑟 𝐴 )
9 3 5 8 rlimi ( 𝐹𝑟 𝐴 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) )
10 rlimcl ( 𝐹𝑟 𝐴𝐴 ∈ ℂ )
11 10 adantr ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) → 𝐴 ∈ ℂ )
12 11 abscld ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) → ( abs ‘ 𝐴 ) ∈ ℝ )
13 peano2re ( ( abs ‘ 𝐴 ) ∈ ℝ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
14 12 13 syl ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
15 2 adantlr ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹𝑧 ) ∈ ℂ )
16 11 adantr ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → 𝐴 ∈ ℂ )
17 15 16 abs2difd ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) )
18 15 abscld ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹𝑧 ) ) ∈ ℝ )
19 12 adantr ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
20 18 19 resubcld ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) ∈ ℝ )
21 15 16 subcld ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹𝑧 ) − 𝐴 ) ∈ ℂ )
22 21 abscld ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) ∈ ℝ )
23 1red ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → 1 ∈ ℝ )
24 lelttr ( ( ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) → ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ) )
25 20 22 23 24 syl3anc ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) → ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ) )
26 17 25 mpand ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 → ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ) )
27 18 19 23 ltsubadd2d ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( abs ‘ ( 𝐹𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ↔ ( abs ‘ ( 𝐹𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) ) )
28 26 27 sylibd ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 → ( abs ‘ ( 𝐹𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) ) )
29 14 adantr ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
30 ltle ( ( ( abs ‘ ( 𝐹𝑧 ) ) ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ) → ( ( abs ‘ ( 𝐹𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
31 18 29 30 syl2anc ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( 𝐹𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
32 28 31 syld ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
33 32 imim2d ( ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝑦𝑧 → ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) → ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) )
34 33 ralimdva ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) → ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) )
35 breq2 ( 𝑤 = ( ( abs ‘ 𝐴 ) + 1 ) → ( ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ↔ ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
36 35 imbi2d ( 𝑤 = ( ( abs ‘ 𝐴 ) + 1 ) → ( ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) ↔ ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) )
37 36 ralbidv ( 𝑤 = ( ( abs ‘ 𝐴 ) + 1 ) → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) ↔ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) )
38 37 rspcev ( ( ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ∧ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) )
39 14 34 38 syl6an ( ( 𝐹𝑟 𝐴𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) ) )
40 39 reximdva ( 𝐹𝑟 𝐴 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( ( 𝐹𝑧 ) − 𝐴 ) ) < 1 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) ) )
41 9 40 mpd ( 𝐹𝑟 𝐴 → ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) )
42 rlimss ( 𝐹𝑟 𝐴 → dom 𝐹 ⊆ ℝ )
43 elo12 ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) ) )
44 1 42 43 syl2anc ( 𝐹𝑟 𝐴 → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦𝑧 → ( abs ‘ ( 𝐹𝑧 ) ) ≤ 𝑤 ) ) )
45 41 44 mpbird ( 𝐹𝑟 𝐴𝐹 ∈ 𝑂(1) )