qredeu - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > qredeu		GIF version

Theorem qredeu 12080

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

**Assertion**
Ref	Expression
qredeu	⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))

Distinct variable group: 𝑥,𝐴

Proof of Theorem qredeu Dummy variables 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnz 9261	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
2		gcddvds 11947	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ∧ (𝑧 gcd 𝑛) ∥ 𝑛))
3	2	simpld 112	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑧)
4	1, 3	sylan2 286	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑧)
5		gcdcl 11950	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
6	1, 5	sylan2 286	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
7	6	nn0zd 9362	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℤ)
8		simpl 109	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℤ)
9	1	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
10		nnne0 8936	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
11	10	neneqd 2368	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ¬ 𝑛 = 0)
12	11	intnand 931	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
13	12	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
14		gcdn0cl 11946	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬ (𝑧 = 0 ∧ 𝑛 = 0)) → (𝑧 gcd 𝑛) ∈ ℕ)
15	8, 9, 13, 14	syl21anc 1237	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ)
16	15	nnne0d 8953	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ≠ 0)
17		dvdsval2 11781	. . . . . . . . . 10 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
18	7, 16, 8, 17	syl3anc 1238	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
19	4, 18	mpbid 147	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
20	19	3adant3 1017	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
21	2	simprd 114	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑛)
22	1, 21	sylan2 286	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑛)
23		dvdsval2 11781	. . . . . . . . . . . 12 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
24	7, 16, 9, 23	syl3anc 1238	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
25	22, 24	mpbid 147	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)
26		nnre 8915	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
27	26	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
28	6	nn0red 9219	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℝ)
29		nngt0 8933	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
30	29	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
31	15	nngt0d 8952	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑧 gcd 𝑛))
32	27, 28, 30, 31	divgt0d 8881	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑛 / (𝑧 gcd 𝑛)))
33	25, 32	jca 306	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
34	33	3adant3 1017	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
35		elnnz 9252	. . . . . . . 8 ⊢ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ ↔ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
36	34, 35	sylibr 134	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ)
37		opelxpi 4655	. . . . . . 7 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
38	20, 36, 37	syl2anc 411	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
39		fveq2 5511	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (1^st ‘𝑥) = (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
40		simp1 997	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑧 ∈ ℤ)
41	15	3adant3 1017	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 gcd 𝑛) ∈ ℕ)
42		znq 9613	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
43	40, 41, 42	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
44	9	3adant3 1017	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑛 ∈ ℤ)
45		znq 9613	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
46	44, 41, 45	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
47		op1stg 6145	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
48	43, 46, 47	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
49	39, 48	sylan9eqr 2232	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (1^st ‘𝑥) = (𝑧 / (𝑧 gcd 𝑛)))
50		fveq2 5511	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (2^nd ‘𝑥) = (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
51		op2ndg 6146	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
52	43, 46, 51	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
53	50, 52	sylan9eqr 2232	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (2^nd ‘𝑥) = (𝑛 / (𝑧 gcd 𝑛)))
54	49, 53	oveq12d 5887	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))
55	54	eqeq1d 2186	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1))
56	49, 53	oveq12d 5887	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
57	56	eqeq2d 2189	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
58	55, 57	anbi12d 473	. . . . . 6 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))))
59	19, 25	gcdcld 11952	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℕ₀)
60	59	nn0cnd 9220	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℂ)
61		1cnd 7964	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
62	6	nn0cnd 9220	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℂ)
63	15	nnap0d 8954	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) # 0)
64	62	mulid1d 7965	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · 1) = (𝑧 gcd 𝑛))
65		zcn 9247	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
66	65	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ)
67	66, 62, 63	divcanap2d 8738	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) = 𝑧)
68		nncn 8916	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
69	68	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
70	69, 62, 63	divcanap2d 8738	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛))) = 𝑛)
71	67, 70	oveq12d 5887	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = (𝑧 gcd 𝑛))
72		mulgcd 12000	. . . . . . . . . . 11 ⊢ (((𝑧 gcd 𝑛) ∈ ℕ₀ ∧ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
73	6, 19, 25, 72	syl3anc 1238	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
74	64, 71, 73	3eqtr2rd 2217	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · 1))
75	60, 61, 62, 63, 74	mulcanapad 8609	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
76	75	3adant3 1017	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
77		nnap0 8937	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → 𝑛 # 0)
78	77	adantl 277	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 # 0)
79	66, 69, 62, 78, 63	divcanap7d 8765	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) = (𝑧 / 𝑛))
80	79	eqeq2d 2189	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) ↔ 𝐴 = (𝑧 / 𝑛)))
81	80	biimp3ar 1346	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
82	76, 81	jca 306	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
83	38, 58, 82	rspcedvd 2847	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
84		elxp6 6164	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ × ℕ) ↔ (𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)))
85		elxp6 6164	. . . . . . 7 ⊢ (𝑦 ∈ (ℤ × ℕ) ↔ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)))
86		simprl 529	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (1^st ‘𝑥) ∈ ℤ)
87	86	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → (1^st ‘𝑥) ∈ ℤ)
88		simprr 531	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (2^nd ‘𝑥) ∈ ℕ)
89	88	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → (2^nd ‘𝑥) ∈ ℕ)
90		simprll 537	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1)
91		simprl 529	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (1^st ‘𝑦) ∈ ℤ)
92	91	ad2antlr 489	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → (1^st ‘𝑦) ∈ ℤ)
93		simprr 531	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (2^nd ‘𝑦) ∈ ℕ)
94	93	ad2antlr 489	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → (2^nd ‘𝑦) ∈ ℕ)
95		simprrl 539	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1)
96		simprlr 538	. . . . . . . . . . . 12 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)))
97		simprrr 540	. . . . . . . . . . . 12 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
98	96, 97	eqtr3d 2212	. . . . . . . . . . 11 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
99		qredeq 12079	. . . . . . . . . . 11 ⊢ ((((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ ∧ ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1) ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ ∧ ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1) ∧ ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦))) → ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
100	87, 89, 90, 92, 94, 95, 98, 99	syl331anc 1263	. . . . . . . . . 10 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
101		vex 2740	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
102		1stexg 6162	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (1^st ‘𝑥) ∈ V)
103	101, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (1^st ‘𝑥) ∈ V
104		2ndexg 6163	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (2^nd ‘𝑥) ∈ V)
105	101, 104	ax-mp 5	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑥) ∈ V
106	103, 105	opth 4234	. . . . . . . . . 10 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
107	100, 106	sylibr 134	. . . . . . . . 9 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
108		simplll 533	. . . . . . . . 9 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
109		simplrl 535	. . . . . . . . 9 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
110	107, 108, 109	3eqtr4d 2220	. . . . . . . 8 ⊢ ((((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) ∧ ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))) → 𝑥 = 𝑦)
111	110	ex 115	. . . . . . 7 ⊢ (((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ))) → (((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦))
112	84, 85, 111	syl2anb 291	. . . . . 6 ⊢ ((𝑥 ∈ (ℤ × ℕ) ∧ 𝑦 ∈ (ℤ × ℕ)) → (((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦))
113	112	rgen2a 2531	. . . . 5 ⊢ ∀𝑥 ∈ (ℤ × ℕ)∀𝑦 ∈ (ℤ × ℕ)(((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦)
114	83, 113	jctir 313	. . . 4 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ × ℕ)∀𝑦 ∈ (ℤ × ℕ)(((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦)))
115	114	3expia 1205	. . 3 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = (𝑧 / 𝑛) → (∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ × ℕ)∀𝑦 ∈ (ℤ × ℕ)(((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦))))
116	115	rexlimivv 2600	. 2 ⊢ (∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛) → (∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ × ℕ)∀𝑦 ∈ (ℤ × ℕ)(((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦)))
117		elq 9611	. 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛))
118		fveq2 5511	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1^st ‘𝑥) = (1^st ‘𝑦))
119		fveq2 5511	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2^nd ‘𝑥) = (2^nd ‘𝑦))
120	118, 119	oveq12d 5887	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((1^st ‘𝑦) gcd (2^nd ‘𝑦)))
121	120	eqeq1d 2186	. . . 4 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1))
122	118, 119	oveq12d 5887	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
123	122	eqeq2d 2189	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))
124	121, 123	anbi12d 473	. . 3 ⊢ (𝑥 = 𝑦 → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))))
125	124	reu4 2931	. 2 ⊢ (∃!𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ × ℕ)∀𝑦 ∈ (ℤ × ℕ)(((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦)))
126	116, 117, 125	3imtr4i 201	1 ⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 ≠ wne 2347 ∀wral 2455 ∃wrex 2456 ∃!wreu 2457 Vcvv 2737 ⟨cop 3594 class class class wbr 4000 × cxp 4621 ‘cfv 5212 (class class class)co 5869 1^st c1st 6133 2^nd c2nd 6134 ℂcc 7800 ℝcr 7801 0cc0 7802 1c1 7803 · cmul 7807 < clt 7982 # cap 8528 / cdiv 8618 ℕcn 8908 ℕ₀cn0 9165 ℤcz 9242 ℚcq 9608 ∥ cdvds 11778 gcd cgcd 11926

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921 ax-caucvg 7922

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-frec 6386 df-sup 6977 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-fz 9996 df-fzo 10129 df-fl 10256 df-mod 10309 df-seqfrec 10432 df-exp 10506 df-cj 10835 df-re 10836 df-im 10837 df-rsqrt 10991 df-abs 10992 df-dvds 11779 df-gcd 11927

This theorem is referenced by: qnumdencl 12170 qnumdenbi 12175

W3C validator