Metamath Proof Explorer

Theorem lemul2

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

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

Proof

Step Hyp Ref Expression
1 lemul1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A≤B↔A⁢C≤B⁢C
2 recn ⊢A∈ℝ→A∈ℂ
3 recn ⊢C∈ℝ→C∈ℂ
4 mulcom ⊢A∈ℂ∧C∈ℂ→A⁢C=C⁢A
5 2 3 4 syl2an ⊢A∈ℝ∧C∈ℝ→A⁢C=C⁢A
6 5 3adant2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A⁢C=C⁢A
7 recn ⊢B∈ℝ→B∈ℂ
8 mulcom ⊢B∈ℂ∧C∈ℂ→B⁢C=C⁢B
9 7 3 8 syl2an ⊢B∈ℝ∧C∈ℝ→B⁢C=C⁢B
10 9 3adant1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B⁢C=C⁢B
11 6 10 breq12d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A⁢C≤B⁢C↔C⁢A≤C⁢B
12 11 3adant3r ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A⁢C≤B⁢C↔C⁢A≤C⁢B
13 1 12 bitrd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A≤B↔C⁢A≤C⁢B