Theorem elbigo2r

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

	Ref	Expression
Assertion	elbigo2r	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) ) → 𝐹 ∈ ( Ο ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 ≤ 𝑥 ↔ 𝐶 ≤ 𝑥 ) )
2	1	imbi1d	⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ) )
3	2	ralbidv	⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ) )
4		oveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) = ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) )
5	4	breq2d	⊢ ( 𝑚 = 𝑀 → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) )
6	5	imbi2d	⊢ ( 𝑚 = 𝑀 → ( ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) )
7	6	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) )
8	3 7	rspc2ev	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) )
9	8	3ad2ant3	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) )
10		elbigo2	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ) )
11	10	3adant3	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑥 ) ) ) ) )
12	9 11	mpbird	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑀 · ( 𝐺 ‘ 𝑥 ) ) ) ) ) → 𝐹 ∈ ( Ο ‘ 𝐺 ) )