This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem o1mul

Description: The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion o1mul ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 remulcl ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 𝑚 · 𝑛 ) ∈ ℝ )
2 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
3 simp2l ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → 𝑥 ∈ ℂ )
4 simp2r ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → 𝑦 ∈ ℂ )
5 3 4 absmuld ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) )
6 3 abscld ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
7 simp1l ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → 𝑚 ∈ ℝ )
8 4 abscld ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( abs ‘ 𝑦 ) ∈ ℝ )
9 simp1r ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → 𝑛 ∈ ℝ )
10 3 absge0d ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → 0 ≤ ( abs ‘ 𝑥 ) )
11 4 absge0d ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → 0 ≤ ( abs ‘ 𝑦 ) )
12 simp3l ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( abs ‘ 𝑥 ) ≤ 𝑚 )
13 simp3r ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( abs ‘ 𝑦 ) ≤ 𝑛 )
14 6 7 8 9 10 11 12 13 lemul12ad ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) ≤ ( 𝑚 · 𝑛 ) )
15 5 14 eqbrtrd ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) ≤ ( 𝑚 · 𝑛 ) )
16 15 3expia ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) ≤ ( 𝑚 · 𝑛 ) ) )
17 1 2 16 o1of2 ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝑂(1) )