qnumdenbi

Description: Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	qnumdenbi	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ((B \gcd C = 1 \land A = \frac{B}{C}) \leftrightarrow (numer (A) = B \land denom (A) = C))$

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		1st2nd2	$⊢ (ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) \in (ℤ \times ℕ) \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)})))⟩$
4	1 2 3	3syl	$⊢ 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)})))⟩$
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		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)})))$
7	5 6	opeq12d	$⊢ A \in ℚ \to ⟨numer (A), denom (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)})))⟩$
8	4 7	eqtr4d	$⊢ A \in ℚ \to (ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) = ⟨numer (A), denom (A)⟩$
9	8	eqeq1d	$⊢ A \in ℚ \to ((ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) = ⟨B, C⟩ \leftrightarrow ⟨numer (A), denom (A)⟩ = ⟨B, C⟩)$
10	9	3ad2ant1	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ((ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) = ⟨B, C⟩ \leftrightarrow ⟨numer (A), denom (A)⟩ = ⟨B, C⟩)$
11		fvex	$⊢ numer (A) \in V$
12		fvex	$⊢ denom (A) \in V$
13	11 12	opth	$⊢ ⟨numer (A), denom (A)⟩ = ⟨B, C⟩ \leftrightarrow (numer (A) = B \land denom (A) = C)$
14	10 13	bitr2di	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ((numer (A) = B \land denom (A) = C) \leftrightarrow (ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) = ⟨B, C⟩)$
15		opelxpi	$⊢ (B \in ℤ \land C \in ℕ) \to ⟨B, C⟩ \in (ℤ \times ℕ)$
16	15	3adant1	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ⟨B, C⟩ \in (ℤ \times ℕ)$
17	1	3ad2ant1	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to \exists! a \in (ℤ \times ℕ) (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})$
18		fveq2	$⊢ a = ⟨B, C⟩ \to 1^{st} (a) = 1^{st} (⟨B, C⟩)$
19		fveq2	$⊢ a = ⟨B, C⟩ \to 2^{nd} (a) = 2^{nd} (⟨B, C⟩)$
20	18 19	oveq12d	$⊢ a = ⟨B, C⟩ \to 1^{st} (a) \gcd 2^{nd} (a) = 1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩)$
21	20	eqeq1d	$⊢ a = ⟨B, C⟩ \to (1^{st} (a) \gcd 2^{nd} (a) = 1 \leftrightarrow 1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = 1)$
22	18 19	oveq12d	$⊢ a = ⟨B, C⟩ \to \frac{1^{st} (a)}{2^{nd} (a)} = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)}$
23	22	eqeq2d	$⊢ a = ⟨B, C⟩ \to (A = \frac{1^{st} (a)}{2^{nd} (a)} \leftrightarrow A = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)})$
24	21 23	anbi12d	$⊢ a = ⟨B, C⟩ \to ((1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)}) \leftrightarrow (1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = 1 \land A = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)}))$
25	24	riota2	$⊢ (⟨B, C⟩ \in (ℤ \times ℕ) \land \exists! a \in (ℤ \times ℕ) (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) \to ((1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = 1 \land A = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)}) \leftrightarrow (ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) = ⟨B, C⟩)$
26	16 17 25	syl2anc	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ((1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = 1 \land A = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)}) \leftrightarrow (ι a \in (ℤ \times ℕ) \| (1^{st} (a) \gcd 2^{nd} (a) = 1 \land A = \frac{1^{st} (a)}{2^{nd} (a)})) = ⟨B, C⟩)$
27		op1stg	$⊢ (B \in ℤ \land C \in ℕ) \to 1^{st} (⟨B, C⟩) = B$
28		op2ndg	$⊢ (B \in ℤ \land C \in ℕ) \to 2^{nd} (⟨B, C⟩) = C$
29	27 28	oveq12d	$⊢ (B \in ℤ \land C \in ℕ) \to 1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = B \gcd C$
30	29	3adant1	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to 1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = B \gcd C$
31	30	eqeq1d	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to (1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = 1 \leftrightarrow B \gcd C = 1)$
32	27	3adant1	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to 1^{st} (⟨B, C⟩) = B$
33	28	3adant1	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to 2^{nd} (⟨B, C⟩) = C$
34	32 33	oveq12d	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)} = \frac{B}{C}$
35	34	eqeq2d	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to (A = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)} \leftrightarrow A = \frac{B}{C})$
36	31 35	anbi12d	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ((1^{st} (⟨B, C⟩) \gcd 2^{nd} (⟨B, C⟩) = 1 \land A = \frac{1^{st} (⟨B, C⟩)}{2^{nd} (⟨B, C⟩)}) \leftrightarrow (B \gcd C = 1 \land A = \frac{B}{C}))$
37	14 26 36	3bitr2rd	$⊢ (A \in ℚ \land B \in ℤ \land C \in ℕ) \to ((B \gcd C = 1 \land A = \frac{B}{C}) \leftrightarrow (numer (A) = B \land denom (A) = C))$

Metamath Proof Explorer

Theorem qnumdenbi

Proof