Metamath Proof Explorer

Theorem xlemul2a

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

Ref Expression
Assertion xlemul2a ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → C ⋅ 𝑒 A ≤ C ⋅ 𝑒 B

Proof

Step Hyp Ref Expression
1 xlemul1a ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → A ⋅ 𝑒 C ≤ B ⋅ 𝑒 C
2 simpl1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → A ∈ ℝ *
3 simpl3l ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → C ∈ ℝ *
4 xmulcom ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
5 2 3 4 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → A ⋅ 𝑒 C = C ⋅ 𝑒 A
6 simpl2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → B ∈ ℝ *
7 xmulcom ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
8 6 3 7 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → B ⋅ 𝑒 C = C ⋅ 𝑒 B
9 1 5 8 3brtr3d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 0 ≤ C ∧ A ≤ B → C ⋅ 𝑒 A ≤ C ⋅ 𝑒 B