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