o1of2 - Metamath Proof Explorer

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

Theorem o1of2 15586

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)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1))

Distinct variable groups: 𝑚,𝑛,𝑥,𝑦,𝐹 𝑚,𝐺,𝑛,𝑥,𝑦 𝑅,𝑚,𝑛,𝑥,𝑦 𝑥,𝑀,𝑦 Allowed substitution hints: 𝑀(𝑚,𝑛)

Proof of Theorem o1of2 Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		o1f 15502	. . . 4 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
2		o1bdd 15504	. . . 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 15502	. . . 4 ⊢ (𝐺 ∈ 𝑂(1) → 𝐺:dom 𝐺⟶ℂ)
6		o1bdd 15504	. . . 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 3210	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
10		reeanv 3210	. . . . 5 ⊢ (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
11		inss1 4203	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
12		ssralv 4018	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)))
13	11, 12	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
14		inss2 4204	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
15		ssralv 4018	. . . . . . . . . 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 3092	. . . . . . . 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 808	. . . . . . . . . 10 ⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
21		simplrl 776	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑎 ∈ ℝ)
22	21	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑎 ∈ ℝ)
23		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑏 ∈ ℝ)
24	23	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑏 ∈ ℝ)
25		o1dm 15503	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
26	25	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ⊆ ℝ)
27	11, 26	sstrid 3961	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
28	27	sselda 3949	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑧 ∈ ℝ)
29		maxle 13158	. . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹)
34		ffvelcdm 7056	. . . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺)
38		ffvelcdm 7056	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ)
39	36, 37, 38	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑧) ∈ ℂ)
40		o1of2.3	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
41	40	ralrimivva 3181	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
42	41	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
43		fveq2 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧)))
44	43	breq1d 5120	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚))
45	44	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛)))
46		fvoveq1 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦)))
47	46	breq1d 5120	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))
48	45, 47	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)))
49		fveq2 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧)))
50	49	breq1d 5120	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛))
51	50	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
52		oveq2 7398	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
53	52	fveq2d 6865	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
54	53	breq1d 5120	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
55	51, 54	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)))
56	48, 55	rspc2va 3603	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
57	35, 39, 42, 56	syl21anc 837	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
58	32	ffnd 6692	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹 Fn dom 𝐹)
59	36	ffnd 6692	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺 Fn dom 𝐺)
60		reex 11166	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
61		ssexg 5281	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
62	26, 60, 61	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ∈ V)
63		dmexg 7880	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ 𝑂(1) → dom 𝐺 ∈ V)
64	63	ad3antlr 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐺 ∈ V)
65		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
66		eqidd 2731	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧))
67		eqidd 2731	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧))
68	58, 59, 62, 64, 65, 66, 67	ofval 7667	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹 ∘_f 𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
69	68	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
70	69	breq1d 5120	. . . . . . . . . . . 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 3146	. . . . . . . 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 7674	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ)
78	23, 21	ifcld 4538	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ)
79		o1of2.1	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)
80	79	adantl 481	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑀 ∈ ℝ)
81		elo12r 15501	. . . . . . . . . 10 ⊢ ((((𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1))
82	81	3expia 1121	. . . . . . . . 9 ⊢ ((((𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
83	77, 27, 78, 80, 82	syl22anc 838	. . . . . . . 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 3195	. . . . 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 3195	. . 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))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 Vcvv 3450 ∩ cin 3916 ⊆ wss 3917 ifcif 4491 class class class wbr 5110 dom cdm 5641 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 ∘_f cof 7654 ℂcc 11073 ℝcr 11074 ≤ cle 11216 abscabs 15207 𝑂(1)co1 15459

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-pre-lttri 11149 ax-pre-lttrn 11150

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-po 5549 df-so 5550 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-er 8674 df-pm 8805 df-en 8922 df-dom 8923 df-sdom 8924 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-ico 13319 df-o1 15463

This theorem is referenced by: o1add 15587 o1mul 15588 o1sub 15589

W3C validator