MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  o1of2 Structured version   Visualization version   GIF version

Theorem o1of2 14272
Description: Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.)
Hypotheses
Ref Expression
o1of2.1 ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)
o1of2.2 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ)
o1of2.3 (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
Assertion
Ref Expression
o1of2 ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1))
Distinct variable groups:   𝑚,𝑛,𝑥,𝑦,𝐹   𝑚,𝐺,𝑛,𝑥,𝑦   𝑅,𝑚,𝑛,𝑥,𝑦   𝑥,𝑀,𝑦
Allowed substitution hints:   𝑀(𝑚,𝑛)

Proof of Theorem o1of2
Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 o1f 14189 . . . 4 (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
2 o1bdd 14191 . . . 4 ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚))
31, 2mpdan 701 . . 3 (𝐹 ∈ 𝑂(1) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚))
43adantr 481 . 2 ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚))
5 o1f 14189 . . . 4 (𝐺 ∈ 𝑂(1) → 𝐺:dom 𝐺⟶ℂ)
6 o1bdd 14191 . . . 4 ((𝐺 ∈ 𝑂(1) ∧ 𝐺:dom 𝐺⟶ℂ) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛))
75, 6mpdan 701 . . 3 (𝐺 ∈ 𝑂(1) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛))
87adantl 482 . 2 ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛))
9 reeanv 3102 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)))
10 reeanv 3102 . . . . 5 (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)))
11 inss1 3816 . . . . . . . . . 10 (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
12 ssralv 3650 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚)))
1311, 12ax-mp 5 . . . . . . . . 9 (∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚))
14 inss2 3817 . . . . . . . . . 10 (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
15 ssralv 3650 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → (∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)))
1614, 15ax-mp 5 . . . . . . . . 9 (∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛))
1713, 16anim12i 589 . . . . . . . 8 ((∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)))
18 r19.26 3062 . . . . . . . 8 (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ (𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) ↔ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)))
1917, 18sylibr 224 . . . . . . 7 ((∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ (𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)))
20 prth 594 . . . . . . . . . 10 (((𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ (𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → ((𝑎𝑧𝑏𝑧) → ((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛)))
21 simplrl 799 . . . . . . . . . . . . . 14 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑎 ∈ ℝ)
2221adantr 481 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑎 ∈ ℝ)
23 simplrr 800 . . . . . . . . . . . . . 14 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑏 ∈ ℝ)
2423adantr 481 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑏 ∈ ℝ)
25 o1dm 14190 . . . . . . . . . . . . . . . 16 (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
2625ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ⊆ ℝ)
2711, 26syl5ss 3599 . . . . . . . . . . . . . 14 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
2827sselda 3588 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑧 ∈ ℝ)
29 maxle 11964 . . . . . . . . . . . . 13 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎𝑧𝑏𝑧)))
3022, 24, 28, 29syl3anc 1323 . . . . . . . . . . . 12 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎𝑧𝑏𝑧)))
3130biimpd 219 . . . . . . . . . . 11 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (𝑎𝑧𝑏𝑧)))
321ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹:dom 𝐹⟶ℂ)
3311sseli 3584 . . . . . . . . . . . . . 14 (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹)
34 ffvelrn 6314 . . . . . . . . . . . . . 14 ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ ℂ)
3532, 33, 34syl2an 494 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹𝑧) ∈ ℂ)
365ad3antlr 766 . . . . . . . . . . . . . 14 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺:dom 𝐺⟶ℂ)
3714sseli 3584 . . . . . . . . . . . . . 14 (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺)
38 ffvelrn 6314 . . . . . . . . . . . . . 14 ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺𝑧) ∈ ℂ)
3936, 37, 38syl2an 494 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺𝑧) ∈ ℂ)
40 o1of2.3 . . . . . . . . . . . . . . 15 (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
4140ralrimivva 2970 . . . . . . . . . . . . . 14 ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
4241ad2antlr 762 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
43 fveq2 6150 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐹𝑧) → (abs‘𝑥) = (abs‘(𝐹𝑧)))
4443breq1d 4628 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹𝑧)) ≤ 𝑚))
4544anbi1d 740 . . . . . . . . . . . . . . 15 (𝑥 = (𝐹𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛)))
46 oveq1 6612 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐹𝑧) → (𝑥𝑅𝑦) = ((𝐹𝑧)𝑅𝑦))
4746fveq2d 6154 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹𝑧)𝑅𝑦)))
4847breq1d 4628 . . . . . . . . . . . . . . 15 (𝑥 = (𝐹𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹𝑧)𝑅𝑦)) ≤ 𝑀))
4945, 48imbi12d 334 . . . . . . . . . . . . . 14 (𝑥 = (𝐹𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹𝑧)𝑅𝑦)) ≤ 𝑀)))
50 fveq2 6150 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐺𝑧) → (abs‘𝑦) = (abs‘(𝐺𝑧)))
5150breq1d 4628 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐺𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺𝑧)) ≤ 𝑛))
5251anbi2d 739 . . . . . . . . . . . . . . 15 (𝑦 = (𝐺𝑧) → (((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛)))
53 oveq2 6613 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐺𝑧) → ((𝐹𝑧)𝑅𝑦) = ((𝐹𝑧)𝑅(𝐺𝑧)))
5453fveq2d 6154 . . . . . . . . . . . . . . . 16 (𝑦 = (𝐺𝑧) → (abs‘((𝐹𝑧)𝑅𝑦)) = (abs‘((𝐹𝑧)𝑅(𝐺𝑧))))
5554breq1d 4628 . . . . . . . . . . . . . . 15 (𝑦 = (𝐺𝑧) → ((abs‘((𝐹𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹𝑧)𝑅(𝐺𝑧))) ≤ 𝑀))
5652, 55imbi12d 334 . . . . . . . . . . . . . 14 (𝑦 = (𝐺𝑧) → ((((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛) → (abs‘((𝐹𝑧)𝑅(𝐺𝑧))) ≤ 𝑀)))
5749, 56rspc2va 3312 . . . . . . . . . . . . 13 ((((𝐹𝑧) ∈ ℂ ∧ (𝐺𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛) → (abs‘((𝐹𝑧)𝑅(𝐺𝑧))) ≤ 𝑀))
5835, 39, 42, 57syl21anc 1322 . . . . . . . . . . . 12 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛) → (abs‘((𝐹𝑧)𝑅(𝐺𝑧))) ≤ 𝑀))
59 ffn 6004 . . . . . . . . . . . . . . . 16 (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹)
6032, 59syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹 Fn dom 𝐹)
61 ffn 6004 . . . . . . . . . . . . . . . 16 (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺)
6236, 61syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺 Fn dom 𝐺)
63 reex 9972 . . . . . . . . . . . . . . . 16 ℝ ∈ V
64 ssexg 4769 . . . . . . . . . . . . . . . 16 ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
6526, 63, 64sylancl 693 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ∈ V)
66 dmexg 7045 . . . . . . . . . . . . . . . 16 (𝐺 ∈ 𝑂(1) → dom 𝐺 ∈ V)
6766ad3antlr 766 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐺 ∈ V)
68 eqid 2626 . . . . . . . . . . . . . . 15 (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
69 eqidd 2627 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹𝑧) = (𝐹𝑧))
70 eqidd 2627 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺𝑧) = (𝐺𝑧))
7160, 62, 65, 67, 68, 69, 70ofval 6860 . . . . . . . . . . . . . 14 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹𝑓 𝑅𝐺)‘𝑧) = ((𝐹𝑧)𝑅(𝐺𝑧)))
7271fveq2d 6154 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) = (abs‘((𝐹𝑧)𝑅(𝐺𝑧))))
7372breq1d 4628 . . . . . . . . . . . 12 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀 ↔ (abs‘((𝐹𝑧)𝑅(𝐺𝑧))) ≤ 𝑀))
7458, 73sylibrd 249 . . . . . . . . . . 11 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛) → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀))
7531, 74imim12d 81 . . . . . . . . . 10 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎𝑧𝑏𝑧) → ((abs‘(𝐹𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺𝑧)) ≤ 𝑛)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
7620, 75syl5 34 . . . . . . . . 9 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ (𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
7776ralimdva 2961 . . . . . . . 8 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ (𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
78 o1of2.2 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ)
7978adantl 482 . . . . . . . . . 10 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥𝑅𝑦) ∈ ℂ)
8079, 32, 36, 65, 67, 68off 6866 . . . . . . . . 9 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝐹𝑓 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ)
8123, 21ifcld 4108 . . . . . . . . 9 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ)
82 o1of2.1 . . . . . . . . . 10 ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)
8382adantl 482 . . . . . . . . 9 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑀 ∈ ℝ)
84 elo12r 14188 . . . . . . . . . 10 ((((𝐹𝑓 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1))
85843expia 1264 . . . . . . . . 9 ((((𝐹𝑓 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
8680, 27, 81, 83, 85syl22anc 1324 . . . . . . . 8 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹𝑓 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
8777, 86syld 47 . . . . . . 7 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ (𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
8819, 87syl5 34 . . . . . 6 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → ((∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
8988rexlimdvva 3036 . . . . 5 (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
9010, 89syl5bir 233 . . . 4 (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → ((∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
9190rexlimdvva 3036 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
929, 91syl5bir 233 . 2 ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ((∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎𝑧 → (abs‘(𝐹𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏𝑧 → (abs‘(𝐺𝑧)) ≤ 𝑛)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1)))
934, 8, 92mp2and 714 1 ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹𝑓 𝑅𝐺) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wral 2912  wrex 2913  Vcvv 3191  cin 3559  wss 3560  ifcif 4063   class class class wbr 4618  dom cdm 5079   Fn wfn 5845  wf 5846  cfv 5850  (class class class)co 6605  𝑓 cof 6849  cc 9879  cr 9880  cle 10020  abscabs 13903  𝑂(1)co1 14146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-pre-lttri 9955  ax-pre-lttrn 9956
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-of 6851  df-er 7688  df-pm 7806  df-en 7901  df-dom 7902  df-sdom 7903  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-ico 12120  df-o1 14150
This theorem is referenced by:  o1add  14273  o1mul  14274  o1sub  14275
  Copyright terms: Public domain W3C validator