Step | Hyp | Ref
| Expression |
1 | | o1f 14260 |
. . . 4
⊢ (𝐹 ∈ 𝑂(1) →
𝐹:dom 𝐹⟶ℂ) |
2 | | o1bdd 14262 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
3 | 1, 2 | mpdan 702 |
. . 3
⊢ (𝐹 ∈ 𝑂(1) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
4 | 3 | adantr 481 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
5 | | o1f 14260 |
. . . 4
⊢ (𝐺 ∈ 𝑂(1) →
𝐺:dom 𝐺⟶ℂ) |
6 | | o1bdd 14262 |
. . . 4
⊢ ((𝐺 ∈ 𝑂(1) ∧ 𝐺:dom 𝐺⟶ℂ) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
7 | 5, 6 | mpdan 702 |
. . 3
⊢ (𝐺 ∈ 𝑂(1) →
∃𝑏 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
8 | 7 | adantl 482 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
∃𝑏 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
9 | | reeanv 3107 |
. . 3
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ (∃𝑚 ∈
ℝ ∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
10 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑚 ∈
ℝ ∃𝑛 ∈
ℝ (∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
11 | | inss1 3833 |
. . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
12 | | ssralv 3666 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
14 | | inss2 3834 |
. . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
15 | | ssralv 3666 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → (∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
17 | 13, 16 | anim12i 590 |
. . . . . . . 8
⊢
((∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
18 | | r19.26 3064 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
19 | 17, 18 | sylibr 224 |
. . . . . . 7
⊢
((∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
20 | | prth 595 |
. . . . . . . . . 10
⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
21 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑎 ∈
ℝ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑎 ∈
ℝ) |
23 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑏 ∈
ℝ) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑏 ∈
ℝ) |
25 | | o1dm 14261 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ 𝑂(1) → dom
𝐹 ⊆
ℝ) |
26 | 25 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐹 ⊆
ℝ) |
27 | 11, 26 | syl5ss 3614 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(dom 𝐹 ∩ dom 𝐺) ⊆
ℝ) |
28 | 27 | sselda 3603 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑧 ∈
ℝ) |
29 | | maxle 12022 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
30 | 22, 24, 28, 29 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
31 | 30 | biimpd 219 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
32 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐹:dom 𝐹⟶ℂ) |
33 | 11 | sseli 3599 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹) |
34 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
35 | 32, 33, 34 | syl2an 494 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (𝐹‘𝑧) ∈ ℂ) |
36 | 5 | ad3antlr 767 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐺:dom 𝐺⟶ℂ) |
37 | 14 | sseli 3599 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺) |
38 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) |
39 | 36, 37, 38 | syl2an 494 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (𝐺‘𝑧) ∈ ℂ) |
40 | | o1of2.3 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) |
41 | 40 | ralrimivva 2971 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) →
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) |
42 | 41 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) |
43 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧))) |
44 | 43 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
45 | 44 | anbi1d 741 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛))) |
46 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝐹‘𝑧) → (𝑥𝑅𝑦) = ((𝐹‘𝑧)𝑅𝑦)) |
47 | 46 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦))) |
48 | 47 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)) |
49 | 45, 48 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))) |
50 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧))) |
51 | 50 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
52 | 51 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
53 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧))) |
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
55 | 54 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
56 | 52, 55 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))) |
57 | 49, 56 | rspc2va 3323 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
58 | 35, 39, 42, 57 | syl21anc 1325 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
59 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
60 | 32, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐹 Fn dom 𝐹) |
61 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺) |
62 | 36, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐺 Fn dom 𝐺) |
63 | | reex 10027 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
64 | | ssexg 4804 |
. . . . . . . . . . . . . . . 16
⊢ ((dom
𝐹 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐹 ∈ V) |
65 | 26, 63, 64 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐹 ∈
V) |
66 | | dmexg 7097 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ 𝑂(1) → dom
𝐺 ∈
V) |
67 | 66 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐺 ∈
V) |
68 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
69 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
70 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
71 | 60, 62, 65, 67, 68, 69, 70 | ofval 6906 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → ((𝐹 ∘𝑓
𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧))) |
72 | 71 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(abs‘((𝐹
∘𝑓 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
73 | 72 | breq1d 4663 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
((abs‘((𝐹
∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
74 | 58, 73 | sylibrd 249 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀)) |
75 | 31, 74 | imim12d 81 |
. . . . . . . . . 10
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀))) |
76 | 20, 75 | syl5 34 |
. . . . . . . . 9
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀))) |
77 | 76 | ralimdva 2962 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(∀𝑧 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀))) |
78 | | o1of2.2 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ) |
79 | 78 | adantl 482 |
. . . . . . . . . 10
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ (𝑥
∈ ℂ ∧ 𝑦
∈ ℂ)) → (𝑥𝑅𝑦) ∈ ℂ) |
80 | 79, 32, 36, 65, 67, 68 | off 6912 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(𝐹
∘𝑓 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ) |
81 | 23, 21 | ifcld 4131 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
82 | | o1of2.1 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈
ℝ) |
83 | 82 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑀 ∈
ℝ) |
84 | | elo12r 14259 |
. . . . . . . . . 10
⊢ ((((𝐹 ∘𝑓
𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1)) |
85 | 84 | 3expia 1267 |
. . . . . . . . 9
⊢ ((((𝐹 ∘𝑓
𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
86 | 80, 27, 81, 83, 85 | syl22anc 1327 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(∀𝑧 ∈ (dom
𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
87 | 77, 86 | syld 47 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(∀𝑧 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
88 | 19, 87 | syl5 34 |
. . . . . 6
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
((∀𝑧 ∈ dom
𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
89 | 88 | rexlimdvva 3038 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) →
(∃𝑚 ∈ ℝ
∃𝑛 ∈ ℝ
(∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
90 | 10, 89 | syl5bir 233 |
. . . 4
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) →
((∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
91 | 90 | rexlimdvva 3038 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
(∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
(∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
92 | 9, 91 | syl5bir 233 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
((∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘𝑓 𝑅𝐺) ∈ 𝑂(1))) |
93 | 4, 8, 92 | mp2and 715 |
1
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
(𝐹
∘𝑓 𝑅𝐺) ∈ 𝑂(1)) |