Step | Hyp | Ref
| Expression |
1 | | o1f 14108 |
. . . . 5
⊢ (𝐹 ∈ 𝑂(1) →
𝐹:dom 𝐹⟶ℂ) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐹:dom 𝐹⟶ℂ) |
3 | | ffn 5958 |
. . . 4
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
4 | 2, 3 | syl 17 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐹 Fn dom 𝐹) |
5 | | rlimf 14080 |
. . . . 5
⊢ (𝐺 ⇝𝑟 0
→ 𝐺:dom 𝐺⟶ℂ) |
6 | 5 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺:dom 𝐺⟶ℂ) |
7 | | ffn 5958 |
. . . 4
⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺) |
8 | 6, 7 | syl 17 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺 Fn dom 𝐺) |
9 | | o1dm 14109 |
. . . . 5
⊢ (𝐹 ∈ 𝑂(1) → dom
𝐹 ⊆
ℝ) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐹 ⊆
ℝ) |
11 | | reex 9906 |
. . . 4
⊢ ℝ
∈ V |
12 | | ssexg 4732 |
. . . 4
⊢ ((dom
𝐹 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐹 ∈ V) |
13 | 10, 11, 12 | sylancl 693 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐹 ∈
V) |
14 | | rlimss 14081 |
. . . . 5
⊢ (𝐺 ⇝𝑟 0
→ dom 𝐺 ⊆
ℝ) |
15 | 14 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐺 ⊆
ℝ) |
16 | | ssexg 4732 |
. . . 4
⊢ ((dom
𝐺 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐺 ∈ V) |
17 | 15, 11, 16 | sylancl 693 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ dom 𝐺 ∈
V) |
18 | | eqid 2610 |
. . 3
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
19 | | eqidd 2611 |
. . 3
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
20 | | eqidd 2611 |
. . 3
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
21 | 4, 8, 13, 17, 18, 19, 20 | offval 6802 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝐹
∘𝑓 · 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))) |
22 | | o1bdd 14110 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
23 | 1, 22 | mpdan 699 |
. . . . . 6
⊢ (𝐹 ∈ 𝑂(1) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
24 | 23 | ad2antrr 758 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
25 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐺‘𝑥) ∈ V |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ V) |
27 | 26 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∀𝑥 ∈ dom 𝐺(𝐺‘𝑥) ∈ V) |
28 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑦 ∈ ℝ+) |
29 | | recn 9905 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℝ → 𝑚 ∈
ℂ) |
30 | 29 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑚 ∈ ℂ) |
31 | 30 | abscld 14023 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (abs‘𝑚) ∈
ℝ) |
32 | 30 | absge0d 14031 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 0 ≤
(abs‘𝑚)) |
33 | 31, 32 | ge0p1rpd 11778 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈
ℝ+) |
34 | 28, 33 | rpdivcld 11765 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦 / ((abs‘𝑚) + 1)) ∈
ℝ+) |
35 | 6 | feqmptd 6159 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
36 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ 𝐺
⇝𝑟 0) |
37 | 35, 36 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ⇝𝑟
0) |
38 | 37 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ⇝𝑟
0) |
39 | 27, 34, 38 | rlimi 14092 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) |
40 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
41 | | ssralv 3629 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)) |
43 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
44 | | ssralv 3629 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → (∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) |
46 | 42, 45 | anim12i 588 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
47 | | r19.26 3046 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) ↔ (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
48 | 46, 47 | sylibr 223 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
49 | | prth 593 |
. . . . . . . . . . . 12
⊢ (((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
50 | 49 | ralimi 2936 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))) |
52 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑎 ∈ ℝ) |
53 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑏 ∈ ℝ) |
54 | 40, 10 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (dom 𝐹 ∩ dom
𝐺) ⊆
ℝ) |
55 | 54 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) |
56 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) |
57 | 55, 56 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ ℝ) |
58 | | maxle 11896 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥))) |
59 | 52, 53, 57, 58 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥))) |
60 | 59 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥))) |
61 | 6 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐺:dom 𝐺⟶ℂ) |
62 | 43 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
63 | 62 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐺) |
64 | 61, 63 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐺‘𝑥) ∈ ℂ) |
65 | 64 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐺‘𝑥) − 0) = (𝐺‘𝑥)) |
66 | 65 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐺‘𝑥) − 0)) = (abs‘(𝐺‘𝑥))) |
67 | 66 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) ↔ (abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)))) |
68 | 64 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐺‘𝑥)) ∈ ℝ) |
69 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈
ℝ+) |
70 | 69 | rpred 11748 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ) |
71 | | ltle 10005 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ) →
((abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))) |
72 | 68, 70, 71 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))) |
73 | 67, 72 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))) |
74 | 73 | anim2d 587 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))) |
75 | 2 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐹:dom 𝐹⟶ℂ) |
76 | 40 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
77 | 76 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐹) |
78 | 75, 77 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐹‘𝑥) ∈ ℂ) |
79 | 78 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
80 | 78 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐹‘𝑥))) |
81 | 79, 80 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐹‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐹‘𝑥)))) |
82 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℝ) |
83 | 64 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐺‘𝑥))) |
84 | 68, 83 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑥)))) |
85 | | lemul12a 10760 |
. . . . . . . . . . . . . . . 16
⊢
(((((abs‘(𝐹‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐹‘𝑥))) ∧ 𝑚 ∈ ℝ) ∧ (((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑥))) ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ)) →
(((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))) |
86 | 81, 82, 84, 70, 85 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))) |
87 | 78, 64 | absmuld 14041 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) = ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥)))) |
88 | 87 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ↔ ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))) |
89 | 82 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℂ) |
90 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ+) |
91 | 90 | rpcnd 11750 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℂ) |
92 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈
ℝ+) |
93 | 92 | rpcnd 11750 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℂ) |
94 | 92 | rpne0d 11753 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ≠ 0) |
95 | 89, 91, 93, 94 | divassd 10715 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) = (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))) |
96 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((abs‘𝑚)
∈ ℝ → ((abs‘𝑚) + 1) ∈ ℝ) |
97 | 31, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈
ℝ) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℝ) |
99 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) ∈ ℝ) |
100 | 82 | leabsd 14001 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ≤ (abs‘𝑚)) |
101 | 99 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) < ((abs‘𝑚) + 1)) |
102 | 82, 99, 98, 100, 101 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 < ((abs‘𝑚) + 1)) |
103 | 82, 98, 90, 102 | ltmul1dd 11803 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦)) |
104 | 90 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ) |
105 | 82, 104 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) ∈ ℝ) |
106 | 105, 104,
92 | ltdivmuld 11799 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦 ↔ (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦))) |
107 | 103, 106 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦) |
108 | 95, 107 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) |
109 | 78, 64 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
110 | 109 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ ℝ) |
111 | 82, 70 | remulcld 9949 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ) |
112 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ ℝ ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
113 | 110, 111,
104, 112 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
114 | 108, 113 | mpan2d 706 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
115 | 88, 114 | sylbird 249 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
116 | 74, 86, 115 | 3syld 58 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
117 | 60, 116 | imim12d 79 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
118 | 117 | anassrs 678 |
. . . . . . . . . . . 12
⊢
((((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
119 | 118 | ralimdva 2945 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
(∀𝑥 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
120 | | simpr 476 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑏 ∈
ℝ) |
121 | | simplrl 796 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑎 ∈
ℝ) |
122 | 120, 121 | ifcld 4081 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
123 | 119, 122 | jctild 564 |
. . . . . . . . . 10
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
(∀𝑥 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))) |
124 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → (𝑧 ≤ 𝑥 ↔ if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥)) |
125 | 124 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → ((𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦) ↔ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
126 | 125 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦) ↔ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
127 | 126 | rspcev 3282 |
. . . . . . . . . 10
⊢
((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
128 | 51, 123, 127 | syl56 35 |
. . . . . . . . 9
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
((∀𝑥 ∈ dom
𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
129 | 128 | expcomd 453 |
. . . . . . . 8
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺
⇝𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) →
(∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))) |
130 | 129 | rexlimdva 3013 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))) |
131 | 39, 130 | mpd 15 |
. . . . . 6
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
132 | 131 | rexlimdvva 3020 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) → (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
133 | 24, 132 | mpd 15 |
. . . 4
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑦 ∈
ℝ+) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
134 | 133 | ralrimiva 2949 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ ∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) |
135 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
136 | 2, 76, 135 | syl2an 493 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
137 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
138 | 6, 62, 137 | syl2an 493 |
. . . . . 6
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
139 | 136, 138 | mulcld 9939 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
140 | 139 | ralrimiva 2949 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ ∀𝑥 ∈
(dom 𝐹 ∩ dom 𝐺)((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
141 | 140, 54 | rlim0 14087 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ ((𝑥 ∈ (dom
𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇝𝑟 0 ↔
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))) |
142 | 134, 141 | mpbird 246 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇝𝑟
0) |
143 | 21, 142 | eqbrtrd 4605 |
1
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0)
→ (𝐹
∘𝑓 · 𝐺) ⇝𝑟
0) |