| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℝ+ → 𝐹:𝐴⟶ℝ+) |
| 2 | | rpssre 13042 |
. . . . . . . . . . . . 13
⊢
ℝ+ ⊆ ℝ |
| 3 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℝ+ →
ℝ+ ⊆ ℝ) |
| 4 | 1, 3 | fssd 6753 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℝ+ → 𝐹:𝐴⟶ℝ) |
| 5 | 4 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐹:𝐴⟶ℝ) |
| 6 | 5 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐹:𝐴⟶ℝ) |
| 7 | 6 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ℝ) |
| 8 | | simplrr 778 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → 𝑚 ∈ ℝ) |
| 9 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐺:𝐴⟶ℝ+) |
| 10 | 9 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈
ℝ+) |
| 11 | 10 | rpregt0d 13083 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦))) |
| 12 | 7, 8, 11 | 3jca 1129 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦)))) |
| 13 | | ledivmul2 12147 |
. . . . . . . 8
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦))) → (((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) |
| 14 | 13 | bicomd 223 |
. . . . . . 7
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦))) → ((𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚)) |
| 15 | 12, 14 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚)) |
| 16 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴⟶ℝ+ → 𝐺:𝐴⟶ℝ+) |
| 17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴⟶ℝ+ →
ℝ+ ⊆ ℝ) |
| 18 | 16, 17 | fssd 6753 |
. . . . . . . . . . . 12
⊢ (𝐺:𝐴⟶ℝ+ → 𝐺:𝐴⟶ℝ) |
| 19 | 18 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐺:𝐴⟶ℝ) |
| 20 | | reex 11246 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
| 21 | 20 | ssex 5321 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ → 𝐴 ∈ V) |
| 22 | 21 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 ∈ V) |
| 23 | 5, 19, 22 | 3jca 1129 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V)) |
| 24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V)) |
| 25 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V)) |
| 26 | | ffun 6739 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐴⟶ℝ+ → Fun 𝐺) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → Fun
𝐺) |
| 28 | 21 | anim1ci 616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺:𝐴⟶ℝ+ ∧ 𝐴 ∈ V)) |
| 29 | | fex 7246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:𝐴⟶ℝ+ ∧ 𝐴 ∈ V) → 𝐺 ∈ V) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 𝐺 ∈ V) |
| 31 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 0 ∈
ℝ) |
| 32 | | frn 6743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:𝐴⟶ℝ+ → ran 𝐺 ⊆
ℝ+) |
| 33 | | 0nrp 13070 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 0
∈ ℝ+ |
| 34 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ran
𝐺 ⊆
ℝ+ → ran 𝐺 ⊆
ℝ+) |
| 35 | 34 | ssneld 3985 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
𝐺 ⊆
ℝ+ → (¬ 0 ∈ ℝ+ → ¬ 0
∈ ran 𝐺)) |
| 36 | 33, 35 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝐺 ⊆
ℝ+ → ¬ 0 ∈ ran 𝐺) |
| 37 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . 18
⊢ (0
∉ ran 𝐺 ↔ ¬
0 ∈ ran 𝐺) |
| 38 | 36, 37 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
𝐺 ⊆
ℝ+ → 0 ∉ ran 𝐺) |
| 39 | 32, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐴⟶ℝ+ → 0 ∉
ran 𝐺) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 0
∉ ran 𝐺) |
| 41 | | suppdm 48427 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐺 ∧ 𝐺 ∈ V ∧ 0 ∈ ℝ) ∧ 0
∉ ran 𝐺) →
(𝐺 supp 0) = dom 𝐺) |
| 42 | 27, 30, 31, 40, 41 | syl31anc 1375 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = dom 𝐺) |
| 43 | | fdm 6745 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝐴⟶ℝ+ → dom 𝐺 = 𝐴) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → dom
𝐺 = 𝐴) |
| 45 | 42, 44 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = 𝐴) |
| 46 | 45 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐺 supp 0) = 𝐴) |
| 47 | 46 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 = (𝐺 supp 0)) |
| 48 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐴 = (𝐺 supp 0)) |
| 49 | 48 | eleq2d 2827 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ (𝐺 supp 0))) |
| 50 | 49 | biimpa 476 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ (𝐺 supp 0)) |
| 51 | | refdivmptfv 48467 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑦) = ((𝐹‘𝑦) / (𝐺‘𝑦))) |
| 52 | 25, 50, 51 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹 /f 𝐺)‘𝑦) = ((𝐹‘𝑦) / (𝐺‘𝑦))) |
| 53 | 52 | breq1d 5153 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚 ↔ ((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚)) |
| 54 | 15, 53 | bitr4d 282 |
. . . . 5
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)) |
| 55 | 54 | imbi2d 340 |
. . . 4
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
| 56 | 55 | ralbidva 3176 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) →
(∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
| 57 | 56 | 2rexbidva 3220 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) →
(∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
| 58 | | simp1 1137 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 ⊆
ℝ) |
| 59 | | ssidd 4007 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 ⊆ 𝐴) |
| 60 | | elbigo2 48473 |
. . 3
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) |
| 61 | 19, 58, 5, 59, 60 | syl22anc 839 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) |
| 62 | | refdivmptf 48463 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ) |
| 63 | 23, 62 | syl 17 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ) |
| 64 | 47 | feq2d 6722 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → ((𝐹 /f 𝐺):𝐴⟶ℝ ↔ (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ)) |
| 65 | 63, 64 | mpbird 257 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 /f 𝐺):𝐴⟶ℝ) |
| 66 | | ello12 15552 |
. . 3
⊢ (((𝐹 /f 𝐺):𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → ((𝐹 /f 𝐺) ∈ ≤𝑂(1) ↔
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
| 67 | 65, 58, 66 | syl2anc 584 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → ((𝐹 /f 𝐺) ∈ ≤𝑂(1) ↔
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
| 68 | 57, 61, 67 | 3bitr4d 311 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1))) |