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	$⊢ (φ \land x \in A) \to B \in ℂ$
	o1dif.2	$⊢ (φ \land x \in A) \to C \in ℂ$
	o1dif.3	$⊢ φ \to (x \in A ⟼ B - C) \in 𝑂 (1)$
Assertion	o1dif	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in 𝑂 (1))$

Proof

Step	Hyp	Ref	Expression
1		o1dif.1	$⊢ (φ \land x \in A) \to B \in ℂ$
2		o1dif.2	$⊢ (φ \land x \in A) \to C \in ℂ$
3		o1dif.3	$⊢ φ \to (x \in A ⟼ B - C) \in 𝑂 (1)$
4		o1sub	$⊢ ((x \in A ⟼ B) \in 𝑂 (1) \land (x \in A ⟼ B - C) \in 𝑂 (1)) \to (x \in A ⟼ B) -_{f} (x \in A ⟼ B - C) \in 𝑂 (1)$
5	4	expcom	$⊢ (x \in A ⟼ B - C) \in 𝑂 (1) \to ((x \in A ⟼ B) \in 𝑂 (1) \to (x \in A ⟼ B) -_{f} (x \in A ⟼ B - C) \in 𝑂 (1))$
6	3 5	syl	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \to (x \in A ⟼ B) -_{f} (x \in A ⟼ B - C) \in 𝑂 (1))$
7	1 2	subcld	$⊢ (φ \land x \in A) \to B - C \in ℂ$
8	7	ralrimiva	$⊢ φ \to \forall x \in A B - C \in ℂ$
9		dmmptg	$⊢ \forall x \in A B - C \in ℂ \to dom (x \in A ⟼ B - C) = A$
10	8 9	syl	$⊢ φ \to dom (x \in A ⟼ B - C) = A$
11		o1dm	$⊢ (x \in A ⟼ B - C) \in 𝑂 (1) \to dom (x \in A ⟼ B - C) \subseteq ℝ$
12	3 11	syl	$⊢ φ \to dom (x \in A ⟼ B - C) \subseteq ℝ$
13	10 12	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
14		reex	$⊢ ℝ \in V$
15	14	ssex	$⊢ A \subseteq ℝ \to A \in V$
16	13 15	syl	$⊢ φ \to A \in V$
17		eqidd	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
18		eqidd	$⊢ φ \to (x \in A ⟼ B - C) = (x \in A ⟼ B - C)$
19	16 1 7 17 18	offval2	$⊢ φ \to (x \in A ⟼ B) -_{f} (x \in A ⟼ B - C) = (x \in A ⟼ B - (B - C))$
20	1 2	nncand	$⊢ (φ \land x \in A) \to B - (B - C) = C$
21	20	mpteq2dva	$⊢ φ \to (x \in A ⟼ B - (B - C)) = (x \in A ⟼ C)$
22	19 21	eqtrd	$⊢ φ \to (x \in A ⟼ B) -_{f} (x \in A ⟼ B - C) = (x \in A ⟼ C)$
23	22	eleq1d	$⊢ φ \to ((x \in A ⟼ B) -_{f} (x \in A ⟼ B - C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in 𝑂 (1))$
24	6 23	sylibd	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \to (x \in A ⟼ C) \in 𝑂 (1))$
25		o1add	$⊢ ((x \in A ⟼ B - C) \in 𝑂 (1) \land (x \in A ⟼ C) \in 𝑂 (1)) \to (x \in A ⟼ B - C) +_{f} (x \in A ⟼ C) \in 𝑂 (1)$
26	25	ex	$⊢ (x \in A ⟼ B - C) \in 𝑂 (1) \to ((x \in A ⟼ C) \in 𝑂 (1) \to (x \in A ⟼ B - C) +_{f} (x \in A ⟼ C) \in 𝑂 (1))$
27	3 26	syl	$⊢ φ \to ((x \in A ⟼ C) \in 𝑂 (1) \to (x \in A ⟼ B - C) +_{f} (x \in A ⟼ C) \in 𝑂 (1))$
28		eqidd	$⊢ φ \to (x \in A ⟼ C) = (x \in A ⟼ C)$
29	16 7 2 18 28	offval2	$⊢ φ \to (x \in A ⟼ B - C) +_{f} (x \in A ⟼ C) = (x \in A ⟼ B - C + C)$
30	1 2	npcand	$⊢ (φ \land x \in A) \to B - C + C = B$
31	30	mpteq2dva	$⊢ φ \to (x \in A ⟼ B - C + C) = (x \in A ⟼ B)$
32	29 31	eqtrd	$⊢ φ \to (x \in A ⟼ B - C) +_{f} (x \in A ⟼ C) = (x \in A ⟼ B)$
33	32	eleq1d	$⊢ φ \to ((x \in A ⟼ B - C) +_{f} (x \in A ⟼ C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ B) \in 𝑂 (1))$
34	27 33	sylibd	$⊢ φ \to ((x \in A ⟼ C) \in 𝑂 (1) \to (x \in A ⟼ B) \in 𝑂 (1))$
35	24 34	impbid	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in 𝑂 (1))$

Metamath Proof Explorer

Theorem o1dif

Proof