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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → A ⁢ C ≤ B ⁢ C

Proof

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