elbigo2

Description: Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020)

		Ref	Expression
	Assertion	elbigo2	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in B (x \leq y \to F (y) \leq m G (y)))$

Proof

Step	Hyp	Ref	Expression
1		elbigo	$⊢ F \in O (G) \leftrightarrow (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
2		df-3an	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)) \leftrightarrow ((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
3	1 2	bitri	$⊢ F \in O (G) \leftrightarrow ((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
4		reex	$⊢ ℝ \in V$
5	4 4	pm3.2i	$⊢ (ℝ \in V \land ℝ \in V)$
6	5	a1i	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (ℝ \in V \land ℝ \in V)$
7		simpl	$⊢ (F : B ⟶ ℝ \land B \subseteq A) \to F : B ⟶ ℝ$
8	7	adantl	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to F : B ⟶ ℝ$
9		sstr2	$⊢ B \subseteq A \to (A \subseteq ℝ \to B \subseteq ℝ)$
10	9	adantld	$⊢ B \subseteq A \to ((G : A ⟶ ℝ \land A \subseteq ℝ) \to B \subseteq ℝ)$
11	10	adantl	$⊢ (F : B ⟶ ℝ \land B \subseteq A) \to ((G : A ⟶ ℝ \land A \subseteq ℝ) \to B \subseteq ℝ)$
12	11	impcom	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to B \subseteq ℝ$
13		elpm2r	$⊢ ((ℝ \in V \land ℝ \in V) \land (F : B ⟶ ℝ \land B \subseteq ℝ)) \to F \in (ℝ ↑_{𝑝𝑚} ℝ)$
14	6 8 12 13	syl12anc	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to F \in (ℝ ↑_{𝑝𝑚} ℝ)$
15		simpl	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (G : A ⟶ ℝ \land A \subseteq ℝ)$
16		elpm2r	$⊢ ((ℝ \in V \land ℝ \in V) \land (G : A ⟶ ℝ \land A \subseteq ℝ)) \to G \in (ℝ ↑_{𝑝𝑚} ℝ)$
17	6 15 16	syl2anc	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to G \in (ℝ ↑_{𝑝𝑚} ℝ)$
18		ibar	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \to (\exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y) \leftrightarrow ((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)))$
19	18	bicomd	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \to (((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
20	14 17 19	syl2anc	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ)) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
21	3 20	syl5bb	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
22		elin	$⊢ y \in (dom F \cap [x, +∞)) \leftrightarrow (y \in dom F \land y \in [x, +∞))$
23		fdm	$⊢ F : B ⟶ ℝ \to dom F = B$
24	23	ad2antrl	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to dom F = B$
25	24	ad2antrr	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to dom F = B$
26	25	eleq2d	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to (y \in dom F \leftrightarrow y \in B)$
27	26	anbi1d	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to ((y \in dom F \land y \in [x, +∞)) \leftrightarrow (y \in B \land y \in [x, +∞)))$
28		elicopnf	$⊢ x \in ℝ \to (y \in [x, +∞) \leftrightarrow (y \in ℝ \land x \leq y))$
29	28	ad3antlr	$⊢ (((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \land y \in B) \to (y \in [x, +∞) \leftrightarrow (y \in ℝ \land x \leq y))$
30	12	ad2antrr	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to B \subseteq ℝ$
31	30	sselda	$⊢ (((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \land y \in B) \to y \in ℝ$
32	31	biantrurd	$⊢ (((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \land y \in B) \to (x \leq y \leftrightarrow (y \in ℝ \land x \leq y))$
33	29 32	bitr4d	$⊢ (((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \land y \in B) \to (y \in [x, +∞) \leftrightarrow x \leq y)$
34	33	pm5.32da	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to ((y \in B \land y \in [x, +∞)) \leftrightarrow (y \in B \land x \leq y))$
35	27 34	bitrd	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to ((y \in dom F \land y \in [x, +∞)) \leftrightarrow (y \in B \land x \leq y))$
36	22 35	syl5bb	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to (y \in (dom F \cap [x, +∞)) \leftrightarrow (y \in B \land x \leq y))$
37	36	imbi1d	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to ((y \in (dom F \cap [x, +∞)) \to F (y) \leq m G (y)) \leftrightarrow ((y \in B \land x \leq y) \to F (y) \leq m G (y)))$
38		impexp	$⊢ ((y \in B \land x \leq y) \to F (y) \leq m G (y)) \leftrightarrow (y \in B \to (x \leq y \to F (y) \leq m G (y)))$
39	37 38	syl6bb	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to ((y \in (dom F \cap [x, +∞)) \to F (y) \leq m G (y)) \leftrightarrow (y \in B \to (x \leq y \to F (y) \leq m G (y))))$
40	39	ralbidv2	$⊢ ((((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \land m \in ℝ) \to (\forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y) \leftrightarrow \forall y \in B (x \leq y \to F (y) \leq m G (y)))$
41	40	rexbidva	$⊢ (((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \land x \in ℝ) \to (\exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y) \leftrightarrow \exists m \in ℝ \forall y \in B (x \leq y \to F (y) \leq m G (y)))$
42	41	rexbidva	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (\exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in B (x \leq y \to F (y) \leq m G (y)))$
43	21 42	bitrd	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : B ⟶ ℝ \land B \subseteq A)) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in B (x \leq y \to F (y) \leq m G (y)))$

Metamath Proof Explorer

Theorem elbigo2

Proof