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

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) ) )