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 ffvelcdmda ⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑧 ∈ 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) )