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 15615

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 15531	. . . 4 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
2		o1bdd 15533	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
3	1, 2	mpdan 685	. . 3 ⊢ (𝐹 ∈ 𝑂(1) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
4	3	adantr 479	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
5		o1f 15531	. . . 4 ⊢ (𝐺 ∈ 𝑂(1) → 𝐺:dom 𝐺⟶ℂ)
6		o1bdd 15533	. . . 4 ⊢ ((𝐺 ∈ 𝑂(1) ∧ 𝐺:dom 𝐺⟶ℂ) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))
7	5, 6	mpdan 685	. . 3 ⊢ (𝐺 ∈ 𝑂(1) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))
8	7	adantl 480	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛))
9		reeanv 3217	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
10		reeanv 3217	. . . . 5 ⊢ (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
11		inss1 4230	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
12		ssralv 4048	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚)))
13	11, 12	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚))
14		inss2 4231	. . . . . . . . . 10 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
15		ssralv 4048	. . . . . . . . . 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 611	. . . . . . . 8 ⊢ ((∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
18		r19.26 3101	. . . . . . . 8 ⊢ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) ↔ (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
19	17, 18	sylibr 233	. . . . . . 7 ⊢ ((∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
20		anim12 807	. . . . . . . . . 10 ⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
21		simplrl 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑎 ∈ ℝ)
22	21	adantr 479	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑎 ∈ ℝ)
23		simplrr 776	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑏 ∈ ℝ)
24	23	adantr 479	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑏 ∈ ℝ)
25		o1dm 15532	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
26	25	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ⊆ ℝ)
27	11, 26	sstrid 3991	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
28	27	sselda 3979	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → 𝑧 ∈ ℝ)
29		maxle 13224	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧)))
30	22, 24, 28, 29	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧)))
31	30	biimpd 228	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧)))
32	1	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹:dom 𝐹⟶ℂ)
33	11	sseli 3975	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐹)
34		ffvelcdm 7095	. . . . . . . . . . . . . 14 ⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ)
35	32, 33, 34	syl2an 594	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑧) ∈ ℂ)
36	5	ad3antlr 729	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺:dom 𝐺⟶ℂ)
37	14	sseli 3975	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑧 ∈ dom 𝐺)
38		ffvelcdm 7095	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) ∈ ℂ)
39	36, 37, 38	syl2an 594	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑧) ∈ ℂ)
40		o1of2.3	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
41	40	ralrimivva 3191	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
42	41	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀))
43		fveq2 6901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘𝑥) = (abs‘(𝐹‘𝑧)))
44	43	breq1d 5163	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘𝑥) ≤ 𝑚 ↔ (abs‘(𝐹‘𝑧)) ≤ 𝑚))
45	44	anbi1d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛)))
46		fvoveq1 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐹‘𝑧) → (abs‘(𝑥𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅𝑦)))
47	46	breq1d 5163	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐹‘𝑧) → ((abs‘(𝑥𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀))
48	45, 47	imbi12d 343	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐹‘𝑧) → ((((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀)))
49		fveq2 6901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘𝑦) = (abs‘(𝐺‘𝑧)))
50	49	breq1d 5163	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘𝑦) ≤ 𝑛 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑛))
51	50	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) ↔ ((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛)))
52		oveq2 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑧)𝑅𝑦) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
53	52	fveq2d 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝐺‘𝑧) → (abs‘((𝐹‘𝑧)𝑅𝑦)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
54	53	breq1d 5163	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘𝑧) → ((abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
55	51, 54	imbi12d 343	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘𝑧) → ((((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅𝑦)) ≤ 𝑀) ↔ (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀)))
56	48, 55	rspc2va 3620	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (((abs‘𝑥) ≤ 𝑚 ∧ (abs‘𝑦) ≤ 𝑛) → (abs‘(𝑥𝑅𝑦)) ≤ 𝑀)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
57	35, 39, 42, 56	syl21anc 836	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((abs‘(𝐹‘𝑧)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑧)) ≤ 𝑛) → (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
58	32	ffnd 6729	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐹 Fn dom 𝐹)
59	36	ffnd 6729	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐺 Fn dom 𝐺)
60		reex 11249	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
61		ssexg 5328	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
62	26, 60, 61	sylancl 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐹 ∈ V)
63		dmexg 7914	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ 𝑂(1) → dom 𝐺 ∈ V)
64	63	ad3antlr 729	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → dom 𝐺 ∈ V)
65		eqid 2726	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
66		eqidd 2727	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) = (𝐹‘𝑧))
67		eqidd 2727	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ dom 𝐺) → (𝐺‘𝑧) = (𝐺‘𝑧))
68	58, 59, 62, 64, 65, 66, 67	ofval 7701	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹 ∘_f 𝑅𝐺)‘𝑧) = ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))
69	68	fveq2d 6905	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) = (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
70	69	breq1d 5163	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑧)𝑅(𝐺‘𝑧))) ≤ 𝑀))
71	57, 70	sylibrd 258	. . . . . . . . . . 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 3157	. . . . . . . 8 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)))
75		o1of2.2	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑅𝑦) ∈ ℂ)
76	75	adantl 480	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥𝑅𝑦) ∈ ℂ)
77	76, 32, 36, 62, 64, 65	off 7708	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ)
78	23, 21	ifcld 4579	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ)
79		o1of2.1	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → 𝑀 ∈ ℝ)
80	79	adantl 480	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑀 ∈ ℝ)
81		elo12r 15530	. . . . . . . . . 10 ⊢ ((((𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ ∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1))
82	81	3expia 1118	. . . . . . . . 9 ⊢ ((((𝐹 ∘_f 𝑅𝐺):(dom 𝐹 ∩ dom 𝐺)⟶ℂ ∧ (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ) ∧ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (∀𝑧 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐹 ∘_f 𝑅𝐺)‘𝑧)) ≤ 𝑀) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
83	77, 27, 78, 80, 82	syl22anc 837	. . . . . . . 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 3202	. . . . 5 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
87	10, 86	biimtrrid 242	. . . 4 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → ((∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
88	87	rexlimdvva 3202	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
89	9, 88	biimtrrid 242	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → ((∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑎 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑚) ∧ ∃𝑏 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ dom 𝐺(𝑏 ≤ 𝑧 → (abs‘(𝐺‘𝑧)) ≤ 𝑛)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1)))
90	4, 8, 89	mp2and 697	1 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1)) → (𝐹 ∘_f 𝑅𝐺) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∀wral 3051 ∃wrex 3060 Vcvv 3462 ∩ cin 3946 ⊆ wss 3947 ifcif 4533 class class class wbr 5153 dom cdm 5682 ⟶wf 6550 ‘cfv 6554 (class class class)co 7424 ∘_f cof 7688 ℂcc 11156 ℝcr 11157 ≤ cle 11299 abscabs 15239 𝑂(1)co1 15488

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11214 ax-resscn 11215 ax-pre-lttri 11232 ax-pre-lttrn 11233

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-po 5594 df-so 5595 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7690 df-er 8734 df-pm 8858 df-en 8975 df-dom 8976 df-sdom 8977 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-ico 13384 df-o1 15492

This theorem is referenced by: o1add 15616 o1mul 15617 o1sub 15618

W3C validator