Metamath Proof Explorer

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 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) )