qredeu

Description: Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013)

		Ref	Expression
	Assertion	qredeu	$⊢ A \in ℚ \to \exists! x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)})$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ n \in ℕ \to n \in ℤ$
2		gcddvds	$⊢ (z \in ℤ \land n \in ℤ) \to ((z \gcd n) ∥ z \land (z \gcd n) ∥ n)$
3	2	simpld	$⊢ (z \in ℤ \land n \in ℤ) \to (z \gcd n) ∥ z$
4	1 3	sylan2	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) ∥ z$
5		gcdcl	$⊢ (z \in ℤ \land n \in ℤ) \to z \gcd n \in ℕ_{0}$
6	1 5	sylan2	$⊢ (z \in ℤ \land n \in ℕ) \to z \gcd n \in ℕ_{0}$
7	6	nn0zd	$⊢ (z \in ℤ \land n \in ℕ) \to z \gcd n \in ℤ$
8		simpl	$⊢ (z \in ℤ \land n \in ℕ) \to z \in ℤ$
9	1	adantl	$⊢ (z \in ℤ \land n \in ℕ) \to n \in ℤ$
10		nnne0	$⊢ n \in ℕ \to n \neq 0$
11	10	neneqd	$⊢ n \in ℕ \to \neg n = 0$
12	11	intnand	$⊢ n \in ℕ \to \neg (z = 0 \land n = 0)$
13	12	adantl	$⊢ (z \in ℤ \land n \in ℕ) \to \neg (z = 0 \land n = 0)$
14		gcdn0cl	$⊢ ((z \in ℤ \land n \in ℤ) \land \neg (z = 0 \land n = 0)) \to z \gcd n \in ℕ$
15	8 9 13 14	syl21anc	$⊢ (z \in ℤ \land n \in ℕ) \to z \gcd n \in ℕ$
16		nnne0	$⊢ z \gcd n \in ℕ \to z \gcd n \neq 0$
17	15 16	syl	$⊢ (z \in ℤ \land n \in ℕ) \to z \gcd n \neq 0$
18		dvdsval2	$⊢ (z \gcd n \in ℤ \land z \gcd n \neq 0 \land z \in ℤ) \to ((z \gcd n) ∥ z \leftrightarrow \frac{z}{z \gcd n} \in ℤ)$
19	7 17 8 18	syl3anc	$⊢ (z \in ℤ \land n \in ℕ) \to ((z \gcd n) ∥ z \leftrightarrow \frac{z}{z \gcd n} \in ℤ)$
20	4 19	mpbid	$⊢ (z \in ℤ \land n \in ℕ) \to \frac{z}{z \gcd n} \in ℤ$
21	20	3adant3	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to \frac{z}{z \gcd n} \in ℤ$
22	2	simprd	$⊢ (z \in ℤ \land n \in ℤ) \to (z \gcd n) ∥ n$
23	1 22	sylan2	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) ∥ n$
24		dvdsval2	$⊢ (z \gcd n \in ℤ \land z \gcd n \neq 0 \land n \in ℤ) \to ((z \gcd n) ∥ n \leftrightarrow \frac{n}{z \gcd n} \in ℤ)$
25	7 17 9 24	syl3anc	$⊢ (z \in ℤ \land n \in ℕ) \to ((z \gcd n) ∥ n \leftrightarrow \frac{n}{z \gcd n} \in ℤ)$
26	23 25	mpbid	$⊢ (z \in ℤ \land n \in ℕ) \to \frac{n}{z \gcd n} \in ℤ$
27		nnre	$⊢ n \in ℕ \to n \in ℝ$
28	27	adantl	$⊢ (z \in ℤ \land n \in ℕ) \to n \in ℝ$
29	6	nn0red	$⊢ (z \in ℤ \land n \in ℕ) \to z \gcd n \in ℝ$
30		nngt0	$⊢ n \in ℕ \to 0 < n$
31	30	adantl	$⊢ (z \in ℤ \land n \in ℕ) \to 0 < n$
32		nngt0	$⊢ z \gcd n \in ℕ \to 0 < z \gcd n$
33	15 32	syl	$⊢ (z \in ℤ \land n \in ℕ) \to 0 < z \gcd n$
34	28 29 31 33	divgt0d	$⊢ (z \in ℤ \land n \in ℕ) \to 0 < \frac{n}{z \gcd n}$
35	26 34	jca	$⊢ (z \in ℤ \land n \in ℕ) \to (\frac{n}{z \gcd n} \in ℤ \land 0 < \frac{n}{z \gcd n})$
36	35	3adant3	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to (\frac{n}{z \gcd n} \in ℤ \land 0 < \frac{n}{z \gcd n})$
37		elnnz	$⊢ \frac{n}{z \gcd n} \in ℕ \leftrightarrow (\frac{n}{z \gcd n} \in ℤ \land 0 < \frac{n}{z \gcd n})$
38	36 37	sylibr	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to \frac{n}{z \gcd n} \in ℕ$
39	21 38	opelxpd	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \in (ℤ \times ℕ)$
40	20 26	gcdcld	$⊢ (z \in ℤ \land n \in ℕ) \to (\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) \in ℕ_{0}$
41	40	nn0cnd	$⊢ (z \in ℤ \land n \in ℕ) \to (\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) \in ℂ$
42		1cnd	$⊢ (z \in ℤ \land n \in ℕ) \to 1 \in ℂ$
43	6	nn0cnd	$⊢ (z \in ℤ \land n \in ℕ) \to z \gcd n \in ℂ$
44	43	mulid1d	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) \cdot 1 = z \gcd n$
45		zcn	$⊢ z \in ℤ \to z \in ℂ$
46	45	adantr	$⊢ (z \in ℤ \land n \in ℕ) \to z \in ℂ$
47	46 43 17	divcan2d	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) (\frac{z}{z \gcd n}) = z$
48		nncn	$⊢ n \in ℕ \to n \in ℂ$
49	48	adantl	$⊢ (z \in ℤ \land n \in ℕ) \to n \in ℂ$
50	49 43 17	divcan2d	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) (\frac{n}{z \gcd n}) = n$
51	47 50	oveq12d	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) (\frac{z}{z \gcd n}) \gcd (z \gcd n) (\frac{n}{z \gcd n}) = z \gcd n$
52		mulgcd	$⊢ (z \gcd n \in ℕ_{0} \land \frac{z}{z \gcd n} \in ℤ \land \frac{n}{z \gcd n} \in ℤ) \to (z \gcd n) (\frac{z}{z \gcd n}) \gcd (z \gcd n) (\frac{n}{z \gcd n}) = (z \gcd n) ((\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}))$
53	6 20 26 52	syl3anc	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) (\frac{z}{z \gcd n}) \gcd (z \gcd n) (\frac{n}{z \gcd n}) = (z \gcd n) ((\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}))$
54	44 51 53	3eqtr2rd	$⊢ (z \in ℤ \land n \in ℕ) \to (z \gcd n) ((\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n})) = (z \gcd n) \cdot 1$
55	41 42 43 17 54	mulcanad	$⊢ (z \in ℤ \land n \in ℕ) \to (\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) = 1$
56	55	3adant3	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to (\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) = 1$
57	10	adantl	$⊢ (z \in ℤ \land n \in ℕ) \to n \neq 0$
58	46 49 43 57 17	divcan7d	$⊢ (z \in ℤ \land n \in ℕ) \to \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}} = \frac{z}{n}$
59	58	eqeq2d	$⊢ (z \in ℤ \land n \in ℕ) \to (A = \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}} \leftrightarrow A = \frac{z}{n})$
60	59	biimp3ar	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to A = \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}}$
61		ovex	$⊢ \frac{z}{z \gcd n} \in V$
62		ovex	$⊢ \frac{n}{z \gcd n} \in V$
63	61 62	op1std	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to 1^{st} (x) = \frac{z}{z \gcd n}$
64	61 62	op2ndd	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to 2^{nd} (x) = \frac{n}{z \gcd n}$
65	63 64	oveq12d	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to 1^{st} (x) \gcd 2^{nd} (x) = (\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n})$
66	65	eqeq1d	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to (1^{st} (x) \gcd 2^{nd} (x) = 1 \leftrightarrow (\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) = 1)$
67	63 64	oveq12d	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to \frac{1^{st} (x)}{2^{nd} (x)} = \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}}$
68	67	eqeq2d	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to (A = \frac{1^{st} (x)}{2^{nd} (x)} \leftrightarrow A = \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}})$
69	66 68	anbi12d	$⊢ x = ⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \to ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \leftrightarrow ((\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) = 1 \land A = \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}}))$
70	69	rspcev	$⊢ (⟨\frac{z}{z \gcd n}, \frac{n}{z \gcd n}⟩ \in (ℤ \times ℕ) \land ((\frac{z}{z \gcd n}) \gcd (\frac{n}{z \gcd n}) = 1 \land A = \frac{\frac{z}{z \gcd n}}{\frac{n}{z \gcd n}})) \to \exists x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)})$
71	39 56 60 70	syl12anc	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to \exists x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)})$
72		elxp6	$⊢ x \in (ℤ \times ℕ) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ))$
73		elxp6	$⊢ y \in (ℤ \times ℕ) \leftrightarrow (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))$
74		simprl	$⊢ (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \to 1^{st} (x) \in ℤ$
75	74	ad2antrr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to 1^{st} (x) \in ℤ$
76		simprr	$⊢ (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \to 2^{nd} (x) \in ℕ$
77	76	ad2antrr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to 2^{nd} (x) \in ℕ$
78		simprll	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to 1^{st} (x) \gcd 2^{nd} (x) = 1$
79		simprl	$⊢ (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ)) \to 1^{st} (y) \in ℤ$
80	79	ad2antlr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to 1^{st} (y) \in ℤ$
81		simprr	$⊢ (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ)) \to 2^{nd} (y) \in ℕ$
82	81	ad2antlr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to 2^{nd} (y) \in ℕ$
83		simprrl	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to 1^{st} (y) \gcd 2^{nd} (y) = 1$
84		simprlr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to A = \frac{1^{st} (x)}{2^{nd} (x)}$
85		simprrr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to A = \frac{1^{st} (y)}{2^{nd} (y)}$
86	84 85	eqtr3d	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to \frac{1^{st} (x)}{2^{nd} (x)} = \frac{1^{st} (y)}{2^{nd} (y)}$
87		qredeq	$⊢ ((1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ \land 1^{st} (x) \gcd 2^{nd} (x) = 1) \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ \land 1^{st} (y) \gcd 2^{nd} (y) = 1) \land \frac{1^{st} (x)}{2^{nd} (x)} = \frac{1^{st} (y)}{2^{nd} (y)}) \to (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y))$
88	75 77 78 80 82 83 86 87	syl331anc	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y))$
89		fvex	$⊢ 1^{st} (x) \in V$
90		fvex	$⊢ 2^{nd} (x) \in V$
91	89 90	opth	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩ \leftrightarrow (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y))$
92	88 91	sylibr	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩$
93		simplll	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
94		simplrl	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
95	92 93 94	3eqtr4d	$⊢ (((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \land ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))) \to x = y$
96	95	ex	$⊢ ((x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in ℤ \land 2^{nd} (x) \in ℕ)) \land (y = ⟨1^{st} (y), 2^{nd} (y)⟩ \land (1^{st} (y) \in ℤ \land 2^{nd} (y) \in ℕ))) \to (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y)$
97	72 73 96	syl2anb	$⊢ (x \in (ℤ \times ℕ) \land y \in (ℤ \times ℕ)) \to (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y)$
98	97	rgen2	$⊢ \forall x \in (ℤ \times ℕ) \forall y \in (ℤ \times ℕ) (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y)$
99	71 98	jctir	$⊢ (z \in ℤ \land n \in ℕ \land A = \frac{z}{n}) \to (\exists x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land \forall x \in (ℤ \times ℕ) \forall y \in (ℤ \times ℕ) (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y))$
100	99	3expia	$⊢ (z \in ℤ \land n \in ℕ) \to (A = \frac{z}{n} \to (\exists x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land \forall x \in (ℤ \times ℕ) \forall y \in (ℤ \times ℕ) (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y)))$
101	100	rexlimivv	$⊢ \exists z \in ℤ \exists n \in ℕ A = \frac{z}{n} \to (\exists x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land \forall x \in (ℤ \times ℕ) \forall y \in (ℤ \times ℕ) (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y))$
102		elq	$⊢ A \in ℚ \leftrightarrow \exists z \in ℤ \exists n \in ℕ A = \frac{z}{n}$
103		fveq2	$⊢ x = y \to 1^{st} (x) = 1^{st} (y)$
104		fveq2	$⊢ x = y \to 2^{nd} (x) = 2^{nd} (y)$
105	103 104	oveq12d	$⊢ x = y \to 1^{st} (x) \gcd 2^{nd} (x) = 1^{st} (y) \gcd 2^{nd} (y)$
106	105	eqeq1d	$⊢ x = y \to (1^{st} (x) \gcd 2^{nd} (x) = 1 \leftrightarrow 1^{st} (y) \gcd 2^{nd} (y) = 1)$
107	103 104	oveq12d	$⊢ x = y \to \frac{1^{st} (x)}{2^{nd} (x)} = \frac{1^{st} (y)}{2^{nd} (y)}$
108	107	eqeq2d	$⊢ x = y \to (A = \frac{1^{st} (x)}{2^{nd} (x)} \leftrightarrow A = \frac{1^{st} (y)}{2^{nd} (y)})$
109	106 108	anbi12d	$⊢ x = y \to ((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \leftrightarrow (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)}))$
110	109	reu4	$⊢ \exists! x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \leftrightarrow (\exists x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land \forall x \in (ℤ \times ℕ) \forall y \in (ℤ \times ℕ) (((1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)}) \land (1^{st} (y) \gcd 2^{nd} (y) = 1 \land A = \frac{1^{st} (y)}{2^{nd} (y)})) \to x = y))$
111	101 102 110	3imtr4i	$⊢ A \in ℚ \to \exists! x \in (ℤ \times ℕ) (1^{st} (x) \gcd 2^{nd} (x) = 1 \land A = \frac{1^{st} (x)}{2^{nd} (x)})$

Metamath Proof Explorer

Theorem qredeu

Proof