elpqb

Description: A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022)

		Ref	Expression
	Assertion	elpqb	$⊢ (A \in ℚ \land 0 < A) \leftrightarrow \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y}$

Step	Hyp	Ref	Expression
1		elpq	$⊢ (A \in ℚ \land 0 < A) \to \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y}$
2		nnz	$⊢ x \in ℕ \to x \in ℤ$
3		znq	$⊢ (x \in ℤ \land y \in ℕ) \to \frac{x}{y} \in ℚ$
4	2 3	sylan	$⊢ (x \in ℕ \land y \in ℕ) \to \frac{x}{y} \in ℚ$
5		nnre	$⊢ x \in ℕ \to x \in ℝ$
6		nngt0	$⊢ x \in ℕ \to 0 < x$
7	5 6	jca	$⊢ x \in ℕ \to (x \in ℝ \land 0 < x)$
8		nnre	$⊢ y \in ℕ \to y \in ℝ$
9		nngt0	$⊢ y \in ℕ \to 0 < y$
10	8 9	jca	$⊢ y \in ℕ \to (y \in ℝ \land 0 < y)$
11		divgt0	$⊢ ((x \in ℝ \land 0 < x) \land (y \in ℝ \land 0 < y)) \to 0 < \frac{x}{y}$
12	7 10 11	syl2an	$⊢ (x \in ℕ \land y \in ℕ) \to 0 < \frac{x}{y}$
13	4 12	jca	$⊢ (x \in ℕ \land y \in ℕ) \to (\frac{x}{y} \in ℚ \land 0 < \frac{x}{y})$
14		eleq1	$⊢ A = \frac{x}{y} \to (A \in ℚ \leftrightarrow \frac{x}{y} \in ℚ)$
15		breq2	$⊢ A = \frac{x}{y} \to (0 < A \leftrightarrow 0 < \frac{x}{y})$
16	14 15	anbi12d	$⊢ A = \frac{x}{y} \to ((A \in ℚ \land 0 < A) \leftrightarrow (\frac{x}{y} \in ℚ \land 0 < \frac{x}{y}))$
17	13 16	syl5ibrcom	$⊢ (x \in ℕ \land y \in ℕ) \to (A = \frac{x}{y} \to (A \in ℚ \land 0 < A))$
18	17	rexlimivv	$⊢ \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y} \to (A \in ℚ \land 0 < A)$
19	1 18	impbii	$⊢ (A \in ℚ \land 0 < A) \leftrightarrow \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y}$

Metamath Proof Explorer