Metamath Proof Explorer

Theorem xlemul2

Description: Extended real version of lemul2 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xlemul2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ≤ B ↔ C ⋅ 𝑒 A ≤ C ⋅ 𝑒 B

Proof

Step Hyp Ref Expression
1 xlemul1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ≤ B ↔ A ⋅ 𝑒 C ≤ B ⋅ 𝑒 C
2 simp1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ∈ ℝ *
3 rpxr ⊢ C ∈ ℝ + → C ∈ ℝ *
4 3 3ad2ant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → C ∈ ℝ *
5 xmulcom ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
6 2 4 5 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C = C ⋅ 𝑒 A
7 simp2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → B ∈ ℝ *
8 xmulcom ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
9 7 4 8 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → B ⋅ 𝑒 C = C ⋅ 𝑒 B
10 6 9 breq12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C ≤ B ⋅ 𝑒 C ↔ C ⋅ 𝑒 A ≤ C ⋅ 𝑒 B
11 1 10 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ≤ B ↔ C ⋅ 𝑒 A ≤ C ⋅ 𝑒 B