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