elpq

Description: A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022)

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

Proof

Step	Hyp	Ref	Expression
1		elq	$⊢ A \in ℚ \leftrightarrow \exists z \in ℤ \exists y \in ℕ A = \frac{z}{y}$
2		rexcom	$⊢ \exists z \in ℤ \exists y \in ℕ A = \frac{z}{y} \leftrightarrow \exists y \in ℕ \exists z \in ℤ A = \frac{z}{y}$
3	1 2	bitri	$⊢ A \in ℚ \leftrightarrow \exists y \in ℕ \exists z \in ℤ A = \frac{z}{y}$
4		breq2	$⊢ A = \frac{z}{y} \to (0 < A \leftrightarrow 0 < \frac{z}{y})$
5		zre	$⊢ z \in ℤ \to z \in ℝ$
6	5	adantl	$⊢ (y \in ℕ \land z \in ℤ) \to z \in ℝ$
7		nnre	$⊢ y \in ℕ \to y \in ℝ$
8	7	adantr	$⊢ (y \in ℕ \land z \in ℤ) \to y \in ℝ$
9		nngt0	$⊢ y \in ℕ \to 0 < y$
10	9	adantr	$⊢ (y \in ℕ \land z \in ℤ) \to 0 < y$
11		gt0div	$⊢ (z \in ℝ \land y \in ℝ \land 0 < y) \to (0 < z \leftrightarrow 0 < \frac{z}{y})$
12	6 8 10 11	syl3anc	$⊢ (y \in ℕ \land z \in ℤ) \to (0 < z \leftrightarrow 0 < \frac{z}{y})$
13	12	bicomd	$⊢ (y \in ℕ \land z \in ℤ) \to (0 < \frac{z}{y} \leftrightarrow 0 < z)$
14	4 13	sylan9bb	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < A \leftrightarrow 0 < z)$
15		elnnz	$⊢ z \in ℕ \leftrightarrow (z \in ℤ \land 0 < z)$
16	15	simplbi2	$⊢ z \in ℤ \to (0 < z \to z \in ℕ)$
17	16	adantl	$⊢ (y \in ℕ \land z \in ℤ) \to (0 < z \to z \in ℕ)$
18	17	adantl	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < z \to z \in ℕ)$
19	18	imp	$⊢ ((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \to z \in ℕ$
20		oveq1	$⊢ x = z \to \frac{x}{y} = \frac{z}{y}$
21	20	eqeq2d	$⊢ x = z \to (A = \frac{x}{y} \leftrightarrow A = \frac{z}{y})$
22	21	adantl	$⊢ (((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \land x = z) \to (A = \frac{x}{y} \leftrightarrow A = \frac{z}{y})$
23		simpll	$⊢ ((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \to A = \frac{z}{y}$
24	19 22 23	rspcedvd	$⊢ ((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \to \exists x \in ℕ A = \frac{x}{y}$
25	24	ex	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < z \to \exists x \in ℕ A = \frac{x}{y})$
26	14 25	sylbid	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < A \to \exists x \in ℕ A = \frac{x}{y})$
27	26	ex	$⊢ A = \frac{z}{y} \to ((y \in ℕ \land z \in ℤ) \to (0 < A \to \exists x \in ℕ A = \frac{x}{y}))$
28	27	com13	$⊢ 0 < A \to ((y \in ℕ \land z \in ℤ) \to (A = \frac{z}{y} \to \exists x \in ℕ A = \frac{x}{y}))$
29	28	impl	$⊢ ((0 < A \land y \in ℕ) \land z \in ℤ) \to (A = \frac{z}{y} \to \exists x \in ℕ A = \frac{x}{y})$
30	29	rexlimdva	$⊢ (0 < A \land y \in ℕ) \to (\exists z \in ℤ A = \frac{z}{y} \to \exists x \in ℕ A = \frac{x}{y})$
31	30	reximdva	$⊢ 0 < A \to (\exists y \in ℕ \exists z \in ℤ A = \frac{z}{y} \to \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y})$
32	3 31	syl5bi	$⊢ 0 < A \to (A \in ℚ \to \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y})$
33	32	impcom	$⊢ (A \in ℚ \land 0 < A) \to \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y}$
34		rexcom	$⊢ \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y} \leftrightarrow \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y}$
35	33 34	sylibr	$⊢ (A \in ℚ \land 0 < A) \to \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y}$

Metamath Proof Explorer

Theorem elpq

Proof