Theorem qnumdencoprm

Description: The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014)

	Ref	Expression
Assertion	qnumdencoprm	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)=\mathrm{numer}\left(A\right)$$
2		eqid	$$⊢\mathrm{denom}\left(A\right)=\mathrm{denom}\left(A\right)$$
3	1 2	jctir	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A\right)=\mathrm{numer}\left(A\right)\wedge \mathrm{denom}\left(A\right)=\mathrm{denom}\left(A\right)\right)$$
4		qnumcl	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)\in \mathbb{Z}$$
5		qdencl	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in \mathbb{N}$$
6		qnumdenbi	$$⊢\left(A\in \mathbb{Q}\wedge \mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{N}\right)\to \left(\left(\mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)=1\wedge A=\frac{\mathrm{numer}\left(A\right)}{\mathrm{denom}\left(A\right)}\right)\leftrightarrow \left(\mathrm{numer}\left(A\right)=\mathrm{numer}\left(A\right)\wedge \mathrm{denom}\left(A\right)=\mathrm{denom}\left(A\right)\right)\right)$$
7	4 5 6	mpd3an23	$$⊢A\in \mathbb{Q}\to \left(\left(\mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)=1\wedge A=\frac{\mathrm{numer}\left(A\right)}{\mathrm{denom}\left(A\right)}\right)\leftrightarrow \left(\mathrm{numer}\left(A\right)=\mathrm{numer}\left(A\right)\wedge \mathrm{denom}\left(A\right)=\mathrm{denom}\left(A\right)\right)\right)$$
8	3 7	mpbird	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)=1\wedge A=\frac{\mathrm{numer}\left(A\right)}{\mathrm{denom}\left(A\right)}\right)$$
9	8	simpld	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)=1$$