| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | o1f 15565 | . . . 4
⊢ (𝐹 ∈ 𝑂(1) →
𝐹:dom 𝐹⟶ℂ) | 
| 2 |  | o1bdd 15567 | . . . 4
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) | 
| 3 | 1, 2 | mpdan 687 | . . 3
⊢ (𝐹 ∈ 𝑂(1) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) | 
| 4 | 3 | adantr 480 | . 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) | 
| 5 |  | o1f 15565 | . . . 4
⊢ (𝐺 ∈ 𝑂(1) →
𝐺:dom 𝐺⟶ℂ) | 
| 6 |  | o1bdd 15567 | . . . 4
⊢ ((𝐺 ∈ 𝑂(1) ∧ 𝐺:dom 𝐺⟶ℂ) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) | 
| 7 | 5, 6 | mpdan 687 | . . 3
⊢ (𝐺 ∈ 𝑂(1) →
∃𝑏 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) | 
| 8 | 7 | adantl 481 | . 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
∃𝑏 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) | 
| 9 |  | reeanv 3229 | . . 3
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ (∃𝑚 ∈
ℝ ∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 10 |  | reeanv 3229 | . . . . 5
⊢
(∃𝑚 ∈
ℝ ∃𝑛 ∈
ℝ (∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 11 |  | inss1 4237 | . . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 | 
| 12 |  | ssralv 4052 | . . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))) | 
| 13 | 11, 12 | ax-mp 5 | . . . . . . . . 9
⊢
(∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)) | 
| 14 |  | inss2 4238 | . . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 | 
| 15 |  | ssralv 4052 | . . . . . . . . . 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 613 | . . . . . . . 8
⊢
((∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 18 |  | r19.26 3111 | . . . . . . . 8
⊢
(∀𝑧 ∈
(dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 19 | 17, 18 | sylibr 234 | . . . . . . 7
⊢
((∀𝑧 ∈
dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 20 |  | anim12 809 | . . . . . . . . . 10
⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 21 |  | simplrl 777 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑎 ∈
ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑎 ∈
ℝ) | 
| 23 |  | simplrr 778 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑏 ∈
ℝ) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑏 ∈
ℝ) | 
| 25 |  | o1dm 15566 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ 𝑂(1) → dom
𝐹 ⊆
ℝ) | 
| 26 | 25 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐹 ⊆
ℝ) | 
| 27 | 11, 26 | sstrid 3995 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(dom 𝐹 ∩ dom 𝐺) ⊆
ℝ) | 
| 28 | 27 | sselda 3983 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → 𝑧 ∈
ℝ) | 
| 29 |  | maxle 13233 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) | 
| 30 | 22, 24, 28, 29 | syl3anc 1373 | . . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) | 
| 31 | 30 | biimpd 229 | . . . . . . . . . . 11
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) | 
| 32 | 1 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐹:dom 𝐹⟶ℂ) | 
| 33 | 11 | sseli 3979 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹) | 
| 34 |  | ffvelcdm 7101 | . . . . . . . . . . . . . 14
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) | 
| 35 | 32, 33, 34 | syl2an 596 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (𝐹‘𝑧) ∈ ℂ) | 
| 36 | 5 | ad3antlr 731 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐺:dom 𝐺⟶ℂ) | 
| 37 | 14 | sseli 3979 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺) | 
| 38 |  | ffvelcdm 7101 | . . . . . . . . . . . . . 14
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ) | 
| 39 | 36, 37, 38 | syl2an 596 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → (𝐺‘𝑧) ∈ ℂ) | 
| 40 |  | o1of2.3 | . . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) | 
| 41 | 40 | ralrimivva 3202 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) →
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) | 
| 42 | 41 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) | 
| 43 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧))) | 
| 44 | 43 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚)) | 
| 45 | 44 | anbi1d 631 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛))) | 
| 46 |  | fvoveq1 7454 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦))) | 
| 47 | 46 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)) | 
| 48 | 45, 47 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))) | 
| 49 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧))) | 
| 50 | 49 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛)) | 
| 51 | 50 | anbi2d 630 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛))) | 
| 52 |  | oveq2 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧))) | 
| 53 | 52 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) | 
| 54 | 53 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) | 
| 55 | 51, 54 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))) | 
| 56 | 48, 55 | rspc2va 3634 | . . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ
(((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) | 
| 57 | 35, 39, 42, 56 | syl21anc 838 | . . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) | 
| 58 | 32 | ffnd 6737 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐹 Fn dom 𝐹) | 
| 59 | 36 | ffnd 6737 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝐺 Fn dom 𝐺) | 
| 60 |  | reex 11246 | . . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V | 
| 61 |  | ssexg 5323 | . . . . . . . . . . . . . . . 16
⊢ ((dom
𝐹 ⊆ ℝ ∧
ℝ ∈ V) → dom 𝐹 ∈ V) | 
| 62 | 26, 60, 61 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐹 ∈
V) | 
| 63 |  | dmexg 7923 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ 𝑂(1) → dom
𝐺 ∈
V) | 
| 64 | 63 | ad3antlr 731 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
dom 𝐺 ∈
V) | 
| 65 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) | 
| 66 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧)) | 
| 67 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧)) | 
| 68 | 58, 59, 62, 64, 65, 66, 67 | ofval 7708 | . . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) → ((𝐹 ∘f 𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧))) | 
| 69 | 68 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
(abs‘((𝐹
∘f 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) | 
| 70 | 69 | breq1d 5153 | . . . . . . . . . . . 12
⊢
(((((𝐹 ∈
𝑂(1) ∧ 𝐺 ∈
𝑂(1)) ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) ∧ (𝑚
∈ ℝ ∧ 𝑛
∈ ℝ)) ∧ 𝑧
∈ (dom 𝐹 ∩ dom
𝐺)) →
((abs‘((𝐹
∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)) | 
| 71 | 57, 70 | sylibrd 259 | . . . . . . . . . . 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 3167 | . . . . . . . 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 7715 | . . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
(𝐹 ∘f
𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ) | 
| 78 | 23, 21 | ifcld 4572 | . . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) | 
| 79 |  | o1of2.1 | . . . . . . . . . 10
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈
ℝ) | 
| 80 | 79 | adantl 481 | . . . . . . . . 9
⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) ∧
(𝑚 ∈ ℝ ∧
𝑛 ∈ ℝ)) →
𝑀 ∈
ℝ) | 
| 81 |  | elo12r 15564 | . . . . . . . . . 10
⊢ ((((𝐹 ∘f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1)) | 
| 82 | 81 | 3expia 1122 | . . . . . . . . 9
⊢ ((((𝐹 ∘f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) | 
| 83 | 77, 27, 78, 80, 82 | syl22anc 839 | . . . . . . . 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 3213 | . . . . 5
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) →
(∃𝑚 ∈ ℝ
∃𝑛 ∈ ℝ
(∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) | 
| 87 | 10, 86 | biimtrrid 243 | . . . 4
⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧
(𝑎 ∈ ℝ ∧
𝑏 ∈ ℝ)) →
((∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) | 
| 88 | 87 | rexlimdvva 3213 | . . 3
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
(∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
(∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) | 
| 89 | 9, 88 | biimtrrid 243 | . 2
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
((∃𝑎 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘f 𝑅𝐺) ∈ 𝑂(1))) | 
| 90 | 4, 8, 89 | mp2and 699 | 1
⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) →
(𝐹 ∘f
𝑅𝐺) ∈ 𝑂(1)) |