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 15690

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 15606	. . . 4 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
2		o1bdd 15608	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
3	1, 2	mpdan 700	. . 3 ⊢ (𝐹 ∈ 𝑂(1) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
4	3	adantr 486	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
5		o1f 15606	. . . 4 ⊢ (𝐺 ∈ 𝑂(1) → 𝐺:dom 𝐺⟶ℂ)
6		o1bdd 15608	. . . 4 ⊢ ((𝐺 ∈ 𝑂(1) ∧ 𝐺:dom 𝐺⟶ℂ) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))
7	5, 6	mpdan 700	. . 3 ⊢ (𝐺 ∈ 𝑂(1) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))
8	7	adantl 487	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))
9		reeanv 3239	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
10		reeanv 3239	. . . . 5 ⊢ (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
11		inss1 4189	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
12		ssralv 4007	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)))
13	11, 12	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
14		inss2 4190	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
15		ssralv 4007	. . . . . . . . . 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 625	. . . . . . . 8 ⊢ ((∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
18		r19.26 3127	. . . . . . . 8 ⊢ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
19	17, 18	sylibr 237	. . . . . . 7 ⊢ ((∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
20		anim12 821	. . . . . . . . . 10 ⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
21		simplrl 789	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑎 ∈ ℝ)
22	21	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑎 ∈ ℝ)
23		simplrr 790	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑏 ∈ ℝ)
24	23	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑏 ∈ ℝ)
25		o1dm 15607	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
26	25	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ⊆ ℝ)
27	11, 26	sstrid 3949	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
28	27	sselda 3938	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑧 ∈ ℝ)
29		maxle 13235	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧)))
30	22, 24, 28, 29	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧)))
31	30	biimpd 232	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧)))
32	1	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹:dom 𝐹⟶ℂ)
33	11	sseli 3934	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹)
34		ffvelcdm 7080	. . . . . . . . . . . . . 14 ⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
35	32, 33, 34	syl2an 608	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑧) ∈ ℂ)
36	5	ad3antlr 744	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺:dom 𝐺⟶ℂ)
37	14	sseli 3934	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺)
38		ffvelcdm 7080	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ)
39	36, 37, 38	syl2an 608	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑧) ∈ ℂ)
40		o1of2.3	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
41	40	ralrimivva 3210	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
42	41	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
43		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧)))
44	43	breq1d 5121	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚))
45	44	anbi1d 643	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛)))
46		fvoveq1 7442	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦)))
47	46	breq1d 5121	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))
48	45, 47	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)))
49		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧)))
50	49	breq1d 5121	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛))
51	50	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
52		oveq2 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
53	52	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
54	53	breq1d 5121	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
55	51, 54	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)))
56	48, 55	rspc2va 3595	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
57	35, 39, 42, 56	syl21anc 851	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
58	32	ffnd 6710	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹 Fn dom 𝐹)
59	36	ffnd 6710	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺 Fn dom 𝐺)
60		reex 11208	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
61		ssexg 5292	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
62	26, 60, 61	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ∈ V)
63		dmexg 7904	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ 𝑂(1) → dom 𝐺 ∈ V)
64	63	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐺 ∈ V)
65		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
66		eqidd 2766	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧))
67		eqidd 2766	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧))
68	58, 59, 62, 64, 65, 66, 67	ofval 7695	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹 ∘_f 𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
69	68	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
70	69	breq1d 5121	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
71	57, 70	sylibrd 262	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀))
72	31, 71	imim12d 82	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
73	20, 72	syl5 35	. . . . . . . . 9 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
74	73	ralimdva 3179	. . . . . . . 8 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
75		o1of2.2	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ)
76	75	adantl 487	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥𝑅𝑦) ∈ ℂ)
77	76, 32, 36, 62, 64, 65	off 7702	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ)
78	23, 21	ifcld 4536	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ)
79		o1of2.1	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)
80	79	adantl 487	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑀 ∈ ℝ)
81		elo12r 15605	. . . . . . . . . 10 ⊢ ((((𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1))
82	81	3expia 1139	. . . . . . . . 9 ⊢ ((((𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
83	77, 27, 78, 80, 82	syl22anc 852	. . . . . . . 8 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
84	74, 83	syld 48	. . . . . . 7 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
85	19, 84	syl5 35	. . . . . 6 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → ((∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
86	85	rexlimdvva 3224	. . . . 5 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
87	10, 86	biimtrrid 246	. . . 4 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → ((∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
88	87	rexlimdvva 3224	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
89	9, 88	biimtrrid 246	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ((∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
90	4, 8, 89	mp2and 712	1 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ∩ cin 3905 ⊆ wss 3906 ifcif 4489 class class class wbr 5111 dom cdm 5663 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ∘_f cof 7682 ℂcc 11115 ℝcr 11116 ≤ cle 11261 abscabs 15311 𝑂(1)co1 15563

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-pre-lttri 11191 ax-pre-lttrn 11192

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-po 5571 df-so 5572 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-er 8700 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-ico 13396 df-o1 15567

This theorem is used by: o1add 15691 o1mul 15692 o1sub 15693

W3C validator