Metamath Proof Explorer

Theorem lt2msq1

Description: Lemma for lt2msq . (Contributed by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to A \in ℝ$
2	1 1	remulcld	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to A A \in ℝ$
3		simp2	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to B \in ℝ$
4	3 1	remulcld	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to B A \in ℝ$
5	3 3	remulcld	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to B B \in ℝ$
6		simp1	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to (A \in ℝ \land 0 \leq A)$
7		simp3	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to A < B$
8	1 3 7	ltled	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to A \leq B$
9		lemul1a	$⊢ ((A \in ℝ \land B \in ℝ \land (A \in ℝ \land 0 \leq A)) \land A \leq B) \to A A \leq B A$
10	1 3 6 8 9	syl31anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to A A \leq B A$
11		0red	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to 0 \in ℝ$
12		simp1r	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to 0 \leq A$
13	11 1 3 12 7	lelttrd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to 0 < B$
14		ltmul2	$⊢ (A \in ℝ \land B \in ℝ \land (B \in ℝ \land 0 < B)) \to (A < B \leftrightarrow B A < B B)$
15	1 3 3 13 14	syl112anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to (A < B \leftrightarrow B A < B B)$
16	7 15	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to B A < B B$
17	2 4 5 10 16	lelttrd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ \land A < B) \to A A < B B$