This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lerecd

Description: The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpred.1	$⊢ φ \to A \in ℝ^{+}$
	rpaddcld.1	$⊢ φ \to B \in ℝ^{+}$
Assertion	lerecd	$⊢ φ \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$

Step	Hyp	Ref	Expression
1		rpred.1	$⊢ φ \to A \in ℝ^{+}$
2		rpaddcld.1	$⊢ φ \to B \in ℝ^{+}$
3	1	rpregt0d	$⊢ φ \to (A \in ℝ \land 0 < A)$
4	2	rpregt0d	$⊢ φ \to (B \in ℝ \land 0 < B)$
5		lerec	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$
6	3 4 5	syl2anc	$⊢ φ \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$