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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	lo1sub.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
	lo1sub.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
	lo1sub.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )
Assertion	lo1sub	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ ≤𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		lo1sub.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		lo1sub.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
3		lo1sub.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
4		lo1sub.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )
5	1 3	lo1mptrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6	5	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
7	2	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
8	6 7	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
9	8	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) )
10	2	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℝ )
11	2	o1lo1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ ≤𝑂(1) ) ) )
12	4 11	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ ≤𝑂(1) ) )
13	12	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ ≤𝑂(1) )
14	5 10 3 13	lo1add	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) ∈ ≤𝑂(1) )
15	9 14	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ ≤𝑂(1) )