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 15555

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 15471	. . . 4 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
2		o1bdd 15473	. . . 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 15471	. . . 4 ⊢ (𝐺 ∈ 𝑂(1) → 𝐺:dom 𝐺⟶ℂ)
6		o1bdd 15473	. . . 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 3207	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
10		reeanv 3207	. . . . 5 ⊢ (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
11		inss1 4196	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
12		ssralv 4012	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)))
13	11, 12	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
14		inss2 4197	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
15		ssralv 4012	. . . . . . . . . 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 3091	. . . . . . . 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 15472	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
26	25	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ⊆ ℝ)
27	11, 26	sstrid 3955	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
28	27	sselda 3943	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑧 ∈ ℝ)
29		maxle 13127	. . . . . . . . . . . . 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 3939	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹)
34		ffvelcdm 7035	. . . . . . . . . . . . . 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 3939	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺)
38		ffvelcdm 7035	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ)
39	36, 37, 38	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑧) ∈ ℂ)
40		o1of2.3	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
41	40	ralrimivva 3178	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
42	41	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
43		fveq2 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧)))
44	43	breq1d 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚))
45	44	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛)))
46		fvoveq1 7392	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦)))
47	46	breq1d 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))
48	45, 47	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)))
49		fveq2 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧)))
50	49	breq1d 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛))
51	50	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
52		oveq2 7377	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
53	52	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
54	53	breq1d 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
55	51, 54	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)))
56	48, 55	rspc2va 3597	. . . . . . . . . . . . 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 6671	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹 Fn dom 𝐹)
59	36	ffnd 6671	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺 Fn dom 𝐺)
60		reex 11135	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
61		ssexg 5273	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
62	26, 60, 61	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ∈ V)
63		dmexg 7857	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ 𝑂(1) → dom 𝐺 ∈ V)
64	63	ad3antlr 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐺 ∈ V)
65		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
66		eqidd 2730	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧))
67		eqidd 2730	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧))
68	58, 59, 62, 64, 65, 66, 67	ofval 7644	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹 ∘_f 𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
69	68	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
70	69	breq1d 5112	. . . . . . . . . . . 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 3145	. . . . . . . 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 7651	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ)
78	23, 21	ifcld 4531	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ)
79		o1of2.1	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)
80	79	adantl 481	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑀 ∈ ℝ)
81		elo12r 15470	. . . . . . . . . 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 3192	. . . . 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 3192	. . 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 3044 ∃wrex 3053 Vcvv 3444 ∩ cin 3910 ⊆ wss 3911 ifcif 4484 class class class wbr 5102 dom cdm 5631 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 ∘_f cof 7631 ℂcc 11042 ℝcr 11043 ≤ cle 11185 abscabs 15176 𝑂(1)co1 15428

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 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-pre-lttri 11118 ax-pre-lttrn 11119

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-er 8648 df-pm 8779 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-ico 13288 df-o1 15432

This theorem is referenced by: o1add 15556 o1mul 15557 o1sub 15558

W3C validator