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		oveq1	$⊢ x = z \to \frac{x}{y} = \frac{z}{y}$
16	15	eqeq2d	$⊢ x = z \to (A = \frac{x}{y} \leftrightarrow A = \frac{z}{y})$
17		elnnz	$⊢ z \in ℕ \leftrightarrow (z \in ℤ \land 0 < z)$
18	17	simplbi2	$⊢ z \in ℤ \to (0 < z \to z \in ℕ)$
19	18	adantl	$⊢ (y \in ℕ \land z \in ℤ) \to (0 < z \to z \in ℕ)$
20	19	adantl	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < z \to z \in ℕ)$
21	20	imp	$⊢ ((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \to z \in ℕ$
22		simpll	$⊢ ((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \to A = \frac{z}{y}$
23	16 21 22	rspcedvdw	$⊢ ((A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \land 0 < z) \to \exists x \in ℕ A = \frac{x}{y}$
24	23	ex	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < z \to \exists x \in ℕ A = \frac{x}{y})$
25	14 24	sylbid	$⊢ (A = \frac{z}{y} \land (y \in ℕ \land z \in ℤ)) \to (0 < A \to \exists x \in ℕ A = \frac{x}{y})$
26	25	ex	$⊢ A = \frac{z}{y} \to ((y \in ℕ \land z \in ℤ) \to (0 < A \to \exists x \in ℕ A = \frac{x}{y}))$
27	26	com13	$⊢ 0 < A \to ((y \in ℕ \land z \in ℤ) \to (A = \frac{z}{y} \to \exists x \in ℕ A = \frac{x}{y}))$
28	27	impl	$⊢ ((0 < A \land y \in ℕ) \land z \in ℤ) \to (A = \frac{z}{y} \to \exists x \in ℕ A = \frac{x}{y})$
29	28	rexlimdva	$⊢ (0 < A \land y \in ℕ) \to (\exists z \in ℤ A = \frac{z}{y} \to \exists x \in ℕ A = \frac{x}{y})$
30	29	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})$
31	3 30	biimtrid	$⊢ 0 < A \to (A \in ℚ \to \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y})$
32	31	impcom	$⊢ (A \in ℚ \land 0 < A) \to \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y}$
33		rexcom	$⊢ \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y} \leftrightarrow \exists y \in ℕ \exists x \in ℕ A = \frac{x}{y}$
34	32 33	sylibr	$⊢ (A \in ℚ \land 0 < A) \to \exists x \in ℕ \exists y \in ℕ A = \frac{x}{y}$

Metamath Proof Explorer

Theorem elpq

Proof