elbigolo1

Description: A function (into the positive reals) is of order G(x) iff the quotient of the function and G(x) (also a function into the positive reals) is an eventually upper bounded function. (Contributed by AV, 20-May-2020) (Proof shortened by II, 16-Feb-2023)

		Ref	Expression
	Assertion	elbigolo1	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F \in O (G) \leftrightarrow F /_{fG\in\leq 𝑂 (1)})$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ F : A ⟶ ℝ^{+} \to F : A ⟶ ℝ^{+}$
2		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
3	2	a1i	$⊢ F : A ⟶ ℝ^{+} \to ℝ^{+} \subseteq ℝ$
4	1 3	fssd	$⊢ F : A ⟶ ℝ^{+} \to F : A ⟶ ℝ$
5	4	3ad2ant3	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to F : A ⟶ ℝ$
6	5	adantr	$⊢ ((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \to F : A ⟶ ℝ$
7	6	ffvelcdmda	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to F (y) \in ℝ$
8		simplrr	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to m \in ℝ$
9		simpl2	$⊢ ((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \to G : A ⟶ ℝ^{+}$
10	9	ffvelcdmda	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to G (y) \in ℝ^{+}$
11	10	rpregt0d	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to (G (y) \in ℝ \land 0 < G (y))$
12	7 8 11	3jca	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to (F (y) \in ℝ \land m \in ℝ \land (G (y) \in ℝ \land 0 < G (y)))$
13		ledivmul2	$⊢ (F (y) \in ℝ \land m \in ℝ \land (G (y) \in ℝ \land 0 < G (y))) \to (\frac{F (y)}{G (y)} \leq m \leftrightarrow F (y) \leq m G (y))$
14	13	bicomd	$⊢ (F (y) \in ℝ \land m \in ℝ \land (G (y) \in ℝ \land 0 < G (y))) \to (F (y) \leq m G (y) \leftrightarrow \frac{F (y)}{G (y)} \leq m)$
15	12 14	syl	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to (F (y) \leq m G (y) \leftrightarrow \frac{F (y)}{G (y)} \leq m)$
16		id	$⊢ G : A ⟶ ℝ^{+} \to G : A ⟶ ℝ^{+}$
17	2	a1i	$⊢ G : A ⟶ ℝ^{+} \to ℝ^{+} \subseteq ℝ$
18	16 17	fssd	$⊢ G : A ⟶ ℝ^{+} \to G : A ⟶ ℝ$
19	18	3ad2ant2	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to G : A ⟶ ℝ$
20		reex	$⊢ ℝ \in V$
21	20	ssex	$⊢ A \subseteq ℝ \to A \in V$
22	21	3ad2ant1	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to A \in V$
23	5 19 22	3jca	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V)$
24	23	adantr	$⊢ ((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \to (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V)$
25	24	adantr	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V)$
26		ffun	$⊢ G : A ⟶ ℝ^{+} \to Fun G$
27	26	adantl	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to Fun G$
28	21	anim1ci	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to (G : A ⟶ ℝ^{+} \land A \in V)$
29		fex	$⊢ (G : A ⟶ ℝ^{+} \land A \in V) \to G \in V$
30	28 29	syl	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to G \in V$
31		0red	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to 0 \in ℝ$
32		frn	$⊢ G : A ⟶ ℝ^{+} \to ran G \subseteq ℝ^{+}$
33		0nrp	$⊢ \neg 0 \in ℝ^{+}$
34		id	$⊢ ran G \subseteq ℝ^{+} \to ran G \subseteq ℝ^{+}$
35	34	ssneld	$⊢ ran G \subseteq ℝ^{+} \to (\neg 0 \in ℝ^{+} \to \neg 0 \in ran G)$
36	33 35	mpi	$⊢ ran G \subseteq ℝ^{+} \to \neg 0 \in ran G$
37		df-nel	$⊢ 0 \notin ran G \leftrightarrow \neg 0 \in ran G$
38	36 37	sylibr	$⊢ ran G \subseteq ℝ^{+} \to 0 \notin ran G$
39	32 38	syl	$⊢ G : A ⟶ ℝ^{+} \to 0 \notin ran G$
40	39	adantl	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to 0 \notin ran G$
41		suppdm	$⊢ ((Fun G \land G \in V \land 0 \in ℝ) \land 0 \notin ran G) \to G supp 0 = dom G$
42	27 30 31 40 41	syl31anc	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to G supp 0 = dom G$
43		fdm	$⊢ G : A ⟶ ℝ^{+} \to dom G = A$
44	43	adantl	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to dom G = A$
45	42 44	eqtrd	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+}) \to G supp 0 = A$
46	45	3adant3	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to G supp 0 = A$
47	46	eqcomd	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to A = G supp 0$
48	47	adantr	$⊢ ((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \to A = G supp 0$
49	48	eleq2d	$⊢ ((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \to (y \in A \leftrightarrow y \in {supp}_{0} (G))$
50	49	biimpa	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to y \in {supp}_{0} (G)$
51		refdivmptfv	$⊢ ((F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V) \land y \in {supp}_{0} (G)) \to (F /_{fG(y)=\frac{F (y)}{G (y)}})$
52	25 50 51	syl2anc	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to (F /_{fG(y)=\frac{F (y)}{G (y)}})$
53	52	breq1d	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to ((F /_{fG(y)\leqm\leftrightarrow\frac{F (y)}{G (y)} \leq m}))$
54	15 53	bitr4d	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to (F (y) \leq m G (y) \leftrightarrow (F /_{fG(y)\leqm}))$
55	54	imbi2d	$⊢ (((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \land y \in A) \to ((x \leq y \to F (y) \leq m G (y)) \leftrightarrow (x \leq y \to (F /_{fG(y)\leqm})))$
56	55	ralbidva	$⊢ ((A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \land (x \in ℝ \land m \in ℝ)) \to (\forall y \in A (x \leq y \to F (y) \leq m G (y)) \leftrightarrow \forall y \in A (x \leq y \to (F /_{fG(y)\leqm})))$
57	56	2rexbidva	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (\exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y)) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to (F /_{fG(y)\leqm})))$
58		simp1	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to A \subseteq ℝ$
59		ssidd	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to A \subseteq A$
60		elbigo2	$⊢ ((G : A ⟶ ℝ \land A \subseteq ℝ) \land (F : A ⟶ ℝ \land A \subseteq A)) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y)))$
61	19 58 5 59 60	syl22anc	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y)))$
62		refdivmptf	$⊢ (F : A ⟶ ℝ \land G : A ⟶ ℝ \land A \in V) \to (F /_{fG:G supp 0⟶ℝ})$
63	23 62	syl	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F /_{fG:G supp 0⟶ℝ})$
64	47	feq2d	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to ((F /_{fG:A⟶ℝ\leftrightarrow(F /_{f} G) : G supp 0 ⟶ ℝ}))$
65	63 64	mpbird	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F /_{fG:A⟶ℝ})$
66		ello12	$⊢ ((F /_{fG:A⟶ℝ\landA \subseteq ℝ\to(F /_{f} G \in \leq 𝑂 (1) \leftrightarrow \exists x \in ℝ)}))$
67	65 58 66	syl2anc	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F /_{fG\in\leq 𝑂 (1)\leftrightarrow\exists x \in ℝ})$
68	57 61 67	3bitr4d	$⊢ (A \subseteq ℝ \land G : A ⟶ ℝ^{+} \land F : A ⟶ ℝ^{+}) \to (F \in O (G) \leftrightarrow F /_{fG\in\leq 𝑂 (1)})$

Metamath Proof Explorer

Theorem elbigolo1

Proof