Theorem qnumdencl

Description: Lemma for qnumcl and qdencl . (Contributed by Stefan O'Rear, 13-Sep-2014)

	Ref	Expression
Assertion	qnumdencl	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		qredeu	$$⊢A\in \mathbb{Q}\to \exists !a\in \left(\mathbb{Z}\times \mathbb{N}\right)\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)$$
2		riotacl	$$⊢\exists !a\in \left(\mathbb{Z}\times \mathbb{N}\right)\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\to \left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\in \left(\mathbb{Z}\times \mathbb{N}\right)$$
3	1 2	syl	$$⊢A\in \mathbb{Q}\to \left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\in \left(\mathbb{Z}\times \mathbb{N}\right)$$
4		elxp6	$$⊢\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\in \left(\mathbb{Z}\times \mathbb{N}\right)\leftrightarrow \left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)=⟨1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right),2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)⟩\wedge \left(1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{Z}\wedge 2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{N}\right)\right)$$
5		qnumval	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)=1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)$$
6	5	eleq1d	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\leftrightarrow 1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{Z}\right)$$
7		qdenval	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)=2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)$$
8	7	eleq1d	$$⊢A\in \mathbb{Q}\to \left(\mathrm{denom}\left(A\right)\in \mathbb{N}\leftrightarrow 2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{N}\right)$$
9	6 8	anbi12d	$$⊢A\in \mathbb{Q}\to \left(\left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)\leftrightarrow \left(1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{Z}\wedge 2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{N}\right)\right)$$
10	9	biimprd	$$⊢A\in \mathbb{Q}\to \left(\left(1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{Z}\wedge 2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{N}\right)\to \left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)\right)$$
11	10	adantld	$$⊢A\in \mathbb{Q}\to \left(\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)=⟨1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right),2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)⟩\wedge \left(1^{st}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{Z}\wedge 2^{nd}\left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\right)\in \mathbb{N}\right)\right)\to \left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)\right)$$
12	4 11	biimtrid	$$⊢A\in \mathbb{Q}\to \left(\left(\iota a\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(a\right)\gcd 2^{nd}\left(a\right)=1\wedge A=\frac{1^{st}\left(a\right)}{2^{nd}\left(a\right)}\right)\right)\in \left(\mathbb{Z}\times \mathbb{N}\right)\to \left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)\right)$$
13	3 12	mpd	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)$$