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

Metamath Proof Explorer

Theorem o1le

Description: Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1le.1 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
o1le.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
o1le.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
o1le.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
o1le.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ 𝐶 ) ≤ ( abs ‘ 𝐵 ) )
Assertion o1le ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1le.1 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
2 o1le.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
3 o1le.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 o1le.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
5 o1le.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ 𝐶 ) ≤ ( abs ‘ 𝐵 ) )
6 3 2 o1mptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
7 6 lo1o12 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )
8 2 7 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) )
9 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ V )
10 4 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐶 ) ∈ ℝ )
11 1 8 9 10 5 lo1le ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐶 ) ) ∈ ≤𝑂(1) )
12 4 lo1o12 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐶 ) ) ∈ ≤𝑂(1) ) )
13 11 12 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )