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

Metamath Proof Explorer

Theorem lemulge11

Description: Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005)

Ref Expression
Assertion lemulge11 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 𝐴 ≤ ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
2 1 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → ( 𝐴 · 1 ) = 𝐴 )
3 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )
4 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 0 ≤ 𝐴 )
5 3 4 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
6 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
7 1re ⊢ 1 ∈ ℝ
8 0le1 ⊢ 0 ≤ 1
9 7 8 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 )
10 6 9 jctil ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝐵 ∈ ℝ ) )
11 5 3 10 jca31 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝐵 ∈ ℝ ) ) )
12 leid ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ 𝐴 )
13 12 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 𝐴 ≤ 𝐴 )
14 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 1 ≤ 𝐵 )
15 13 14 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → ( 𝐴 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) )
16 lemul12a ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐴 ∈ ℝ ) ∧ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝐵 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) → ( 𝐴 · 1 ) ≤ ( 𝐴 · 𝐵 ) ) )
17 11 15 16 sylc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → ( 𝐴 · 1 ) ≤ ( 𝐴 · 𝐵 ) )
18 2 17 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 𝐴 ≤ ( 𝐴 · 𝐵 ) )