Metamath Proof Explorer

Theorem xltmul1

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

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

Proof

Step Hyp Ref Expression
1 xlemul1 ⊢B∈ℝ*∧A∈ℝ*∧C∈ℝ+→B≤A↔B⋅𝑒C≤A⋅𝑒C
2 1 3com12 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B≤A↔B⋅𝑒C≤A⋅𝑒C
3 2 notbid ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→¬B≤A↔¬B⋅𝑒C≤A⋅𝑒C
4 xrltnle ⊢A∈ℝ*∧B∈ℝ*→A<B↔¬B≤A
5 4 3adant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A<B↔¬B≤A
6 simp1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A∈ℝ*
7 rpxr ⊢C∈ℝ+→C∈ℝ*
8 7 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C∈ℝ*
9 xmulcl ⊢A∈ℝ*∧C∈ℝ*→A⋅𝑒C∈ℝ*
10 6 8 9 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C∈ℝ*
11 simp2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B∈ℝ*
12 xmulcl ⊢B∈ℝ*∧C∈ℝ*→B⋅𝑒C∈ℝ*
13 11 8 12 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B⋅𝑒C∈ℝ*
14 xrltnle ⊢A⋅𝑒C∈ℝ*∧B⋅𝑒C∈ℝ*→A⋅𝑒C<B⋅𝑒C↔¬B⋅𝑒C≤A⋅𝑒C
15 10 13 14 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C<B⋅𝑒C↔¬B⋅𝑒C≤A⋅𝑒C
16 3 5 15 3bitr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A<B↔A⋅𝑒C<B⋅𝑒C