Step | Hyp | Ref
| Expression |
1 | | dfphi2 15479 |
. 2
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(#‘{𝑥 ∈
(0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
2 | | nnnn0 11299 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
3 | | znchr.y |
. . . . . . . . . 10
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
4 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘𝑌) =
(Base‘𝑌) |
5 | | eqid 2622 |
. . . . . . . . . 10
⊢
((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) |
6 | | eqid 2622 |
. . . . . . . . . 10
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) = if(𝑁 = 0, ℤ, (0..^𝑁)) |
7 | 3, 4, 5, 6 | znf1o 19900 |
. . . . . . . . 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 11053 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
10 | | ifnefalse 4098 |
. . . . . . . . 9
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
11 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ (0..^𝑁))) |
12 | | f1oeq1 6127 |
. . . . . . . . . . 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 6128 |
. . . . . . . . . 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 268 |
. . . . . . . . 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 222 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((ℤRHom‘𝑌)
↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌)) |
18 | | f1ofn 6138 |
. . . . . . 7
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌) → ((ℤRHom‘𝑌) ↾ (0..^𝑁)) Fn (0..^𝑁)) |
19 | | elpreima 6337 |
. . . . . . 7
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)) Fn (0..^𝑁) → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈))) |
21 | | fvres 6207 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0..^𝑁) → (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
22 | 21 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
23 | 22 | eleq1d 2686 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → ((((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈 ↔ ((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈)) |
24 | | elfzoelz 12470 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) |
25 | | znunit.u |
. . . . . . . . . 10
⊢ 𝑈 = (Unit‘𝑌) |
26 | | eqid 2622 |
. . . . . . . . . 10
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
27 | 3, 25, 26 | znunit 19912 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) |
28 | 2, 24, 27 | syl2an 494 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → (((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) |
29 | 23, 28 | bitrd 268 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → ((((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) |
30 | 29 | pm5.32da 673 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1))) |
31 | 20, 30 | bitrd 268 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1))) |
32 | 31 | abbi2dv 2742 |
. . . 4
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) = {𝑥 ∣ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1)}) |
33 | | df-rab 2921 |
. . . 4
⊢ {𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1} = {𝑥 ∣ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1)} |
34 | 32, 33 | syl6eqr 2674 |
. . 3
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) = {𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1}) |
35 | 34 | fveq2d 6195 |
. 2
⊢ (𝑁 ∈ ℕ →
(#‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (#‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
36 | | f1ocnv 6149 |
. . . . 5
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌) → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1-onto→(0..^𝑁)) |
37 | | f1of1 6136 |
. . . . 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 6680 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) ∈
V) |
40 | 4, 25 | unitss 18660 |
. . . . 5
⊢ 𝑈 ⊆ (Base‘𝑌) |
41 | 40 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑈 ⊆ (Base‘𝑌)) |
42 | | fvex 6201 |
. . . . . 6
⊢
(Unit‘𝑌)
∈ V |
43 | 25, 42 | eqeltri 2697 |
. . . . 5
⊢ 𝑈 ∈ V |
44 | 43 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑈 ∈ V) |
45 | | f1imaen2g 8017 |
. . . 4
⊢ (((◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁) ∧ (0..^𝑁) ∈ V) ∧ (𝑈 ⊆ (Base‘𝑌) ∧ 𝑈 ∈ V)) → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈) |
46 | 38, 39, 41, 44, 45 | syl22anc 1327 |
. . 3
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈) |
47 | | hasheni 13136 |
. . 3
⊢ ((◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈 → (#‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (#‘𝑈)) |
48 | 46, 47 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ →
(#‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (#‘𝑈)) |
49 | 1, 35, 48 | 3eqtr2rd 2663 |
1
⊢ (𝑁 ∈ ℕ →
(#‘𝑈) =
(ϕ‘𝑁)) |