Metamath Proof Explorer

Theorem qnumdencl

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

		Ref	Expression
	Assertion	qnumdencl	$⊢ A \in ℚ \to (numer (A) \in ℤ \land denom (A) \in ℕ)$

Proof

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