Metamath Proof Explorer

Theorem lemuldiv2

Description: 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006)

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

Proof

Step Hyp Ref Expression
1 recn ⊢A∈ℝ→A∈ℂ
2 recn ⊢C∈ℝ→C∈ℂ
3 mulcom ⊢A∈ℂ∧C∈ℂ→A⁢C=C⁢A
4 1 2 3 syl2an ⊢A∈ℝ∧C∈ℝ→A⁢C=C⁢A
5 4 adantrr ⊢A∈ℝ∧C∈ℝ∧0<C→A⁢C=C⁢A
6 5 3adant2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A⁢C=C⁢A
7 6 breq1d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A⁢C≤B↔C⁢A≤B
8 lemuldiv ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A⁢C≤B↔A≤BC
9 7 8 bitr3d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→C⁢A≤B↔A≤BC