Theorem qnumgt0

Description: A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014)

	Ref	Expression
Assertion	qnumgt0	$$⊢A\in \mathbb{Q}\to \left(0<A\leftrightarrow 0<\mathrm{numer}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		0red	$$⊢A\in \mathbb{Q}\to 0\in ℝ$$
2		qre	$$⊢A\in \mathbb{Q}\to A\in ℝ$$
3		qdencl	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in \mathbb{N}$$
4	3	nnred	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in ℝ$$
5	3	nngt0d	$$⊢A\in \mathbb{Q}\to 0<\mathrm{denom}\left(A\right)$$
6		ltmul1	$$⊢\left(0\in ℝ\wedge A\in ℝ\wedge \left(\mathrm{denom}\left(A\right)\in ℝ\wedge 0<\mathrm{denom}\left(A\right)\right)\right)\to \left(0<A\leftrightarrow 0\cdot \mathrm{denom}\left(A\right)<A\mathrm{denom}\left(A\right)\right)$$
7	1 2 4 5 6	syl112anc	$$⊢A\in \mathbb{Q}\to \left(0<A\leftrightarrow 0\cdot \mathrm{denom}\left(A\right)<A\mathrm{denom}\left(A\right)\right)$$
8	3	nncnd	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in ℂ$$
9	8	mul02d	$$⊢A\in \mathbb{Q}\to 0\cdot \mathrm{denom}\left(A\right)=0$$
10		qmuldeneqnum	$$⊢A\in \mathbb{Q}\to A\mathrm{denom}\left(A\right)=\mathrm{numer}\left(A\right)$$
11	9 10	breq12d	$$⊢A\in \mathbb{Q}\to \left(0\cdot \mathrm{denom}\left(A\right)<A\mathrm{denom}\left(A\right)\leftrightarrow 0<\mathrm{numer}\left(A\right)\right)$$
12	7 11	bitrd	$$⊢A\in \mathbb{Q}\to \left(0<A\leftrightarrow 0<\mathrm{numer}\left(A\right)\right)$$