qredeu - Intuitionistic Logic Explorer

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

Theorem qredeu 11814

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 9097	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
2		gcddvds 11688	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ∧ (𝑧 gcd 𝑛) ∥ 𝑛))
3	2	simpld 111	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑧)
4	1, 3	sylan2 284	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑧)
5		gcdcl 11691	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
6	1, 5	sylan2 284	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ₀)
7	6	nn0zd 9195	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℤ)
8		simpl 108	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℤ)
9	1	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
10		nnne0 8772	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
11	10	neneqd 2330	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ¬ 𝑛 = 0)
12	11	intnand 917	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
13	12	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ¬ (𝑧 = 0 ∧ 𝑛 = 0))
14		gcdn0cl 11687	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬ (𝑧 = 0 ∧ 𝑛 = 0)) → (𝑧 gcd 𝑛) ∈ ℕ)
15	8, 9, 13, 14	syl21anc 1216	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ)
16	15	nnne0d 8789	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ≠ 0)
17		dvdsval2 11532	. . . . . . . . . 10 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
18	7, 16, 8, 17	syl3anc 1217	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ))
19	4, 18	mpbid 146	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
20	19	3adant3 1002	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)
21	2	simprd 113	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑛)
22	1, 21	sylan2 284	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑛)
23		dvdsval2 11532	. . . . . . . . . . . 12 ⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
24	7, 16, 9, 23	syl3anc 1217	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ))
25	22, 24	mpbid 146	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)
26		nnre 8751	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
27	26	adantl 275	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
28	6	nn0red 9055	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℝ)
29		nngt0 8769	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
30	29	adantl 275	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
31	15	nngt0d 8788	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑧 gcd 𝑛))
32	27, 28, 30, 31	divgt0d 8717	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 < (𝑛 / (𝑧 gcd 𝑛)))
33	25, 32	jca 304	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
34	33	3adant3 1002	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
35		elnnz 9088	. . . . . . . 8 ⊢ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ ↔ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛))))
36	34, 35	sylibr 133	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ)
37		opelxpi 4579	. . . . . . 7 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
38	20, 36, 37	syl2anc 409	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ ∈ (ℤ × ℕ))
39		fveq2 5429	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (1^st ‘𝑥) = (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
40		simp1 982	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑧 ∈ ℤ)
41	15	3adant3 1002	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 gcd 𝑛) ∈ ℕ)
42		znq 9443	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
43	40, 41, 42	syl2anc 409	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ)
44	9	3adant3 1002	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑛 ∈ ℤ)
45		znq 9443	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
46	44, 41, 45	syl2anc 409	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ)
47		op1stg 6056	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
48	43, 46, 47	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (1^st ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑧 / (𝑧 gcd 𝑛)))
49	39, 48	sylan9eqr 2195	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (1^st ‘𝑥) = (𝑧 / (𝑧 gcd 𝑛)))
50		fveq2 5429	. . . . . . . . . 10 ⊢ (𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩ → (2^nd ‘𝑥) = (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩))
51		op2ndg 6057	. . . . . . . . . . 11 ⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
52	43, 46, 51	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (2^nd ‘⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) = (𝑛 / (𝑧 gcd 𝑛)))
53	50, 52	sylan9eqr 2195	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (2^nd ‘𝑥) = (𝑛 / (𝑧 gcd 𝑛)))
54	49, 53	oveq12d 5800	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))
55	54	eqeq1d 2149	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1))
56	49, 53	oveq12d 5800	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
57	56	eqeq2d 2152	. . . . . . 7 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
58	55, 57	anbi12d 465	. . . . . 6 ⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = ⟨(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))⟩) → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))))
59	19, 25	gcdcld 11693	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℕ₀)
60	59	nn0cnd 9056	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℂ)
61		1cnd 7806	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
62	6	nn0cnd 9056	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℂ)
63	15	nnap0d 8790	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) # 0)
64	62	mulid1d 7807	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · 1) = (𝑧 gcd 𝑛))
65		zcn 9083	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
66	65	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ)
67	66, 62, 63	divcanap2d 8576	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) = 𝑧)
68		nncn 8752	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
69	68	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
70	69, 62, 63	divcanap2d 8576	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛))) = 𝑛)
71	67, 70	oveq12d 5800	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = (𝑧 gcd 𝑛))
72		mulgcd 11740	. . . . . . . . . . 11 ⊢ (((𝑧 gcd 𝑛) ∈ ℕ₀ ∧ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
73	6, 19, 25, 72	syl3anc 1217	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))))
74	64, 71, 73	3eqtr2rd 2180	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · 1))
75	60, 61, 62, 63, 74	mulcanapad 8448	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
76	75	3adant3 1002	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)
77		nnap0 8773	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → 𝑛 # 0)
78	77	adantl 275	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 # 0)
79	66, 69, 62, 78, 63	divcanap7d 8603	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) = (𝑧 / 𝑛))
80	79	eqeq2d 2152	. . . . . . . 8 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) ↔ 𝐴 = (𝑧 / 𝑛)))
81	80	biimp3ar 1325	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))
82	76, 81	jca 304	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))
83	38, 58, 82	rspcedvd 2799	. . . . 5 ⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ∃𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))
84		elxp6 6075	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ × ℕ) ↔ (𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)))
85		elxp6 6075	. . . . . . 7 ⊢ (𝑦 ∈ (ℤ × ℕ) ↔ (𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)))
86		simprl 521	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (1^st ‘𝑥) ∈ ℤ)
87	86	ad2antrr 480	. . . . . . . . . . 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 522	. . . . . . . . . . . 12 ⊢ ((𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∧ ((1^st ‘𝑥) ∈ ℤ ∧ (2^nd ‘𝑥) ∈ ℕ)) → (2^nd ‘𝑥) ∈ ℕ)
89	88	ad2antrr 480	. . . . . . . . . . 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 527	. . . . . . . . . . 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 521	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (1^st ‘𝑦) ∈ ℤ)
92	91	ad2antlr 481	. . . . . . . . . . 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 522	. . . . . . . . . . . 12 ⊢ ((𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∧ ((1^st ‘𝑦) ∈ ℤ ∧ (2^nd ‘𝑦) ∈ ℕ)) → (2^nd ‘𝑦) ∈ ℕ)
94	93	ad2antlr 481	. . . . . . . . . . 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 529	. . . . . . . . . . 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 528	. . . . . . . . . . . 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 530	. . . . . . . . . . . 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 2175	. . . . . . . . . . 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 11813	. . . . . . . . . . 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 1242	. . . . . . . . . 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 2692	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
102		1stexg 6073	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (1^st ‘𝑥) ∈ V)
103	101, 102	ax-mp 5	. . . . . . . . . . 11 ⊢ (1^st ‘𝑥) ∈ V
104		2ndexg 6074	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (2^nd ‘𝑥) ∈ V)
105	101, 104	ax-mp 5	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑥) ∈ V
106	103, 105	opth 4167	. . . . . . . . . 10 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
107	100, 106	sylibr 133	. . . . . . . . 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 523	. . . . . . . . 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 525	. . . . . . . . 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 2183	. . . . . . . 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 114	. . . . . . 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 289	. . . . . 6 ⊢ ((𝑥 ∈ (ℤ × ℕ) ∧ 𝑦 ∈ (ℤ × ℕ)) → (((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ∧ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))) → 𝑥 = 𝑦))
113	112	rgen2a 2489	. . . . 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 311	. . . 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 1184	. . 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 2558	. 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 9441	. 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑛 ∈ ℕ 𝐴 = (𝑧 / 𝑛))
118		fveq2 5429	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1^st ‘𝑥) = (1^st ‘𝑦))
119		fveq2 5429	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2^nd ‘𝑥) = (2^nd ‘𝑦))
120	118, 119	oveq12d 5800	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = ((1^st ‘𝑦) gcd (2^nd ‘𝑦)))
121	120	eqeq1d 2149	. . . 4 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ↔ ((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1))
122	118, 119	oveq12d 5800	. . . . 5 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝑥) / (2^nd ‘𝑥)) = ((1^st ‘𝑦) / (2^nd ‘𝑦)))
123	122	eqeq2d 2152	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥)) ↔ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦))))
124	121, 123	anbi12d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))) ↔ (((1^st ‘𝑦) gcd (2^nd ‘𝑦)) = 1 ∧ 𝐴 = ((1^st ‘𝑦) / (2^nd ‘𝑦)))))
125	124	reu4 2882	. 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 200	1 ⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ (ℤ × ℕ)(((1^st ‘𝑥) gcd (2^nd ‘𝑥)) = 1 ∧ 𝐴 = ((1^st ‘𝑥) / (2^nd ‘𝑥))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 963 = wceq 1332 ∈ wcel 1481 ≠ wne 2309 ∀wral 2417 ∃wrex 2418 ∃!wreu 2419 Vcvv 2689 ⟨cop 3535 class class class wbr 3937 × cxp 4545 ‘cfv 5131 (class class class)co 5782 1^st c1st 6044 2^nd c2nd 6045 ℂcc 7642 ℝcr 7643 0cc0 7644 1c1 7645 · cmul 7649 < clt 7824 # cap 8367 / cdiv 8456 ℕcn 8744 ℕ₀cn0 9001 ℤcz 9078 ℚcq 9438 ∥ cdvds 11529 gcd cgcd 11671

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-coll 4051 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-iinf 4510 ax-cnex 7735 ax-resscn 7736 ax-1cn 7737 ax-1re 7738 ax-icn 7739 ax-addcl 7740 ax-addrcl 7741 ax-mulcl 7742 ax-mulrcl 7743 ax-addcom 7744 ax-mulcom 7745 ax-addass 7746 ax-mulass 7747 ax-distr 7748 ax-i2m1 7749 ax-0lt1 7750 ax-1rid 7751 ax-0id 7752 ax-rnegex 7753 ax-precex 7754 ax-cnre 7755 ax-pre-ltirr 7756 ax-pre-ltwlin 7757 ax-pre-lttrn 7758 ax-pre-apti 7759 ax-pre-ltadd 7760 ax-pre-mulgt0 7761 ax-pre-mulext 7762 ax-arch 7763 ax-caucvg 7764

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-nel 2405 df-ral 2422 df-rex 2423 df-reu 2424 df-rmo 2425 df-rab 2426 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-if 3480 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-iun 3823 df-br 3938 df-opab 3998 df-mpt 3999 df-tr 4035 df-id 4223 df-po 4226 df-iso 4227 df-iord 4296 df-on 4298 df-ilim 4299 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-f1 5136 df-fo 5137 df-f1o 5138 df-fv 5139 df-riota 5738 df-ov 5785 df-oprab 5786 df-mpo 5787 df-1st 6046 df-2nd 6047 df-recs 6210 df-frec 6296 df-sup 6879 df-pnf 7826 df-mnf 7827 df-xr 7828 df-ltxr 7829 df-le 7830 df-sub 7959 df-neg 7960 df-reap 8361 df-ap 8368 df-div 8457 df-inn 8745 df-2 8803 df-3 8804 df-4 8805 df-n0 9002 df-z 9079 df-uz 9351 df-q 9439 df-rp 9471 df-fz 9822 df-fzo 9951 df-fl 10074 df-mod 10127 df-seqfrec 10250 df-exp 10324 df-cj 10646 df-re 10647 df-im 10648 df-rsqrt 10802 df-abs 10803 df-dvds 11530 df-gcd 11672

This theorem is referenced by: qnumdencl 11901 qnumdenbi 11906

W3C validator