lemulge12

Description: Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	lemulge12	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 1 \leq B)) \to A \leq B A$

Step	Hyp	Ref	Expression
1		lemulge11	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 1 \leq B)) \to A \leq A B$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		recn	$⊢ B \in ℝ \to B \in ℂ$
4		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
5	2 3 4	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A B = B A$
6	5	breq2d	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq A B \leftrightarrow A \leq B A)$
7	6	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 1 \leq B)) \to (A \leq A B \leftrightarrow A \leq B A)$
8	1 7	mpbid	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 1 \leq B)) \to A \leq B A$

Metamath Proof Explorer