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

Metamath Proof Explorer

Theorem ltdivgt1

Description: Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	ltdivgt1.1	$⊢ φ \to A \in ℝ^{+}$
	ltdivgt1.2	$⊢ φ \to B \in ℝ^{+}$
Assertion	ltdivgt1	$⊢ φ \to (1 < B \leftrightarrow \frac{A}{B} < A)$

Step	Hyp	Ref	Expression
1		ltdivgt1.1	$⊢ φ \to A \in ℝ^{+}$
2		ltdivgt1.2	$⊢ φ \to B \in ℝ^{+}$
3		1rp	$⊢ 1 \in ℝ^{+}$
4	3	a1i	$⊢ φ \to 1 \in ℝ^{+}$
5	4 2 1	ltdiv2d	$⊢ φ \to (1 < B \leftrightarrow \frac{A}{B} < \frac{A}{1})$
6	1	rpcnd	$⊢ φ \to A \in ℂ$
7	6	div1d	$⊢ φ \to \frac{A}{1} = A$
8	7	breq2d	$⊢ φ \to (\frac{A}{B} < \frac{A}{1} \leftrightarrow \frac{A}{B} < A)$
9	5 8	bitrd	$⊢ φ \to (1 < B \leftrightarrow \frac{A}{B} < A)$