Theorem lemul1a

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005)

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

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		leloe	⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 ≤ 𝐶 ↔ ( 0 < 𝐶 ∨ 0 = 𝐶 ) ) )
3	1 2	mpan	⊢ ( 𝐶 ∈ ℝ → ( 0 ≤ 𝐶 ↔ ( 0 < 𝐶 ∨ 0 = 𝐶 ) ) )
4	3	pm5.32i	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ↔ ( 𝐶 ∈ ℝ ∧ ( 0 < 𝐶 ∨ 0 = 𝐶 ) ) )
5		lemul1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
6	5	biimpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
7	6	3expia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
8	7	com12	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
9	1	leidi	⊢ 0 ≤ 0
10		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
11	10	mul01d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
12		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
13	12	mul01d	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 0 ) = 0 )
14	11 13	breqan12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 0 ) ≤ ( 𝐵 · 0 ) ↔ 0 ≤ 0 ) )
15	9 14	mpbiri	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 0 ) ≤ ( 𝐵 · 0 ) )
16		oveq2	⊢ ( 0 = 𝐶 → ( 𝐴 · 0 ) = ( 𝐴 · 𝐶 ) )
17		oveq2	⊢ ( 0 = 𝐶 → ( 𝐵 · 0 ) = ( 𝐵 · 𝐶 ) )
18	16 17	breq12d	⊢ ( 0 = 𝐶 → ( ( 𝐴 · 0 ) ≤ ( 𝐵 · 0 ) ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
19	15 18	imbitrid	⊢ ( 0 = 𝐶 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
20	19	a1dd	⊢ ( 0 = 𝐶 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
21	20	adantl	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 = 𝐶 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
22	8 21	jaodan	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 0 < 𝐶 ∨ 0 = 𝐶 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
23	4 22	sylbi	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
24	23	com12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) )
25	24	3impia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
26	25	imp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) )