Metamath Proof Explorer

Theorem lo1sub

Description: The difference of an eventually upper bounded function and an eventually bounded function is eventually upper bounded. The "correct" sharp result here takes the second function to be eventually lower bounded instead of just bounded, but our notation for this is simply ( x e. A |-> -u C ) e. <_O(1) , so it is just a special case of lo1add . (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypotheses lo1sub.1 ⊢ φ ∧ x ∈ A → B ∈ V
lo1sub.2 ⊢ φ ∧ x ∈ A → C ∈ ℝ
lo1sub.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
lo1sub.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1
Assertion lo1sub ⊢ φ → x ∈ A ⟼ B − C ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 lo1sub.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 lo1sub.2 ⊢ φ ∧ x ∈ A → C ∈ ℝ
3 lo1sub.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
4 lo1sub.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1
5 1 3 lo1mptrcl ⊢ φ ∧ x ∈ A → B ∈ ℝ
6 5 recnd ⊢ φ ∧ x ∈ A → B ∈ ℂ
7 2 recnd ⊢ φ ∧ x ∈ A → C ∈ ℂ
8 6 7 negsubd ⊢ φ ∧ x ∈ A → B + − C = B − C
9 8 mpteq2dva ⊢ φ → x ∈ A ⟼ B + − C = x ∈ A ⟼ B − C
10 2 renegcld ⊢ φ ∧ x ∈ A → − C ∈ ℝ
11 2 o1lo1 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1 ↔ x ∈ A ⟼ C ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − C ∈ ≤𝑂⁡1
12 4 11 mpbid ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − C ∈ ≤𝑂⁡1
13 12 simprd ⊢ φ → x ∈ A ⟼ − C ∈ ≤𝑂⁡1
14 5 10 3 13 lo1add ⊢ φ → x ∈ A ⟼ B + − C ∈ ≤𝑂⁡1
15 9 14 eqeltrrd ⊢ φ → x ∈ A ⟼ B − C ∈ ≤𝑂⁡1