Step | Hyp | Ref
| Expression |
1 | | phival 15310 |
. 2
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
2 | | fzfi 12633 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
3 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...𝑁) |
4 | | ssfi 8065 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...𝑁)) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin) |
5 | 2, 3, 4 | mp2an 704 |
. . . . . 6
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin |
6 | | hashcl 13009 |
. . . . . 6
⊢ ({𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin → (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈
ℕ0) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈
ℕ0 |
8 | 7 | nn0zi 11279 |
. . . 4
⊢
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ |
9 | 8 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ) |
10 | | 1z 11284 |
. . . . 5
⊢ 1 ∈
ℤ |
11 | | hashsng 13020 |
. . . . 5
⊢ (1 ∈
ℤ → (#‘{1}) = 1) |
12 | 10, 11 | ax-mp 5 |
. . . 4
⊢
(#‘{1}) = 1 |
13 | | ovex 6577 |
. . . . . . 7
⊢
(1...𝑁) ∈
V |
14 | 13 | rabex 4740 |
. . . . . 6
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ V |
15 | | eluzfz1 12219 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
16 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
17 | 15, 16 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
(1...𝑁)) |
18 | | nnz 11276 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
19 | | 1gcd 15092 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (1 gcd
𝑁) = 1) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 gcd
𝑁) = 1) |
21 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 gcd 𝑁) = (1 gcd 𝑁)) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑥 = 1 → ((𝑥 gcd 𝑁) = 1 ↔ (1 gcd 𝑁) = 1)) |
23 | 22 | elrab 3331 |
. . . . . . . 8
⊢ (1 ∈
{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ↔ (1 ∈ (1...𝑁) ∧ (1 gcd 𝑁) = 1)) |
24 | 17, 20, 23 | sylanbrc 695 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∈
{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
25 | 24 | snssd 4281 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {1}
⊆ {𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
26 | | ssdomg 7887 |
. . . . . 6
⊢ ({𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ V → ({1} ⊆ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} → {1} ≼ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
27 | 14, 25, 26 | mpsyl 66 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {1}
≼ {𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
28 | | snfi 7923 |
. . . . . 6
⊢ {1}
∈ Fin |
29 | | hashdom 13029 |
. . . . . 6
⊢ (({1}
∈ Fin ∧ {𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin) → ((#‘{1})
≤ (#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ↔ {1} ≼ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
30 | 28, 5, 29 | mp2an 704 |
. . . . 5
⊢
((#‘{1}) ≤ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ↔ {1} ≼ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
31 | 27, 30 | sylibr 223 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(#‘{1}) ≤ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
32 | 12, 31 | syl5eqbrr 4619 |
. . 3
⊢ (𝑁 ∈ ℕ → 1 ≤
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
33 | | ssdomg 7887 |
. . . . . 6
⊢
((1...𝑁) ∈ V
→ ({𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...𝑁) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁))) |
34 | 13, 3, 33 | mp2 9 |
. . . . 5
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁) |
35 | | hashdom 13029 |
. . . . . 6
⊢ (({𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin ∧ (1...𝑁) ∈ Fin) →
((#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ (#‘(1...𝑁)) ↔ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁))) |
36 | 5, 2, 35 | mp2an 704 |
. . . . 5
⊢
((#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ (#‘(1...𝑁)) ↔ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁)) |
37 | 34, 36 | mpbir 220 |
. . . 4
⊢
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ (#‘(1...𝑁)) |
38 | | nnnn0 11176 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
39 | | hashfz1 12996 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(#‘(1...𝑁)) = 𝑁) |
41 | 37, 40 | syl5breq 4620 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ 𝑁) |
42 | | elfz1 12202 |
. . . 4
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → ((#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ (1...𝑁) ↔ ((#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ ∧ 1 ≤
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∧ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ 𝑁))) |
43 | 10, 18, 42 | sylancr 694 |
. . 3
⊢ (𝑁 ∈ ℕ →
((#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ (1...𝑁) ↔ ((#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ ∧ 1 ≤
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∧ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ 𝑁))) |
44 | 9, 32, 41, 43 | mpbir3and 1238 |
. 2
⊢ (𝑁 ∈ ℕ →
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ (1...𝑁)) |
45 | 1, 44 | eqeltrd 2688 |
1
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
(1...𝑁)) |