Metamath Proof Explorer

Theorem xltmul2

Description: Extended real version of ltmul2 . (Contributed by Mario Carneiro, 8-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 xltmul1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A < B ↔ A ⋅ 𝑒 C < B ⋅ 𝑒 C
2 rpxr ⊢ C ∈ ℝ + → C ∈ ℝ *
3 xmulcom ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
4 3 3adant2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
5 xmulcom ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
6 5 3adant1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
7 4 6 breq12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C < B ⋅ 𝑒 C ↔ C ⋅ 𝑒 A < C ⋅ 𝑒 B
8 2 7 syl3an3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C < B ⋅ 𝑒 C ↔ C ⋅ 𝑒 A < C ⋅ 𝑒 B
9 1 8 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A < B ↔ C ⋅ 𝑒 A < C ⋅ 𝑒 B