Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐹 /f 𝐺 ) ∈ ≤𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐹 : 𝐴 ⟶ ℝ+ → 𝐹 : 𝐴 ⟶ ℝ+ )
2 rpssre ⊢ ℝ+ ⊆ ℝ
3 2 a1i ⊢ ( 𝐹 : 𝐴 ⟶ ℝ+ → ℝ+ ⊆ ℝ )
4 1 3 fssd ⊢ ( 𝐹 : 𝐴 ⟶ ℝ+ → 𝐹 : 𝐴 ⟶ ℝ )
5 4 3ad2ant3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → 𝐹 : 𝐴 ⟶ ℝ )
6 5 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝐹 : 𝐴 ⟶ ℝ )
7 6 ffvelrnda ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
8 simplrr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑚 ∈ ℝ )
9 simpl2 ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝐺 : 𝐴 ⟶ ℝ+ )
10 9 ffvelrnda ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ+ )
11 10 rpregt0d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑦 ) ∈ ℝ ∧ 0 < ( 𝐺 ‘ 𝑦 ) ) )
12 7 8 11 3jca ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ ℝ ∧ 0 < ( 𝐺 ‘ 𝑦 ) ) ) )
13 ledivmul2 ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ ℝ ∧ 0 < ( 𝐺 ‘ 𝑦 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ≤ 𝑚 ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
14 13 bicomd ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ ℝ ∧ 0 < ( 𝐺 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ≤ 𝑚 ) )
15 12 14 syl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ≤ 𝑚 ) )
16 id ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → 𝐺 : 𝐴 ⟶ ℝ+ )
17 2 a1i ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → ℝ+ ⊆ ℝ )
18 16 17 fssd ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → 𝐺 : 𝐴 ⟶ ℝ )
19 18 3ad2ant2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → 𝐺 : 𝐴 ⟶ ℝ )
20 reex ⊢ ℝ ∈ V
21 20 ssex ⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
22 21 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → 𝐴 ∈ V )
23 5 19 22 3jca ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ V ) )
24 23 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ V ) )
25 24 adantr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ V ) )
26 ffun ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → Fun 𝐺 )
27 26 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → Fun 𝐺 )
28 21 anim1ci ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → ( 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐴 ∈ V ) )
29 fex ⊢ ( ( 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐴 ∈ V ) → 𝐺 ∈ V )
30 28 29 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → 𝐺 ∈ V )
31 0red ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → 0 ∈ ℝ )
32 frn ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → ran 𝐺 ⊆ ℝ+ )
33 0nrp ⊢ ¬ 0 ∈ ℝ+
34 id ⊢ ( ran 𝐺 ⊆ ℝ+ → ran 𝐺 ⊆ ℝ+ )
35 34 ssneld ⊢ ( ran 𝐺 ⊆ ℝ+ → ( ¬ 0 ∈ ℝ+ → ¬ 0 ∈ ran 𝐺 ) )
36 33 35 mpi ⊢ ( ran 𝐺 ⊆ ℝ+ → ¬ 0 ∈ ran 𝐺 )
37 df-nel ⊢ ( 0 ∉ ran 𝐺 ↔ ¬ 0 ∈ ran 𝐺 )
38 36 37 sylibr ⊢ ( ran 𝐺 ⊆ ℝ+ → 0 ∉ ran 𝐺 )
39 32 38 syl ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → 0 ∉ ran 𝐺 )
40 39 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → 0 ∉ ran 𝐺 )
41 suppdm ⊢ ( ( ( Fun 𝐺 ∧ 𝐺 ∈ V ∧ 0 ∈ ℝ ) ∧ 0 ∉ ran 𝐺 ) → ( 𝐺 supp 0 ) = dom 𝐺 )
42 27 30 31 40 41 syl31anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → ( 𝐺 supp 0 ) = dom 𝐺 )
43 fdm ⊢ ( 𝐺 : 𝐴 ⟶ ℝ+ → dom 𝐺 = 𝐴 )
44 43 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → dom 𝐺 = 𝐴 )
45 42 44 eqtrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ) → ( 𝐺 supp 0 ) = 𝐴 )
46 45 3adant3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐺 supp 0 ) = 𝐴 )
47 46 eqcomd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → 𝐴 = ( 𝐺 supp 0 ) )
48 47 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝐴 = ( 𝐺 supp 0 ) )
49 48 eleq2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ ( 𝐺 supp 0 ) ) )
50 49 biimpa ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ( 𝐺 supp 0 ) )
51 refdivmptfv ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) )
52 25 50 51 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) )
53 52 breq1d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ↔ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ≤ 𝑚 ) )
54 15 53 bitr4d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ) )
55 54 imbi2d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≤ 𝑦 → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
56 55 ralbidva ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
57 56 2rexbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
58 simp1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → 𝐴 ⊆ ℝ )
59 ssidd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → 𝐴 ⊆ 𝐴 )
60 elbigo2 ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
61 19 58 5 59 60 syl22anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
62 refdivmptf ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ V ) → ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ )
63 23 62 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ )
64 47 feq2d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( ( 𝐹 /f 𝐺 ) : 𝐴 ⟶ ℝ ↔ ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ ) )
65 63 64 mpbird ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐹 /f 𝐺 ) : 𝐴 ⟶ ℝ )
66 ello12 ⊢ ( ( ( 𝐹 /f 𝐺 ) : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ( 𝐹 /f 𝐺 ) ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
67 65 58 66 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( ( 𝐹 /f 𝐺 ) ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( ( 𝐹 /f 𝐺 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
68 57 61 67 3bitr4d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ+ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐹 /f 𝐺 ) ∈ ≤𝑂(1) ) )