Step | Hyp | Ref
| Expression |
1 | | dfphi2 16105 |
. 2
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(♯‘{𝑥 ∈
(0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
2 | | nnnn0 11898 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
3 | | znchr.y |
. . . . . . . . . 10
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
4 | | eqid 2821 |
. . . . . . . . . 10
⊢
(Base‘𝑌) =
(Base‘𝑌) |
5 | | eqid 2821 |
. . . . . . . . . 10
⊢
((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) |
6 | | eqid 2821 |
. . . . . . . . . 10
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) = if(𝑁 = 0, ℤ, (0..^𝑁)) |
7 | 3, 4, 5, 6 | znf1o 20692 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌)) |
8 | 2, 7 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((ℤRHom‘𝑌)
↾ if(𝑁 = 0, ℤ,
(0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌)) |
9 | | nnne0 11665 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
10 | | ifnefalse 4478 |
. . . . . . . . 9
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
11 | | reseq2 5842 |
. . . . . . . . . . 11
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ (0..^𝑁))) |
12 | | f1oeq1 6598 |
. . . . . . . . . . 11
⊢
(((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ (0..^𝑁)) → (((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → (((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌))) |
14 | | f1oeq2 6599 |
. . . . . . . . . 10
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → (((ℤRHom‘𝑌) ↾ (0..^𝑁)):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌))) |
15 | 13, 14 | bitrd 281 |
. . . . . . . . 9
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → (((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌))) |
16 | 9, 10, 15 | 3syl 18 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(((ℤRHom‘𝑌)
↾ if(𝑁 = 0, ℤ,
(0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌))) |
17 | 8, 16 | mpbid 234 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((ℤRHom‘𝑌)
↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌)) |
18 | | f1ofn 6610 |
. . . . . . 7
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌) → ((ℤRHom‘𝑌) ↾ (0..^𝑁)) Fn (0..^𝑁)) |
19 | | elpreima 6822 |
. . . . . . 7
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)) Fn (0..^𝑁) → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈))) |
21 | | fvres 6683 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0..^𝑁) → (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
22 | 21 | adantl 484 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
23 | 22 | eleq1d 2897 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → ((((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈 ↔ ((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈)) |
24 | | elfzoelz 13032 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) |
25 | | znunit.u |
. . . . . . . . . 10
⊢ 𝑈 = (Unit‘𝑌) |
26 | | eqid 2821 |
. . . . . . . . . 10
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
27 | 3, 25, 26 | znunit 20704 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) |
28 | 2, 24, 27 | syl2an 597 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → (((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) |
29 | 23, 28 | bitrd 281 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → ((((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) |
30 | 29 | pm5.32da 581 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1))) |
31 | 20, 30 | bitrd 281 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1))) |
32 | 31 | abbi2dv 2950 |
. . . 4
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) = {𝑥 ∣ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1)}) |
33 | | df-rab 3147 |
. . . 4
⊢ {𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1} = {𝑥 ∣ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1)} |
34 | 32, 33 | syl6eqr 2874 |
. . 3
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) = {𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
35 | 34 | fveq2d 6668 |
. 2
⊢ (𝑁 ∈ ℕ →
(♯‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (♯‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
36 | | f1ocnv 6621 |
. . . . 5
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌) → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1-onto→(0..^𝑁)) |
37 | | f1of1 6608 |
. . . . 5
⊢ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1-onto→(0..^𝑁) → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁)) |
38 | 17, 36, 37 | 3syl 18 |
. . . 4
⊢ (𝑁 ∈ ℕ → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁)) |
39 | | ovexd 7185 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) ∈
V) |
40 | 4, 25 | unitss 19404 |
. . . . 5
⊢ 𝑈 ⊆ (Base‘𝑌) |
41 | 40 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑈 ⊆ (Base‘𝑌)) |
42 | 25 | fvexi 6678 |
. . . . 5
⊢ 𝑈 ∈ V |
43 | 42 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑈 ∈ V) |
44 | | f1imaen2g 8564 |
. . . 4
⊢ (((◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁) ∧ (0..^𝑁) ∈ V) ∧ (𝑈 ⊆ (Base‘𝑌) ∧ 𝑈 ∈ V)) → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈) |
45 | 38, 39, 41, 43, 44 | syl22anc 836 |
. . 3
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈) |
46 | | hasheni 13702 |
. . 3
⊢ ((◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈 → (♯‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (♯‘𝑈)) |
47 | 45, 46 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ →
(♯‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (♯‘𝑈)) |
48 | 1, 35, 47 | 3eqtr2rd 2863 |
1
⊢ (𝑁 ∈ ℕ →
(♯‘𝑈) =
(ϕ‘𝑁)) |