Step | Hyp | Ref
| Expression |
1 | | phival 15472 |
. 2
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
2 | | fzfi 12771 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
3 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...𝑁) |
4 | | ssfi 8180 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...𝑁)) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin) |
5 | 2, 3, 4 | mp2an 708 |
. . . . . 6
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin |
6 | | hashcl 13147 |
. . . . . 6
⊢ ({𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin → (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈
ℕ0) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈
ℕ0 |
8 | 7 | nn0zi 11402 |
. . . 4
⊢
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ |
9 | 8 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ) |
10 | | 1z 11407 |
. . . . 5
⊢ 1 ∈
ℤ |
11 | | hashsng 13159 |
. . . . 5
⊢ (1 ∈
ℤ → (#‘{1}) = 1) |
12 | 10, 11 | ax-mp 5 |
. . . 4
⊢
(#‘{1}) = 1 |
13 | | ovex 6678 |
. . . . . . 7
⊢
(1...𝑁) ∈
V |
14 | 13 | rabex 4813 |
. . . . . 6
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ V |
15 | | eluzfz1 12348 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
16 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
17 | 15, 16 | eleq2s 2719 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
(1...𝑁)) |
18 | | nnz 11399 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
19 | | 1gcd 15254 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (1 gcd
𝑁) = 1) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 gcd
𝑁) = 1) |
21 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 gcd 𝑁) = (1 gcd 𝑁)) |
22 | 21 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑥 = 1 → ((𝑥 gcd 𝑁) = 1 ↔ (1 gcd 𝑁) = 1)) |
23 | 22 | elrab 3363 |
. . . . . . . 8
⊢ (1 ∈
{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ↔ (1 ∈ (1...𝑁) ∧ (1 gcd 𝑁) = 1)) |
24 | 17, 20, 23 | sylanbrc 698 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∈
{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
25 | 24 | snssd 4340 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {1}
⊆ {𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
26 | | ssdomg 8001 |
. . . . . 6
⊢ ({𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ V → ({1} ⊆ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} → {1} ≼ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
27 | 14, 25, 26 | mpsyl 68 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {1}
≼ {𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
28 | | snfi 8038 |
. . . . . 6
⊢ {1}
∈ Fin |
29 | | hashdom 13168 |
. . . . . 6
⊢ (({1}
∈ Fin ∧ {𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin) → ((#‘{1})
≤ (#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ↔ {1} ≼ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
30 | 28, 5, 29 | mp2an 708 |
. . . . 5
⊢
((#‘{1}) ≤ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ↔ {1} ≼ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
31 | 27, 30 | sylibr 224 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(#‘{1}) ≤ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
32 | 12, 31 | syl5eqbrr 4689 |
. . 3
⊢ (𝑁 ∈ ℕ → 1 ≤
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
33 | | ssdomg 8001 |
. . . . . 6
⊢
((1...𝑁) ∈ V
→ ({𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...𝑁) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁))) |
34 | 13, 3, 33 | mp2 9 |
. . . . 5
⊢ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁) |
35 | | hashdom 13168 |
. . . . . 6
⊢ (({𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin ∧ (1...𝑁) ∈ Fin) →
((#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ (#‘(1...𝑁)) ↔ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁))) |
36 | 5, 2, 35 | mp2an 708 |
. . . . 5
⊢
((#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ (#‘(1...𝑁)) ↔ {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ≼ (1...𝑁)) |
37 | 34, 36 | mpbir 221 |
. . . 4
⊢
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ (#‘(1...𝑁)) |
38 | | nnnn0 11299 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
39 | | hashfz1 13134 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(#‘(1...𝑁)) = 𝑁) |
41 | 37, 40 | syl5breq 4690 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ 𝑁) |
42 | | elfz1 12331 |
. . . 4
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → ((#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ (1...𝑁) ↔ ((#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ ∧ 1 ≤
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∧ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ 𝑁))) |
43 | 10, 18, 42 | sylancr 695 |
. . 3
⊢ (𝑁 ∈ ℕ →
((#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ (1...𝑁) ↔ ((#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ ℤ ∧ 1 ≤
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∧ (#‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ≤ 𝑁))) |
44 | 9, 32, 41, 43 | mpbir3and 1245 |
. 2
⊢ (𝑁 ∈ ℕ →
(#‘{𝑥 ∈
(1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}) ∈ (1...𝑁)) |
45 | 1, 44 | eqeltrd 2701 |
1
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
(1...𝑁)) |