Step | Hyp | Ref
| Expression |
1 | | nnz 9187 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
2 | | gcddvds 11851 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ∧ (𝑧 gcd 𝑛) ∥ 𝑛)) |
3 | 2 | simpld 111 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∥ 𝑧) |
4 | 1, 3 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∥ 𝑧) |
5 | | gcdcl 11854 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 gcd 𝑛) ∈
ℕ0) |
6 | 1, 5 | sylan2 284 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈
ℕ0) |
7 | 6 | nn0zd 9285 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℤ) |
8 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈
ℤ) |
9 | 1 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℤ) |
10 | | nnne0 8862 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
11 | 10 | neneqd 2348 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ¬
𝑛 = 0) |
12 | 11 | intnand 917 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ¬
(𝑧 = 0 ∧ 𝑛 = 0)) |
13 | 12 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ¬
(𝑧 = 0 ∧ 𝑛 = 0)) |
14 | | gcdn0cl 11850 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬
(𝑧 = 0 ∧ 𝑛 = 0)) → (𝑧 gcd 𝑛) ∈ ℕ) |
15 | 8, 9, 13, 14 | syl21anc 1219 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℕ) |
16 | 15 | nnne0d 8879 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ≠ 0) |
17 | | dvdsval2 11690 |
. . . . . . . . . 10
⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑧 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑧 ↔ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ)) |
18 | 7, 16, 8, 17 | syl3anc 1220 |
. . . . . . . . 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 11690 |
. . . . . . . . . . . 12
⊢ (((𝑧 gcd 𝑛) ∈ ℤ ∧ (𝑧 gcd 𝑛) ≠ 0 ∧ 𝑛 ∈ ℤ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)) |
24 | 7, 16, 9, 23 | syl3anc 1220 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) ∥ 𝑛 ↔ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ)) |
25 | 22, 24 | mpbid 146 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) |
26 | | nnre 8841 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
27 | 26 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℝ) |
28 | 6 | nn0red 9145 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℝ) |
29 | | nngt0 8859 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) |
30 | 29 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 <
𝑛) |
31 | 15 | nngt0d 8878 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 <
(𝑧 gcd 𝑛)) |
32 | 27, 28, 30, 31 | divgt0d 8807 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 0 <
(𝑛 / (𝑧 gcd 𝑛))) |
33 | 25, 32 | jca 304 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛)))) |
34 | 33 | 3adant3 1002 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛)))) |
35 | | elnnz 9178 |
. . . . . . . 8
⊢ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ ↔ ((𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ 0 < (𝑛 / (𝑧 gcd 𝑛)))) |
36 | 34, 35 | sylibr 133 |
. . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ) |
37 | | opelxpi 4619 |
. . . . . . 7
⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℕ) → 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉 ∈ (ℤ ×
ℕ)) |
38 | 20, 36, 37 | syl2anc 409 |
. . . . . 6
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉 ∈ (ℤ ×
ℕ)) |
39 | | fveq2 5469 |
. . . . . . . . . 10
⊢ (𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉 → (1st ‘𝑥) = (1st
‘〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉)) |
40 | | simp1 982 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑧 ∈ ℤ) |
41 | 15 | 3adant3 1002 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 gcd 𝑛) ∈ ℕ) |
42 | | znq 9534 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ) |
43 | 40, 41, 42 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ) |
44 | 9 | 3adant3 1002 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝑛 ∈ ℤ) |
45 | | znq 9534 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ (𝑧 gcd 𝑛) ∈ ℕ) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) |
46 | 44, 41, 45 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) |
47 | | op1stg 6099 |
. . . . . . . . . . 11
⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (1st
‘〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) = (𝑧 / (𝑧 gcd 𝑛))) |
48 | 43, 46, 47 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (1st ‘〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) = (𝑧 / (𝑧 gcd 𝑛))) |
49 | 39, 48 | sylan9eqr 2212 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → (1st ‘𝑥) = (𝑧 / (𝑧 gcd 𝑛))) |
50 | | fveq2 5469 |
. . . . . . . . . 10
⊢ (𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉 → (2nd ‘𝑥) = (2nd
‘〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉)) |
51 | | op2ndg 6100 |
. . . . . . . . . . 11
⊢ (((𝑧 / (𝑧 gcd 𝑛)) ∈ ℚ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℚ) → (2nd
‘〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) = (𝑛 / (𝑧 gcd 𝑛))) |
52 | 43, 46, 51 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (2nd ‘〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) = (𝑛 / (𝑧 gcd 𝑛))) |
53 | 50, 52 | sylan9eqr 2212 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → (2nd ‘𝑥) = (𝑛 / (𝑧 gcd 𝑛))) |
54 | 49, 53 | oveq12d 5843 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → ((1st
‘𝑥) gcd
(2nd ‘𝑥))
= ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) |
55 | 54 | eqeq1d 2166 |
. . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → (((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ↔ ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1)) |
56 | 49, 53 | oveq12d 5843 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → ((1st
‘𝑥) / (2nd
‘𝑥)) = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))) |
57 | 56 | eqeq2d 2169 |
. . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → (𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥)) ↔ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))) |
58 | 55, 57 | anbi12d 465 |
. . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) ∧ 𝑥 = 〈(𝑧 / (𝑧 gcd 𝑛)), (𝑛 / (𝑧 gcd 𝑛))〉) → ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ↔ (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))))) |
59 | 19, 25 | gcdcld 11856 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈
ℕ0) |
60 | 59 | nn0cnd 9146 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) ∈ ℂ) |
61 | | 1cnd 7895 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
62 | 6 | nn0cnd 9146 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) ∈ ℂ) |
63 | 15 | nnap0d 8880 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑧 gcd 𝑛) # 0) |
64 | 62 | mulid1d 7896 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · 1) = (𝑧 gcd 𝑛)) |
65 | | zcn 9173 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℂ) |
66 | 65 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑧 ∈
ℂ) |
67 | 66, 62, 63 | divcanap2d 8666 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) = 𝑧) |
68 | | nncn 8842 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
69 | 68 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℂ) |
70 | 69, 62, 63 | divcanap2d 8666 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛))) = 𝑛) |
71 | 67, 70 | oveq12d 5843 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = (𝑧 gcd 𝑛)) |
72 | | mulgcd 11904 |
. . . . . . . . . . 11
⊢ (((𝑧 gcd 𝑛) ∈ ℕ0 ∧ (𝑧 / (𝑧 gcd 𝑛)) ∈ ℤ ∧ (𝑛 / (𝑧 gcd 𝑛)) ∈ ℤ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))) |
73 | 6, 19, 25, 72 | syl3anc 1220 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑧 gcd 𝑛) · (𝑧 / (𝑧 gcd 𝑛))) gcd ((𝑧 gcd 𝑛) · (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))))) |
74 | 64, 71, 73 | 3eqtr2rd 2197 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 gcd 𝑛) · ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛)))) = ((𝑧 gcd 𝑛) · 1)) |
75 | 60, 61, 62, 63, 74 | mulcanapad 8538 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1) |
76 | 75 | 3adant3 1002 |
. . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1) |
77 | | nnap0 8863 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 # 0) |
78 | 77 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → 𝑛 # 0) |
79 | 66, 69, 62, 78, 63 | divcanap7d 8693 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) = (𝑧 / 𝑛)) |
80 | 79 | eqeq2d 2169 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))) ↔ 𝐴 = (𝑧 / 𝑛))) |
81 | 80 | biimp3ar 1328 |
. . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛)))) |
82 | 76, 81 | jca 304 |
. . . . . 6
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (((𝑧 / (𝑧 gcd 𝑛)) gcd (𝑛 / (𝑧 gcd 𝑛))) = 1 ∧ 𝐴 = ((𝑧 / (𝑧 gcd 𝑛)) / (𝑛 / (𝑧 gcd 𝑛))))) |
83 | 38, 58, 82 | rspcedvd 2822 |
. . . . 5
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → ∃𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥)))) |
84 | | elxp6 6118 |
. . . . . . 7
⊢ (𝑥 ∈ (ℤ ×
ℕ) ↔ (𝑥 =
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st ‘𝑥) ∈ ℤ ∧
(2nd ‘𝑥)
∈ ℕ))) |
85 | | elxp6 6118 |
. . . . . . 7
⊢ (𝑦 ∈ (ℤ ×
ℕ) ↔ (𝑦 =
〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st ‘𝑦) ∈ ℤ ∧
(2nd ‘𝑦)
∈ ℕ))) |
86 | | simprl 521 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) → (1st
‘𝑥) ∈
ℤ) |
87 | 86 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → (1st
‘𝑥) ∈
ℤ) |
88 | | simprr 522 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) → (2nd
‘𝑥) ∈
ℕ) |
89 | 88 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → (2nd
‘𝑥) ∈
ℕ) |
90 | | simprll 527 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → ((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1) |
91 | | simprl 521 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 ∧
((1st ‘𝑦)
∈ ℤ ∧ (2nd ‘𝑦) ∈ ℕ)) → (1st
‘𝑦) ∈
ℤ) |
92 | 91 | ad2antlr 481 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → (1st
‘𝑦) ∈
ℤ) |
93 | | simprr 522 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 ∧
((1st ‘𝑦)
∈ ℤ ∧ (2nd ‘𝑦) ∈ ℕ)) → (2nd
‘𝑦) ∈
ℕ) |
94 | 93 | ad2antlr 481 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → (2nd
‘𝑦) ∈
ℕ) |
95 | | simprrl 529 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → ((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1) |
96 | | simprlr 528 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) |
97 | | simprrr 530 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))) |
98 | 96, 97 | eqtr3d 2192 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → ((1st
‘𝑥) / (2nd
‘𝑥)) =
((1st ‘𝑦)
/ (2nd ‘𝑦))) |
99 | | qredeq 11977 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) ∈ ℤ ∧ (2nd
‘𝑥) ∈ ℕ
∧ ((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1) ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ ∧ ((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1) ∧ ((1st ‘𝑥) / (2nd ‘𝑥)) = ((1st ‘𝑦) / (2nd ‘𝑦))) → ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥) =
(2nd ‘𝑦))) |
100 | 87, 89, 90, 92, 94, 95, 98, 99 | syl331anc 1245 |
. . . . . . . . . 10
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥) =
(2nd ‘𝑦))) |
101 | | vex 2715 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
102 | | 1stexg 6116 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ V → (1st
‘𝑥) ∈
V) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1st ‘𝑥) ∈ V |
104 | | 2ndexg 6117 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ V → (2nd
‘𝑥) ∈
V) |
105 | 101, 104 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑥) ∈ V |
106 | 103, 105 | opth 4198 |
. . . . . . . . . 10
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ↔ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥) =
(2nd ‘𝑦))) |
107 | 100, 106 | sylibr 133 |
. . . . . . . . 9
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) →
〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
108 | | simplll 523 |
. . . . . . . . 9
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
109 | | simplrl 525 |
. . . . . . . . 9
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
110 | 107, 108,
109 | 3eqtr4d 2200 |
. . . . . . . 8
⊢ ((((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) ∧ ((((1st
‘𝑥) gcd
(2nd ‘𝑥))
= 1 ∧ 𝐴 =
((1st ‘𝑥)
/ (2nd ‘𝑥))) ∧ (((1st ‘𝑦) gcd (2nd
‘𝑦)) = 1 ∧ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦))))) → 𝑥 = 𝑦) |
111 | 110 | ex 114 |
. . . . . . 7
⊢ (((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℤ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∧ ((1st
‘𝑦) ∈ ℤ
∧ (2nd ‘𝑦) ∈ ℕ))) →
(((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦)) |
112 | 84, 85, 111 | syl2anb 289 |
. . . . . 6
⊢ ((𝑥 ∈ (ℤ ×
ℕ) ∧ 𝑦 ∈
(ℤ × ℕ)) → (((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦)) |
113 | 112 | rgen2a 2511 |
. . . . 5
⊢
∀𝑥 ∈
(ℤ × ℕ)∀𝑦 ∈ (ℤ ×
ℕ)(((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦) |
114 | 83, 113 | jctir 311 |
. . . 4
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 𝐴 = (𝑧 / 𝑛)) → (∃𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ ×
ℕ)∀𝑦 ∈
(ℤ × ℕ)(((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦))) |
115 | 114 | 3expia 1187 |
. . 3
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝐴 = (𝑧 / 𝑛) → (∃𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ ×
ℕ)∀𝑦 ∈
(ℤ × ℕ)(((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦)))) |
116 | 115 | rexlimivv 2580 |
. 2
⊢
(∃𝑧 ∈
ℤ ∃𝑛 ∈
ℕ 𝐴 = (𝑧 / 𝑛) → (∃𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ ×
ℕ)∀𝑦 ∈
(ℤ × ℕ)(((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦))) |
117 | | elq 9532 |
. 2
⊢ (𝐴 ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑛 ∈ ℕ
𝐴 = (𝑧 / 𝑛)) |
118 | | fveq2 5469 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (1st ‘𝑥) = (1st ‘𝑦)) |
119 | | fveq2 5469 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (2nd ‘𝑥) = (2nd ‘𝑦)) |
120 | 118, 119 | oveq12d 5843 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((1st ‘𝑥) gcd (2nd
‘𝑥)) =
((1st ‘𝑦)
gcd (2nd ‘𝑦))) |
121 | 120 | eqeq1d 2166 |
. . . 4
⊢ (𝑥 = 𝑦 → (((1st ‘𝑥) gcd (2nd
‘𝑥)) = 1 ↔
((1st ‘𝑦)
gcd (2nd ‘𝑦)) = 1)) |
122 | 118, 119 | oveq12d 5843 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((1st ‘𝑥) / (2nd ‘𝑥)) = ((1st
‘𝑦) / (2nd
‘𝑦))) |
123 | 122 | eqeq2d 2169 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥)) ↔ 𝐴 = ((1st ‘𝑦) / (2nd ‘𝑦)))) |
124 | 121, 123 | anbi12d 465 |
. . 3
⊢ (𝑥 = 𝑦 → ((((1st ‘𝑥) gcd (2nd
‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ↔ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦))))) |
125 | 124 | reu4 2906 |
. 2
⊢
(∃!𝑥 ∈
(ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ↔ (∃𝑥 ∈ (ℤ ×
ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ ∀𝑥 ∈ (ℤ ×
ℕ)∀𝑦 ∈
(ℤ × ℕ)(((((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))) ∧ (((1st
‘𝑦) gcd
(2nd ‘𝑦))
= 1 ∧ 𝐴 =
((1st ‘𝑦)
/ (2nd ‘𝑦)))) → 𝑥 = 𝑦))) |
126 | 116, 117,
125 | 3imtr4i 200 |
1
⊢ (𝐴 ∈ ℚ →
∃!𝑥 ∈ (ℤ
× ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥)))) |