Metamath Proof Explorer

Theorem lemul1

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

Ref Expression
Assertion lemul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ A ⁢ C ≤ B ⁢ C

Proof

Step Hyp Ref Expression
1 ltmul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ C < B ⁢ C
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 recn ⊢ C ∈ ℝ → C ∈ ℂ
5 4 adantr ⊢ C ∈ ℝ ∧ 0 < C → C ∈ ℂ
6 gt0ne0 ⊢ C ∈ ℝ ∧ 0 < C → C ≠ 0
7 5 6 jca ⊢ C ∈ ℝ ∧ 0 < C → C ∈ ℂ ∧ C ≠ 0
8 mulcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ C = B ⁢ C ↔ A = B
9 2 3 7 8 syl3an ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C = B ⁢ C ↔ A = B
10 9 bicomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A = B ↔ A ⁢ C = B ⁢ C
11 1 10 orbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ∨ A = B ↔ A ⁢ C < B ⁢ C ∨ A ⁢ C = B ⁢ C
12 leloe ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A < B ∨ A = B
13 12 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ A < B ∨ A = B
14 remulcl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A ⁢ C ∈ ℝ
15 14 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C ∈ ℝ
16 remulcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C ∈ ℝ
17 16 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C ∈ ℝ
18 15 17 leloed ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C ≤ B ⁢ C ↔ A ⁢ C < B ⁢ C ∨ A ⁢ C = B ⁢ C
19 18 3adant3r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C ≤ B ⁢ C ↔ A ⁢ C < B ⁢ C ∨ A ⁢ C = B ⁢ C
20 11 13 19 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ A ⁢ C ≤ B ⁢ C