| Step | Hyp | Ref
| Expression |
| 1 | | o1f 15565 |
. . . . 5
⊢ (𝐹 ∈ 𝑂(1) →
𝐹:dom 𝐹⟶ℂ) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐹:dom 𝐹⟶ℂ) |
| 3 | 2 | ffnd 6737 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐹 Fn dom 𝐹) |
| 4 | | rlimf 15537 |
. . . . 5
⊢ (𝐺 ⇝𝑟 0
→ 𝐺:dom 𝐺⟶ℂ) |
| 5 | 4 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺:dom 𝐺⟶ℂ) |
| 6 | 5 | ffnd 6737 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺 Fn dom 𝐺) |
| 7 | | o1dm 15566 |
. . . . 5
⊢ (𝐹 ∈ 𝑂(1) → dom
𝐹 ⊆
ℝ) |
| 8 | 7 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐹 ⊆
ℝ) |
| 9 | | reex 11246 |
. . . 4
⊢ ℝ
∈ V |
| 10 | | ssexg 5323 |
. . . 4
⊢ ((dom
𝐹 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐹 ∈ V) |
| 11 | 8, 9, 10 | sylancl 586 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐹 ∈
V) |
| 12 | | rlimss 15538 |
. . . . 5
⊢ (𝐺 ⇝𝑟 0
→ dom 𝐺 ⊆
ℝ) |
| 13 | 12 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐺 ⊆
ℝ) |
| 14 | | ssexg 5323 |
. . . 4
⊢ ((dom
𝐺 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐺 ∈ V) |
| 15 | 13, 9, 14 | sylancl 586 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐺 ∈
V) |
| 16 | | eqid 2737 |
. . 3
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
| 17 | | eqidd 2738 |
. . 3
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
| 18 | | eqidd 2738 |
. . 3
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
| 19 | 3, 6, 11, 15, 16, 17, 18 | offval 7706 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝐹
∘f · 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))) |
| 20 | | o1bdd 15567 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
| 21 | 1, 20 | mpdan 687 |
. . . . . 6
⊢ (𝐹 ∈ 𝑂(1) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
| 22 | 21 | ad2antrr 726 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
| 23 | | fvexd 6921 |
. . . . . . . . 9
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ V) |
| 24 | 23 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∀𝑥 ∈ dom 𝐺(𝐺‘𝑥) ∈ V) |
| 25 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑦 ∈ ℝ+) |
| 26 | | recn 11245 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℝ → 𝑚 ∈
ℂ) |
| 27 | 26 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑚 ∈ ℂ) |
| 28 | 27 | abscld 15475 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (abs‘𝑚) ∈
ℝ) |
| 29 | 27 | absge0d 15483 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 0 ≤
(abs‘𝑚)) |
| 30 | 28, 29 | ge0p1rpd 13107 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈
ℝ+) |
| 31 | 25, 30 | rpdivcld 13094 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦 / ((abs‘𝑚) + 1)) ∈
ℝ+) |
| 32 | 5 | feqmptd 6977 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
| 33 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺
⇝𝑟 0) |
| 34 | 32, 33 | eqbrtrrd 5167 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ⇝𝑟
0) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ⇝𝑟
0) |
| 36 | 24, 31, 35 | rlimi 15549 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) |
| 37 | | inss1 4237 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
| 38 | | ssralv 4052 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚))) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
| 40 | | inss2 4238 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
| 41 | | ssralv 4052 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → (∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) |
| 43 | 39, 42 | anim12i 613 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 44 | | r19.26 3111 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) ↔ (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 45 | 43, 44 | sylibr 234 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 46 | | anim12 809 |
. . . . . . . . . . . 12
⊢ (((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 47 | 46 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 48 | 45, 47 | syl 17 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
| 49 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑎 ∈ ℝ) |
| 50 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑏 ∈ ℝ) |
| 51 | 37, 8 | sstrid 3995 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (dom 𝐹 ∩ dom
𝐺) ⊆
ℝ) |
| 52 | 51 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) |
| 53 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) |
| 54 | 52, 53 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ ℝ) |
| 55 | | maxle 13233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥))) |
| 56 | 49, 50, 54, 55 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥))) |
| 57 | 56 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥))) |
| 58 | 5 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐺:dom 𝐺⟶ℂ) |
| 59 | 40 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
| 60 | 59 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐺) |
| 61 | 58, 60 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐺‘𝑥) ∈ ℂ) |
| 62 | 61 | subid1d 11609 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐺‘𝑥) − 0) = (𝐺‘𝑥)) |
| 63 | 62 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐺‘𝑥) − 0)) = (abs‘(𝐺‘𝑥))) |
| 64 | 63 | breq1d 5153 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) ↔ (abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)))) |
| 65 | 61 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐺‘𝑥)) ∈ ℝ) |
| 66 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈
ℝ+) |
| 67 | 66 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ) |
| 68 | | ltle 11349 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ) →
((abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))) |
| 69 | 65, 67, 68 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))) |
| 70 | 64, 69 | sylbid 240 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))) |
| 71 | 70 | anim2d 612 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))) |
| 72 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐹:dom 𝐹⟶ℂ) |
| 73 | 37 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
| 74 | 73 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐹) |
| 75 | 72, 74 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐹‘𝑥) ∈ ℂ) |
| 76 | 75 | abscld 15475 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
| 77 | 75 | absge0d 15483 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐹‘𝑥))) |
| 78 | 76, 77 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐹‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐹‘𝑥)))) |
| 79 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℝ) |
| 80 | 61 | absge0d 15483 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐺‘𝑥))) |
| 81 | 65, 80 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑥)))) |
| 82 | | lemul12a 12125 |
. . . . . . . . . . . . . . . 16
⊢
(((((abs‘(𝐹‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐹‘𝑥))) ∧ 𝑚 ∈ ℝ) ∧ (((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑥))) ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ)) →
(((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))) |
| 83 | 78, 79, 81, 67, 82 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))) |
| 84 | 75, 61 | absmuld 15493 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) = ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥)))) |
| 85 | 84 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ↔ ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))) |
| 86 | 79 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℂ) |
| 87 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ+) |
| 88 | 87 | rpcnd 13079 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℂ) |
| 89 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈
ℝ+) |
| 90 | 89 | rpcnd 13079 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℂ) |
| 91 | 89 | rpne0d 13082 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ≠ 0) |
| 92 | 86, 88, 90, 91 | divassd 12078 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) = (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))) |
| 93 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((abs‘𝑚)
∈ ℝ → ((abs‘𝑚) + 1) ∈ ℝ) |
| 94 | 28, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈
ℝ) |
| 95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℝ) |
| 96 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) ∈ ℝ) |
| 97 | 79 | leabsd 15453 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ≤ (abs‘𝑚)) |
| 98 | 96 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) < ((abs‘𝑚) + 1)) |
| 99 | 79, 96, 95, 97, 98 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 < ((abs‘𝑚) + 1)) |
| 100 | 79, 95, 87, 99 | ltmul1dd 13132 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦)) |
| 101 | 87 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ) |
| 102 | 79, 101 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) ∈ ℝ) |
| 103 | 102, 101,
89 | ltdivmuld 13128 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦 ↔ (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦))) |
| 104 | 100, 103 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦) |
| 105 | 92, 104 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) |
| 106 | 75, 61 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
| 107 | 106 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ ℝ) |
| 108 | 79, 67 | remulcld 11291 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ) |
| 109 | | lelttr 11351 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ ℝ ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 110 | 107, 108,
101, 109 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 111 | 105, 110 | mpan2d 694 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 112 | 85, 111 | sylbird 260 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 113 | 71, 83, 112 | 3syld 60 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 114 | 57, 113 | imim12d 81 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 115 | 114 | anassrs 467 |
. . . . . . . . . . . 12
⊢
((((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 116 | 115 | ralimdva 3167 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
(∀𝑥 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 117 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑏 ∈
ℝ) |
| 118 | | simplrl 777 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑎 ∈
ℝ) |
| 119 | 117, 118 | ifcld 4572 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
| 120 | 116, 119 | jctild 525 |
. . . . . . . . . 10
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
(∀𝑥 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))) |
| 121 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → (𝑧 ≤ 𝑥 ↔ if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥)) |
| 122 | 121 | rspceaimv 3628 |
. . . . . . . . . 10
⊢
((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 123 | 48, 120, 122 | syl56 36 |
. . . . . . . . 9
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
((∀𝑥 ∈ dom
𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 124 | 123 | expcomd 416 |
. . . . . . . 8
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
(∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))) |
| 125 | 124 | rexlimdva 3155 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))) |
| 126 | 36, 125 | mpd 15 |
. . . . . 6
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 127 | 126 | rexlimdvva 3213 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) → (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 128 | 22, 127 | mpd 15 |
. . . 4
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 129 | 128 | ralrimiva 3146 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ ∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
| 130 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
| 131 | 2, 73, 130 | syl2an 596 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
| 132 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
| 133 | 5, 59, 132 | syl2an 596 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
| 134 | 131, 133 | mulcld 11281 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
| 135 | 134 | ralrimiva 3146 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ ∀𝑥 ∈
(dom 𝐹 ∩ dom 𝐺)((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
| 136 | 135, 51 | rlim0 15544 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ ((𝑥 ∈ (dom
𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇝𝑟 0 ↔
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
| 137 | 129, 136 | mpbird 257 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇝𝑟
0) |
| 138 | 19, 137 | eqbrtrd 5165 |
1
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝐹
∘f · 𝐺) ⇝𝑟
0) |