xlemul2a

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

		Ref	Expression
	Assertion	xlemul2a	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to C \cdot_{𝑒} A \leq C \cdot_{𝑒} B$

Step	Hyp	Ref	Expression
1		xlemul1a	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
2		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{} \land 0 \leq C)) \land A \leq B) \to A \in ℝ^{}$
3		simpl3l	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{} \land 0 \leq C)) \land A \leq B) \to C \in ℝ^{}$
4		xmulcom	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to A \cdot_{𝑒} C = C \cdot_{𝑒} A$
5	2 3 4	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to A \cdot_{𝑒} C = C \cdot_{𝑒} A$
6		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{} \land 0 \leq C)) \land A \leq B) \to B \in ℝ^{}$
7		xmulcom	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to B \cdot_{𝑒} C = C \cdot_{𝑒} B$
8	6 3 7	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to B \cdot_{𝑒} C = C \cdot_{𝑒} B$
9	1 5 8	3brtr3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to C \cdot_{𝑒} A \leq C \cdot_{𝑒} B$

Metamath Proof Explorer