Step | Hyp | Ref
| Expression |
1 | | o1f 15166 |
. . . 4
⊢ (𝐹 ∈ 𝑂(1) →
𝐹:dom 𝐹⟶ℂ) |
2 | | o1bdd 15168 |
. . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
3 | 1, 2 | mpdan 683 |
. . 3
⊢ (𝐹 ∈ 𝑂(1) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
4 | 3 | adantr 480 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
5 | | o1f 15166 |
. . . 4
⊢ (𝐺 ∈ 𝑂(1) →
𝐺:dom 𝐺⟶ℂ) |
6 | | o1bdd 15168 |
. . . 4
⊢ ((𝐺 ∈ 𝑂(1) ∧ 𝐺:dom 𝐺⟶ℂ) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
7 | 5, 6 | mpdan 683 |
. . 3
⊢ (𝐺 ∈ 𝑂(1) →
∃𝑏 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
8 | 7 | adantl 481 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
∃𝑏 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
9 | | reeanv 3292 |
. . 3
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ (∃𝑚 ∈
ℝ ∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
10 | | reeanv 3292 |
. . . . 5
⊢
(∃𝑚 ∈
ℝ ∃𝑛 ∈
ℝ (∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
11 | | inss1 4159 |
. . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
12 | | ssralv 3983 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
14 | | inss2 4160 |
. . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
15 | | ssralv 3983 |
. . . . . . . . . 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 612 |
. . . . . . . 8
⊢
((∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
18 | | r19.26 3094 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
19 | 17, 18 | sylibr 233 |
. . . . . . 7
⊢
((∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
20 | | anim12 805 |
. . . . . . . . . 10
⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
21 | | simplrl 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑎 ∈
ℝ) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑎 ∈
ℝ) |
23 | | simplrr 774 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑏 ∈
ℝ) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑏 ∈
ℝ) |
25 | | o1dm 15167 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ 𝑂(1) → dom
𝐹 ⊆
ℝ) |
26 | 25 | ad3antrrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐹 ⊆
ℝ) |
27 | 11, 26 | sstrid 3928 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(dom 𝐹 ∩ dom 𝐺) ⊆
ℝ) |
28 | 27 | sselda 3917 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑧 ∈
ℝ) |
29 | | maxle 12854 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
30 | 22, 24, 28, 29 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
31 | 30 | biimpd 228 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
32 | 1 | ad3antrrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐹:dom 𝐹⟶ℂ) |
33 | 11 | sseli 3913 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹) |
34 | | ffvelrn 6941 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
35 | 32, 33, 34 | syl2an 595 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (𝐹‘𝑧) ∈ ℂ) |
36 | 5 | ad3antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐺:dom 𝐺⟶ℂ) |
37 | 14 | sseli 3913 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺) |
38 | | ffvelrn 6941 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) |
39 | 36, 37, 38 | syl2an 595 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (𝐺‘𝑧) ∈ ℂ) |
40 | | o1of2.3 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) |
41 | 40 | ralrimivva 3114 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) →
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) |
42 | 41 | ad2antlr 723 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) |
43 | | fveq2 6756 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧))) |
44 | 43 | breq1d 5080 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚)) |
45 | 44 | anbi1d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛))) |
46 | | fvoveq1 7278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦))) |
47 | 46 | breq1d 5080 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)) |
48 | 45, 47 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))) |
49 | | fveq2 6756 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧))) |
50 | 49 | breq1d 5080 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛)) |
51 | 50 | anbi2d 628 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛))) |
52 | | oveq2 7263 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧))) |
53 | 52 | fveq2d 6760 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
54 | 53 | breq1d 5080 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
55 | 51, 54 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))) |
56 | 48, 55 | rspc2va 3563 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
57 | 35, 39, 42, 56 | syl21anc 834 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
58 | 32 | ffnd 6585 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐹 Fn dom 𝐹) |
59 | 36 | ffnd 6585 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐺 Fn dom 𝐺) |
60 | | reex 10893 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
61 | | ssexg 5242 |
. . . . . . . . . . . . . . . 16
⊢ ((dom
𝐹 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐹 ∈ V) |
62 | 26, 60, 61 | sylancl 585 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐹 ∈
V) |
63 | | dmexg 7724 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ 𝑂(1) → dom
𝐺 ∈
V) |
64 | 63 | ad3antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐺 ∈
V) |
65 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
66 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
67 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
68 | 58, 59, 62, 64, 65, 66, 67 | ofval 7522 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → ((𝐹 ∘f 𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧))) |
69 | 68 | fveq2d 6760 |
. . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(abs‘((𝐹
∘f 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
70 | 69 | breq1d 5080 |
. . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
((abs‘((𝐹
∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) |
71 | 57, 70 | sylibrd 258 |
. . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀)) |
72 | 31, 71 | imim12d 81 |
. . . . . . . . . 10
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀))) |
73 | 20, 72 | syl5 34 |
. . . . . . . . 9
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀))) |
74 | 73 | ralimdva 3102 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(∀𝑧 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀))) |
75 | | o1of2.2 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ) |
76 | 75 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ (𝑥
∈ ℂ ∧ 𝑦
∈ ℂ)) → (𝑥𝑅𝑦) ∈ ℂ) |
77 | 76, 32, 36, 62, 64, 65 | off 7529 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(𝐹 ∘f
𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ) |
78 | 23, 21 | ifcld 4502 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
79 | | o1of2.1 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈
ℝ) |
80 | 79 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑀 ∈
ℝ) |
81 | | elo12r 15165 |
. . . . . . . . . 10
⊢ ((((𝐹 ∘f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1)) |
82 | 81 | 3expia 1119 |
. . . . . . . . 9
⊢ ((((𝐹 ∘f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
83 | 77, 27, 78, 80, 82 | syl22anc 835 |
. . . . . . . 8
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(∀𝑧 ∈ (dom
𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
84 | 74, 83 | syld 47 |
. . . . . . 7
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(∀𝑧 ∈ (dom
𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
85 | 19, 84 | syl5 34 |
. . . . . 6
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
((∀𝑧 ∈ dom
𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
86 | 85 | rexlimdvva 3222 |
. . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) →
(∃𝑚 ∈ ℝ
∃𝑛 ∈ ℝ
(∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
87 | 10, 86 | syl5bir 242 |
. . . 4
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) →
((∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
88 | 87 | rexlimdvva 3222 |
. . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
(∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
(∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
89 | 9, 88 | syl5bir 242 |
. 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
((∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) |
90 | 4, 8, 89 | mp2and 695 |
1
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
(𝐹 ∘f
𝑅𝐺) ∈ 𝑂(1)) |