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