Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elbigolo1 Structured version   Visualization version   GIF version

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

Proof of Theorem elbigolo1
Dummy variables 𝑚 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . . . . . . . 12 (𝐹:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+)
2 rpssre 13042 . . . . . . . . . . . . 13 + ⊆ ℝ
32a1i 11 . . . . . . . . . . . 12 (𝐹:𝐴⟶ℝ+ → ℝ+ ⊆ ℝ)
41, 3fssd 6753 . . . . . . . . . . 11 (𝐹:𝐴⟶ℝ+𝐹:𝐴⟶ℝ)
543ad2ant3 1136 . . . . . . . . . 10 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → 𝐹:𝐴⟶ℝ)
65adantr 480 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐹:𝐴⟶ℝ)
76ffvelcdmda 7104 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → (𝐹𝑦) ∈ ℝ)
8 simplrr 778 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → 𝑚 ∈ ℝ)
9 simpl2 1193 . . . . . . . . . 10 (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐺:𝐴⟶ℝ+)
109ffvelcdmda 7104 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → (𝐺𝑦) ∈ ℝ+)
1110rpregt0d 13083 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → ((𝐺𝑦) ∈ ℝ ∧ 0 < (𝐺𝑦)))
127, 8, 113jca 1129 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → ((𝐹𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺𝑦) ∈ ℝ ∧ 0 < (𝐺𝑦))))
13 ledivmul2 12147 . . . . . . . 8 (((𝐹𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺𝑦) ∈ ℝ ∧ 0 < (𝐺𝑦))) → (((𝐹𝑦) / (𝐺𝑦)) ≤ 𝑚 ↔ (𝐹𝑦) ≤ (𝑚 · (𝐺𝑦))))
1413bicomd 223 . . . . . . 7 (((𝐹𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺𝑦) ∈ ℝ ∧ 0 < (𝐺𝑦))) → ((𝐹𝑦) ≤ (𝑚 · (𝐺𝑦)) ↔ ((𝐹𝑦) / (𝐺𝑦)) ≤ 𝑚))
1512, 14syl 17 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → ((𝐹𝑦) ≤ (𝑚 · (𝐺𝑦)) ↔ ((𝐹𝑦) / (𝐺𝑦)) ≤ 𝑚))
16 id 22 . . . . . . . . . . . . 13 (𝐺:𝐴⟶ℝ+𝐺:𝐴⟶ℝ+)
172a1i 11 . . . . . . . . . . . . 13 (𝐺:𝐴⟶ℝ+ → ℝ+ ⊆ ℝ)
1816, 17fssd 6753 . . . . . . . . . . . 12 (𝐺:𝐴⟶ℝ+𝐺:𝐴⟶ℝ)
19183ad2ant2 1135 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → 𝐺:𝐴⟶ℝ)
20 reex 11246 . . . . . . . . . . . . 13 ℝ ∈ V
2120ssex 5321 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ → 𝐴 ∈ V)
22213ad2ant1 1134 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → 𝐴 ∈ V)
235, 19, 223jca 1129 . . . . . . . . . 10 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V))
2423adantr 480 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V))
2524adantr 480 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V))
26 ffun 6739 . . . . . . . . . . . . . . . 16 (𝐺:𝐴⟶ℝ+ → Fun 𝐺)
2726adantl 481 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → Fun 𝐺)
2821anim1ci 616 . . . . . . . . . . . . . . . 16 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺:𝐴⟶ℝ+𝐴 ∈ V))
29 fex 7246 . . . . . . . . . . . . . . . 16 ((𝐺:𝐴⟶ℝ+𝐴 ∈ V) → 𝐺 ∈ V)
3028, 29syl 17 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 𝐺 ∈ V)
31 0red 11264 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 0 ∈ ℝ)
32 frn 6743 . . . . . . . . . . . . . . . . 17 (𝐺:𝐴⟶ℝ+ → ran 𝐺 ⊆ ℝ+)
33 0nrp 13070 . . . . . . . . . . . . . . . . . . 19 ¬ 0 ∈ ℝ+
34 id 22 . . . . . . . . . . . . . . . . . . . 20 (ran 𝐺 ⊆ ℝ+ → ran 𝐺 ⊆ ℝ+)
3534ssneld 3985 . . . . . . . . . . . . . . . . . . 19 (ran 𝐺 ⊆ ℝ+ → (¬ 0 ∈ ℝ+ → ¬ 0 ∈ ran 𝐺))
3633, 35mpi 20 . . . . . . . . . . . . . . . . . 18 (ran 𝐺 ⊆ ℝ+ → ¬ 0 ∈ ran 𝐺)
37 df-nel 3047 . . . . . . . . . . . . . . . . . 18 (0 ∉ ran 𝐺 ↔ ¬ 0 ∈ ran 𝐺)
3836, 37sylibr 234 . . . . . . . . . . . . . . . . 17 (ran 𝐺 ⊆ ℝ+ → 0 ∉ ran 𝐺)
3932, 38syl 17 . . . . . . . . . . . . . . . 16 (𝐺:𝐴⟶ℝ+ → 0 ∉ ran 𝐺)
4039adantl 481 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 0 ∉ ran 𝐺)
41 suppdm 48427 . . . . . . . . . . . . . . 15 (((Fun 𝐺𝐺 ∈ V ∧ 0 ∈ ℝ) ∧ 0 ∉ ran 𝐺) → (𝐺 supp 0) = dom 𝐺)
4227, 30, 31, 40, 41syl31anc 1375 . . . . . . . . . . . . . 14 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = dom 𝐺)
43 fdm 6745 . . . . . . . . . . . . . . 15 (𝐺:𝐴⟶ℝ+ → dom 𝐺 = 𝐴)
4443adantl 481 . . . . . . . . . . . . . 14 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → dom 𝐺 = 𝐴)
4542, 44eqtrd 2777 . . . . . . . . . . . . 13 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = 𝐴)
46453adant3 1133 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (𝐺 supp 0) = 𝐴)
4746eqcomd 2743 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → 𝐴 = (𝐺 supp 0))
4847adantr 480 . . . . . . . . . 10 (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐴 = (𝐺 supp 0))
4948eleq2d 2827 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦𝐴𝑦 ∈ (𝐺 supp 0)))
5049biimpa 476 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → 𝑦 ∈ (𝐺 supp 0))
51 refdivmptfv 48467 . . . . . . . 8 (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑦) = ((𝐹𝑦) / (𝐺𝑦)))
5225, 50, 51syl2anc 584 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → ((𝐹 /f 𝐺)‘𝑦) = ((𝐹𝑦) / (𝐺𝑦)))
5352breq1d 5153 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → (((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚 ↔ ((𝐹𝑦) / (𝐺𝑦)) ≤ 𝑚))
5415, 53bitr4d 282 . . . . 5 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → ((𝐹𝑦) ≤ (𝑚 · (𝐺𝑦)) ↔ ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))
5554imbi2d 340 . . . 4 ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦𝐴) → ((𝑥𝑦 → (𝐹𝑦) ≤ (𝑚 · (𝐺𝑦))) ↔ (𝑥𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)))
5655ralbidva 3176 . . 3 (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∀𝑦𝐴 (𝑥𝑦 → (𝐹𝑦) ≤ (𝑚 · (𝐺𝑦))) ↔ ∀𝑦𝐴 (𝑥𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)))
57562rexbidva 3220 . 2 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦𝐴 (𝑥𝑦 → (𝐹𝑦) ≤ (𝑚 · (𝐺𝑦))) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦𝐴 (𝑥𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)))
58 simp1 1137 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → 𝐴 ⊆ ℝ)
59 ssidd 4007 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → 𝐴𝐴)
60 elbigo2 48473 . . 3 (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐴⟶ℝ ∧ 𝐴𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦𝐴 (𝑥𝑦 → (𝐹𝑦) ≤ (𝑚 · (𝐺𝑦)))))
6119, 58, 5, 59, 60syl22anc 839 . 2 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦𝐴 (𝑥𝑦 → (𝐹𝑦) ≤ (𝑚 · (𝐺𝑦)))))
62 refdivmptf 48463 . . . . 5 ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ)
6323, 62syl 17 . . . 4 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ)
6447feq2d 6722 . . . 4 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → ((𝐹 /f 𝐺):𝐴⟶ℝ ↔ (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ))
6563, 64mpbird 257 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (𝐹 /f 𝐺):𝐴⟶ℝ)
66 ello12 15552 . . 3 (((𝐹 /f 𝐺):𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → ((𝐹 /f 𝐺) ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦𝐴 (𝑥𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)))
6765, 58, 66syl2anc 584 . 2 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → ((𝐹 /f 𝐺) ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦𝐴 (𝑥𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)))
6857, 61, 673bitr4d 311 1 ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wnel 3046  wral 3061  wrex 3070  Vcvv 3480  wss 3951   class class class wbr 5143  dom cdm 5685  ran crn 5686  Fun wfun 6555  wf 6557  cfv 6561  (class class class)co 7431   supp csupp 8185  cr 11154  0cc0 11155   · cmul 11160   < clt 11295  cle 11296   / cdiv 11920  +crp 13034  ≤𝑂(1)clo1 15523   /f cfdiv 48458  Οcbigo 48468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-supp 8186  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-rp 13035  df-ico 13393  df-lo1 15527  df-fdiv 48459  df-bigo 48469
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator