qredeu - Intuitionistic Logic Explorer

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

Theorem qredeu 12787

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 9592	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
2		gcddvds 12652	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ∧ (𝑧 gcd 𝑛) ∥ 𝑛))
3	2	simpld 112	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑧)
4	1, 3	sylan2 286	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑧)
5		gcdcl 12655	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
6	1, 5	sylan2 286	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
7	6	nn0zd 9694	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℤ)
8		simpl 109	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℤ)
9	1	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
10		nnne0 9261	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
11	10	neneqd 2433	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ¬ 𝑛 = 0)
12	11	intnand 939	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
13	12	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
14		gcdn0cl 12651	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬ (𝑧 = 0 ∧ 𝑛 = 0)) → (𝑧 gcd 𝑛) ∈ ℕ)
15	8, 9, 13, 14	syl21anc 1273	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ)
16	15	nnne0d 9278	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ≠ 0)
17		dvdsval2 12469	. . . . . . . . . 10 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
18	7, 16, 8, 17	syl3anc 1274	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
19	4, 18	mpbid 147	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
20	19	3adant3 1044	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
21	2	simprd 114	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑛)
22	1, 21	sylan2 286	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑛)
23		dvdsval2 12469	. . . . . . . . . . . 12 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
24	7, 16, 9, 23	syl3anc 1274	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
25	22, 24	mpbid 147	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)
26		nnre 9240	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
27	26	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
28	6	nn0red 9550	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℝ)
29		nngt0 9258	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
30	29	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
31	15	nngt0d 9277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑧 gcd 𝑛))
32	27, 28, 30, 31	divgt0d 9205	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑛 / (𝑧 gcd 𝑛)))
33	25, 32	jca 306	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
34	33	3adant3 1044	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
35		elnnz 9583	. . . . . . . 8 ⊢ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ ↔ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
36	34, 35	sylibr 134	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ)
37		opelxpi 4780	. . . . . . 7 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
38	20, 36, 37	syl2anc 411	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
39		fveq2 5669	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (1^st ‘𝑥) = (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
40		simp1 1024	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑧 ∈ ℤ)
41	15	3adant3 1044	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 gcd 𝑛) ∈ ℕ)
42		znq 9952	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
43	40, 41, 42	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
44	9	3adant3 1044	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑛 ∈ ℤ)
45		znq 9952	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
46	44, 41, 45	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
47		op1stg 6343	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
48	43, 46, 47	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
49	39, 48	sylan9eqr 2287	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (1^st ‘𝑥) = (𝑧 / (𝑧 gcd 𝑛)))
50		fveq2 5669	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (2^nd ‘𝑥) = (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
51		op2ndg 6344	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
52	43, 46, 51	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
53	50, 52	sylan9eqr 2287	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (2^nd ‘𝑥) = (𝑛 / (𝑧 gcd 𝑛)))
54	49, 53	oveq12d 6067	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))
55	54	eqeq1d 2241	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1))
56	49, 53	oveq12d 6067	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
57	56	eqeq2d 2244	. . . . . . 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 12657	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℕ₀)
60	59	nn0cnd 9551	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℂ)
61		1cnd 8286	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
62	6	nn0cnd 9551	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℂ)
63	15	nnap0d 9279	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) # 0)
64	62	mulridd 8287	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · 1) = (𝑧 gcd 𝑛))
65		zcn 9578	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
66	65	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ)
67	66, 62, 63	divcanap2d 9062	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) = 𝑧)
68		nncn 9241	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
69	68	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
70	69, 62, 63	divcanap2d 9062	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛))) = 𝑛)
71	67, 70	oveq12d 6067	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = (𝑧 gcd 𝑛))
72		mulgcd 12705	. . . . . . . . . . 11 ⊢ (((𝑧 gcd 𝑛) ∈ ℕ₀ ∧ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
73	6, 19, 25, 72	syl3anc 1274	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
74	64, 71, 73	3eqtr2rd 2272	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · 1))
75	60, 61, 62, 63, 74	mulcanapad 8933	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
76	75	3adant3 1044	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
77		nnap0 9262	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → 𝑛 # 0)
78	77	adantl 277	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 # 0)
79	66, 69, 62, 78, 63	divcanap7d 9089	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) = (𝑧 / 𝑛))
80	79	eqeq2d 2244	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) ↔ 𝐴 = (𝑧 / 𝑛)))
81	80	biimp3ar 1383	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
82	76, 81	jca 306	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
83	38, 58, 82	rspcedvd 2926	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
84		elxp6 6362	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ × ℕ) ↔ (𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)))
85		elxp6 6362	. . . . . . 7 ⊢ (𝑦 ∈ (ℤ × ℕ) ↔ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)))
86		simprl 531	. . . . . . . . . . . 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 533	. . . . . . . . . . . 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 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)
91		simprl 531	. . . . . . . . . . . 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 533	. . . . . . . . . . . 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 541	. . . . . . . . . . 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 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 ‘𝑥)))
97		simprrr 542	. . . . . . . . . . . 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 2267	. . . . . . . . . . 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 12786	. . . . . . . . . . 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 1299	. . . . . . . . . 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 2815	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
102		1stexg 6360	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (1^st ‘𝑥) ∈ V)
103	101, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (1^st ‘𝑥) ∈ V
104		2ndexg 6361	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (2^nd ‘𝑥) ∈ V)
105	101, 104	ax-mp 5	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑥) ∈ V
106	103, 105	opth 4352	. . . . . . . . . 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 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 ‘𝑥)⟩)
109		simplrl 537	. . . . . . . . 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 2275	. . . . . . . 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 2596	. . . . 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 1232	. . 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 2666	. 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 9950	. 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛))
118		fveq2 5669	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1^st ‘𝑥) = (1^st ‘𝑦))
119		fveq2 5669	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2^nd ‘𝑥) = (2^nd ‘𝑦))
120	118, 119	oveq12d 6067	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((1^st ‘𝑦) gcd (2^nd ‘𝑦)))
121	120	eqeq1d 2241	. . . 4 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1))
122	118, 119	oveq12d 6067	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
123	122	eqeq2d 2244	. . . 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 3010	. 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 1005 = wceq 1398 ∈ wcel 2203 ≠ wne 2412 ∀wral 2520 ∃wrex 2521 ∃!wreu 2522 Vcvv 2812 ⟨cop 3691 class class class wbr 4108 × cxp 4746 ‘cfv 5351 (class class class)co 6049 1^st c1st 6331 2^nd c2nd 6332 ℂcc 8121 ℝcr 8122 0cc0 8123 1c1 8124 · cmul 8128 < clt 8304 # cap 8851 / cdiv 8942 ℕcn 9233 ℕ₀cn0 9492 ℤcz 9573 ℚcq 9947 ∥ cdvds 12466 gcd cgcd 12642

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4224 ax-sep 4227 ax-nul 4235 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-iinf 4709 ax-cnex 8214 ax-resscn 8215 ax-1cn 8216 ax-1re 8217 ax-icn 8218 ax-addcl 8219 ax-addrcl 8220 ax-mulcl 8221 ax-mulrcl 8222 ax-addcom 8223 ax-mulcom 8224 ax-addass 8225 ax-mulass 8226 ax-distr 8227 ax-i2m1 8228 ax-0lt1 8229 ax-1rid 8230 ax-0id 8231 ax-rnegex 8232 ax-precex 8233 ax-cnre 8234 ax-pre-ltirr 8235 ax-pre-ltwlin 8236 ax-pre-lttrn 8237 ax-pre-apti 8238 ax-pre-ltadd 8239 ax-pre-mulgt0 8240 ax-pre-mulext 8241 ax-arch 8242 ax-caucvg 8243

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2814 df-sbc 3042 df-csb 3138 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-nul 3508 df-if 3620 df-pw 3670 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-int 3949 df-iun 3992 df-br 4109 df-opab 4171 df-mpt 4172 df-tr 4208 df-id 4413 df-po 4416 df-iso 4417 df-iord 4486 df-on 4488 df-ilim 4489 df-suc 4491 df-iom 4712 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-rn 4759 df-res 4760 df-ima 4761 df-iota 5311 df-fun 5353 df-fn 5354 df-f 5355 df-f1 5356 df-fo 5357 df-f1o 5358 df-fv 5359 df-riota 6002 df-ov 6052 df-oprab 6053 df-mpo 6054 df-1st 6333 df-2nd 6334 df-recs 6535 df-frec 6621 df-sup 7274 df-pnf 8306 df-mnf 8307 df-xr 8308 df-ltxr 8309 df-le 8310 df-sub 8442 df-neg 8443 df-reap 8845 df-ap 8852 df-div 8943 df-inn 9234 df-2 9292 df-3 9293 df-4 9294 df-n0 9493 df-z 9574 df-uz 9850 df-q 9948 df-rp 9983 df-fz 10339 df-fzo 10473 df-fl 10626 df-mod 10681 df-seqfrec 10806 df-exp 10897 df-cj 11520 df-re 11521 df-im 11522 df-rsqrt 11676 df-abs 11677 df-dvds 12467 df-gcd 12643

This theorem is referenced by: qnumdencl 12877 qnumdenbi 12882

W3C validator