Theorem elq

Description: Membership in the set of rationals. (Contributed by NM, 8-Jan-2002) (Revised by Mario Carneiro, 28-Jan-2014)

	Ref	Expression
Assertion	elq	$$⊢A\in \mathbb{Q}\leftrightarrow \exists x\in \mathbb{Z}\exists y\in \mathbb{N}A=\frac{x}{y}$$

Proof

Step	Hyp	Ref	Expression
1		df-q	$$⊢\mathbb{Q}=÷\left[\mathbb{Z}\times \mathbb{N}\right]$$
2	1	eleq2i	$$⊢A\in \mathbb{Q}\leftrightarrow A\in ÷\left[\mathbb{Z}\times \mathbb{N}\right]$$
3		df-div	$$⊢÷=\left(x\in ℂ,y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota z\in ℂ|yz=x\right)\right)$$
4		riotaex	$$⊢\left(\iota z\in ℂ|yz=x\right)\in \mathrm{V}$$
5	3 4	fnmpoi	$$⊢÷Fn\left(ℂ\times \left(ℂ\setminus \left\{0\right\}\right)\right)$$
6		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
7		nncn	$$⊢x\in \mathbb{N}\to x\in ℂ$$
8		nnne0	$$⊢x\in \mathbb{N}\to x\ne 0$$
9		eldifsn	$$⊢x\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(x\in ℂ\wedge x\ne 0\right)$$
10	7 8 9	sylanbrc	$$⊢x\in \mathbb{N}\to x\in \left(ℂ\setminus \left\{0\right\}\right)$$
11	10	ssriv	$$⊢\mathbb{N}\subseteq ℂ\setminus \left\{0\right\}$$
12		xpss12	$$⊢\left(\mathbb{Z}\subseteq ℂ\wedge \mathbb{N}\subseteq ℂ\setminus \left\{0\right\}\right)\to \mathbb{Z}\times \mathbb{N}\subseteq ℂ\times \left(ℂ\setminus \left\{0\right\}\right)$$
13	6 11 12	mp2an	$$⊢\mathbb{Z}\times \mathbb{N}\subseteq ℂ\times \left(ℂ\setminus \left\{0\right\}\right)$$
14		ovelimab	$$⊢\left(÷Fn\left(ℂ\times \left(ℂ\setminus \left\{0\right\}\right)\right)\wedge \mathbb{Z}\times \mathbb{N}\subseteq ℂ\times \left(ℂ\setminus \left\{0\right\}\right)\right)\to \left(A\in ÷\left[\mathbb{Z}\times \mathbb{N}\right]\leftrightarrow \exists x\in \mathbb{Z}\exists y\in \mathbb{N}A=\frac{x}{y}\right)$$
15	5 13 14	mp2an	$$⊢A\in ÷\left[\mathbb{Z}\times \mathbb{N}\right]\leftrightarrow \exists x\in \mathbb{Z}\exists y\in \mathbb{N}A=\frac{x}{y}$$
16	2 15	bitri	$$⊢A\in \mathbb{Q}\leftrightarrow \exists x\in \mathbb{Z}\exists y\in \mathbb{N}A=\frac{x}{y}$$