qredeu - Intuitionistic Logic Explorer

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

Theorem qredeu 12858

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 9646	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
2		gcddvds 12723	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ∧ (𝑧 gcd 𝑛) ∥ 𝑛))
3	2	simpld 112	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑧)
4	1, 3	sylan2 286	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑧)
5		gcdcl 12726	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
6	1, 5	sylan2 286	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
7	6	nn0zd 9749	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℤ)
8		simpl 109	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℤ)
9	1	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
10		nnne0 9315	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
11	10	neneqd 2441	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ¬ 𝑛 = 0)
12	11	intnand 943	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
13	12	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
14		gcdn0cl 12722	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬ (𝑧 = 0 ∧ 𝑛 = 0)) → (𝑧 gcd 𝑛) ∈ ℕ)
15	8, 9, 13, 14	syl21anc 1277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ)
16	15	nnne0d 9332	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ≠ 0)
17		dvdsval2 12540	. . . . . . . . . 10 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
18	7, 16, 8, 17	syl3anc 1278	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
19	4, 18	mpbid 147	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
20	19	3adant3 1048	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
21	2	simprd 114	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑛)
22	1, 21	sylan2 286	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑛)
23		dvdsval2 12540	. . . . . . . . . . . 12 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
24	7, 16, 9, 23	syl3anc 1278	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
25	22, 24	mpbid 147	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)
26		nnre 9294	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
27	26	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
28	6	nn0red 9604	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℝ)
29		nngt0 9312	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
30	29	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
31	15	nngt0d 9331	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑧 gcd 𝑛))
32	27, 28, 30, 31	divgt0d 9259	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑛 / (𝑧 gcd 𝑛)))
33	25, 32	jca 306	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
34	33	3adant3 1048	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
35		elnnz 9637	. . . . . . . 8 ⊢ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ ↔ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
36	34, 35	sylibr 134	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ)
37		opelxpi 4804	. . . . . . 7 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
38	20, 36, 37	syl2anc 415	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
39		fveq2 5693	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (1^st ‘𝑥) = (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
40		simp1 1028	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑧 ∈ ℤ)
41	15	3adant3 1048	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 gcd 𝑛) ∈ ℕ)
42		znq 10007	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
43	40, 41, 42	syl2anc 415	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
44	9	3adant3 1048	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑛 ∈ ℤ)
45		znq 10007	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
46	44, 41, 45	syl2anc 415	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
47		op1stg 6378	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
48	43, 46, 47	syl2anc 415	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
49	39, 48	sylan9eqr 2293	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (1^st ‘𝑥) = (𝑧 / (𝑧 gcd 𝑛)))
50		fveq2 5693	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (2^nd ‘𝑥) = (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
51		op2ndg 6379	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
52	43, 46, 51	syl2anc 415	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
53	50, 52	sylan9eqr 2293	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (2^nd ‘𝑥) = (𝑛 / (𝑧 gcd 𝑛)))
54	49, 53	oveq12d 6097	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))
55	54	eqeq1d 2247	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1))
56	49, 53	oveq12d 6097	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
57	56	eqeq2d 2250	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
58	55, 57	anbi12d 477	. . . . . 6 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))))
59	19, 25	gcdcld 12728	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℕ₀)
60	59	nn0cnd 9605	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℂ)
61		1cnd 8336	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
62	6	nn0cnd 9605	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℂ)
63	15	nnap0d 9333	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) # 0)
64	62	mulridd 8337	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · 1) = (𝑧 gcd 𝑛))
65		zcn 9632	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
66	65	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ)
67	66, 62, 63	divcanap2d 9116	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) = 𝑧)
68		nncn 9295	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
69	68	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
70	69, 62, 63	divcanap2d 9116	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛))) = 𝑛)
71	67, 70	oveq12d 6097	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = (𝑧 gcd 𝑛))
72		mulgcd 12776	. . . . . . . . . . 11 ⊢ (((𝑧 gcd 𝑛) ∈ ℕ₀ ∧ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
73	6, 19, 25, 72	syl3anc 1278	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
74	64, 71, 73	3eqtr2rd 2278	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · 1))
75	60, 61, 62, 63, 74	mulcanapad 8985	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
76	75	3adant3 1048	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
77		nnap0 9316	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → 𝑛 # 0)
78	77	adantl 277	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 # 0)
79	66, 69, 62, 78, 63	divcanap7d 9143	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) = (𝑧 / 𝑛))
80	79	eqeq2d 2250	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) ↔ 𝐴 = (𝑧 / 𝑛)))
81	80	biimp3ar 1387	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
82	76, 81	jca 306	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
83	38, 58, 82	rspcedvd 2935	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
84		elxp6 6397	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ × ℕ) ↔ (𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)))
85		elxp6 6397	. . . . . . 7 ⊢ (𝑦 ∈ (ℤ × ℕ) ↔ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)))
86		simprl 535	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (1^st ‘𝑥) ∈ ℤ)
87	86	ad2antrr 492	. . . . . . . . . . 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 537	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (2^nd ‘𝑥) ∈ ℕ)
89	88	ad2antrr 492	. . . . . . . . . . 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 543	. . . . . . . . . . 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 535	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (1^st ‘𝑦) ∈ ℤ)
92	91	ad2antlr 493	. . . . . . . . . . 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 537	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (2^nd ‘𝑦) ∈ ℕ)
94	93	ad2antlr 493	. . . . . . . . . . 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 545	. . . . . . . . . . 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 544	. . . . . . . . . . . 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 546	. . . . . . . . . . . 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 2273	. . . . . . . . . . 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 12857	. . . . . . . . . . 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 1303	. . . . . . . . . 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 2824	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
102		1stexg 6395	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (1^st ‘𝑥) ∈ V)
103	101, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (1^st ‘𝑥) ∈ V
104		2ndexg 6396	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (2^nd ‘𝑥) ∈ V)
105	101, 104	ax-mp 5	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑥) ∈ V
106	103, 105	opth 4375	. . . . . . . . . 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 539	. . . . . . . . 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 541	. . . . . . . . 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 2281	. . . . . . . 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 2604	. . . . 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 1236	. . 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 2674	. 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 10005	. 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛))
118		fveq2 5693	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1^st ‘𝑥) = (1^st ‘𝑦))
119		fveq2 5693	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2^nd ‘𝑥) = (2^nd ‘𝑦))
120	118, 119	oveq12d 6097	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((1^st ‘𝑦) gcd (2^nd ‘𝑦)))
121	120	eqeq1d 2247	. . . 4 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1))
122	118, 119	oveq12d 6097	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
123	122	eqeq2d 2250	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))
124	121, 123	anbi12d 477	. . 3 ⊢ (𝑥 = 𝑦 → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))))
125	124	reu4 3020	. 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 1009 = wceq 1402 ∈ wcel 2209 ≠ wne 2420 ∀wral 2528 ∃wrex 2529 ∃!wreu 2530 Vcvv 2821 ⟨cop 3711 class class class wbr 4128 × cxp 4770 ‘cfv 5375 (class class class)co 6079 1^st c1st 6366 2^nd c2nd 6367 ℂcc 8171 ℝcr 8172 0cc0 8173 1c1 8174 · cmul 8178 < clt 8354 # cap 8903 / cdiv 8996 ℕcn 9287 ℕ₀cn0 9546 ℤcz 9627 ℚcq 10002 ∥ cdvds 12537 gcd cgcd 12713

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-1st 6368 df-2nd 6369 df-recs 6570 df-frec 6656 df-sup 7318 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-fz 10395 df-fzo 10533 df-fl 10688 df-mod 10743 df-seqfrec 10868 df-exp 10959 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-dvds 12538 df-gcd 12714

This theorem is referenced by: qnumdencl 12948 qnumdenbi 12953

W3C validator