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