Theorem lemul2a

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007)

	Ref	Expression
Assertion	lemul2a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 · 𝐴 ) ≤ ( 𝐶 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		lemul1a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) )
2		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
4		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
5	2 3 4	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
6	5	adantrr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
7	6	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
8	7	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
9		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
10		mulcom	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
11	9 3 10	syl2an	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
12	11	adantrr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
13	12	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
14	13	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
15	1 8 14	3brtr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 · 𝐴 ) ≤ ( 𝐶 · 𝐵 ) )