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) )