Metamath Proof Explorer


Theorem o1dif

Description: If the difference of two functions is eventually bounded, eventual boundedness of either one implies the other. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1dif.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
o1dif.2 ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
o1dif.3 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) )
Assertion o1dif ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 o1dif.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
2 o1dif.2 ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
3 o1dif.3 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) )
4 o1sub ( ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ∧ ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) ) → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ) ∈ 𝑂(1) )
5 4 expcom ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ) ∈ 𝑂(1) ) )
6 3 5 syl ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ) ∈ 𝑂(1) ) )
7 1 2 subcld ( ( 𝜑𝑥𝐴 ) → ( 𝐵𝐶 ) ∈ ℂ )
8 7 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 ( 𝐵𝐶 ) ∈ ℂ )
9 dmmptg ( ∀ 𝑥𝐴 ( 𝐵𝐶 ) ∈ ℂ → dom ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) = 𝐴 )
10 8 9 syl ( 𝜑 → dom ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) = 𝐴 )
11 o1dm ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) → dom ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ⊆ ℝ )
12 3 11 syl ( 𝜑 → dom ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ⊆ ℝ )
13 10 12 eqsstrrd ( 𝜑𝐴 ⊆ ℝ )
14 reex ℝ ∈ V
15 14 ssex ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
16 13 15 syl ( 𝜑𝐴 ∈ V )
17 eqidd ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 ) )
18 eqidd ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) = ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) )
19 16 1 7 17 18 offval2 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 − ( 𝐵𝐶 ) ) ) )
20 1 2 nncand ( ( 𝜑𝑥𝐴 ) → ( 𝐵 − ( 𝐵𝐶 ) ) = 𝐶 )
21 20 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵 − ( 𝐵𝐶 ) ) ) = ( 𝑥𝐴𝐶 ) )
22 19 21 eqtrd ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ) = ( 𝑥𝐴𝐶 ) )
23 22 eleq1d ( 𝜑 → ( ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ) )
24 6 23 sylibd ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ) )
25 o1add ( ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) ∧ ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∘f + ( 𝑥𝐴𝐶 ) ) ∈ 𝑂(1) )
26 25 ex ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) → ( ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) → ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∘f + ( 𝑥𝐴𝐶 ) ) ∈ 𝑂(1) ) )
27 3 26 syl ( 𝜑 → ( ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) → ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∘f + ( 𝑥𝐴𝐶 ) ) ∈ 𝑂(1) ) )
28 eqidd ( 𝜑 → ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴𝐶 ) )
29 16 7 2 18 28 offval2 ( 𝜑 → ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∘f + ( 𝑥𝐴𝐶 ) ) = ( 𝑥𝐴 ↦ ( ( 𝐵𝐶 ) + 𝐶 ) ) )
30 1 2 npcand ( ( 𝜑𝑥𝐴 ) → ( ( 𝐵𝐶 ) + 𝐶 ) = 𝐵 )
31 30 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( ( 𝐵𝐶 ) + 𝐶 ) ) = ( 𝑥𝐴𝐵 ) )
32 29 31 eqtrd ( 𝜑 → ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∘f + ( 𝑥𝐴𝐶 ) ) = ( 𝑥𝐴𝐵 ) )
33 32 eleq1d ( 𝜑 → ( ( ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∘f + ( 𝑥𝐴𝐶 ) ) ∈ 𝑂(1) ↔ ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ) )
34 27 33 sylibd ( 𝜑 → ( ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ) )
35 24 34 impbid ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ) )