# Metamath Proof Explorer

## Theorem elbigo2r

Description: Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigo2r ${⊢}\left(\left({G}:{A}⟶ℝ\wedge {A}\subseteq ℝ\right)\wedge \left({F}:{B}⟶ℝ\wedge {B}\subseteq {A}\right)\wedge \left({C}\in ℝ\wedge {M}\in ℝ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)\right)\to {F}\in O\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{y}={C}\to \left({y}\le {x}↔{C}\le {x}\right)$
2 1 imbi1d ${⊢}{y}={C}\to \left(\left({y}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)↔\left({C}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)\right)$
3 2 ralbidv ${⊢}{y}={C}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)\right)$
4 oveq1 ${⊢}{m}={M}\to {m}{G}\left({x}\right)={M}{G}\left({x}\right)$
5 4 breq2d ${⊢}{m}={M}\to \left({F}\left({x}\right)\le {m}{G}\left({x}\right)↔{F}\left({x}\right)\le {M}{G}\left({x}\right)\right)$
6 5 imbi2d ${⊢}{m}={M}\to \left(\left({C}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)↔\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)$
7 6 ralbidv ${⊢}{m}={M}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)$
8 3 7 rspc2ev ${⊢}\left({C}\in ℝ\wedge {M}\in ℝ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)$
9 8 3ad2ant3 ${⊢}\left(\left({G}:{A}⟶ℝ\wedge {A}\subseteq ℝ\right)\wedge \left({F}:{B}⟶ℝ\wedge {B}\subseteq {A}\right)\wedge \left({C}\in ℝ\wedge {M}\in ℝ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)$
10 elbigo2 ${⊢}\left(\left({G}:{A}⟶ℝ\wedge {A}\subseteq ℝ\right)\wedge \left({F}:{B}⟶ℝ\wedge {B}\subseteq {A}\right)\right)\to \left({F}\in O\left({G}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)\right)$
11 10 3adant3 ${⊢}\left(\left({G}:{A}⟶ℝ\wedge {A}\subseteq ℝ\right)\wedge \left({F}:{B}⟶ℝ\wedge {B}\subseteq {A}\right)\wedge \left({C}\in ℝ\wedge {M}\in ℝ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)\right)\to \left({F}\in O\left({G}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {F}\left({x}\right)\le {m}{G}\left({x}\right)\right)\right)$
12 9 11 mpbird ${⊢}\left(\left({G}:{A}⟶ℝ\wedge {A}\subseteq ℝ\right)\wedge \left({F}:{B}⟶ℝ\wedge {B}\subseteq {A}\right)\wedge \left({C}\in ℝ\wedge {M}\in ℝ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\le {x}\to {F}\left({x}\right)\le {M}{G}\left({x}\right)\right)\right)\right)\to {F}\in O\left({G}\right)$