| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfphi2 16812 | . 2
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(♯‘{𝑥 ∈
(0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) | 
| 2 |  | nnnn0 12535 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 3 |  | znchr.y | . . . . . . . . . 10
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) | 
| 4 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 5 |  | eqid 2736 | . . . . . . . . . 10
⊢
((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) | 
| 6 |  | eqid 2736 | . . . . . . . . . 10
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) = if(𝑁 = 0, ℤ, (0..^𝑁)) | 
| 7 | 3, 4, 5, 6 | znf1o 21571 | . . . . . . . . 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 12301 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 10 |  | ifnefalse 4536 | . . . . . . . . 9
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) | 
| 11 |  | reseq2 5991 | . . . . . . . . . . 11
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → ((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑌) ↾ (0..^𝑁))) | 
| 12 | 11 | f1oeq1d 6842 | . . . . . . . . . 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‘𝑌))) | 
| 13 |  | f1oeq2 6836 | . . . . . . . . . 10
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → (((ℤRHom‘𝑌) ↾ (0..^𝑁)):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌))) | 
| 14 | 12, 13 | bitrd 279 | . . . . . . . . 9
⊢ (if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁) → (((ℤRHom‘𝑌) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌))) | 
| 15 | 9, 10, 14 | 3syl 18 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(((ℤRHom‘𝑌)
↾ if(𝑁 = 0, ℤ,
(0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑌) ↔ ((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌))) | 
| 16 | 8, 15 | mpbid 232 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((ℤRHom‘𝑌)
↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌)) | 
| 17 |  | f1ofn 6848 | . . . . . . 7
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌) → ((ℤRHom‘𝑌) ↾ (0..^𝑁)) Fn (0..^𝑁)) | 
| 18 |  | elpreima 7077 | . . . . . . 7
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)) Fn (0..^𝑁) → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈))) | 
| 19 | 16, 17, 18 | 3syl 18 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈))) | 
| 20 |  | fvres 6924 | . . . . . . . . . 10
⊢ (𝑥 ∈ (0..^𝑁) → (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) | 
| 21 | 20 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) | 
| 22 | 21 | eleq1d 2825 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → ((((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈 ↔ ((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈)) | 
| 23 |  | elfzoelz 13700 | . . . . . . . . 9
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) | 
| 24 |  | znunit.u | . . . . . . . . . 10
⊢ 𝑈 = (Unit‘𝑌) | 
| 25 |  | eqid 2736 | . . . . . . . . . 10
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) | 
| 26 | 3, 24, 25 | znunit 21583 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) | 
| 27 | 2, 23, 26 | syl2an 596 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → (((ℤRHom‘𝑌)‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) | 
| 28 | 22, 27 | bitrd 279 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (0..^𝑁)) → ((((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈 ↔ (𝑥 gcd 𝑁) = 1)) | 
| 29 | 28 | pm5.32da 579 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑥 ∈ (0..^𝑁) ∧ (((ℤRHom‘𝑌) ↾ (0..^𝑁))‘𝑥) ∈ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1))) | 
| 30 | 19, 29 | bitrd 279 | . . . . 5
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ↔ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1))) | 
| 31 | 30 | eqabdv 2874 | . . . 4
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) = {𝑥 ∣ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1)}) | 
| 32 |  | df-rab 3436 | . . . 4
⊢ {𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1} = {𝑥 ∣ (𝑥 ∈ (0..^𝑁) ∧ (𝑥 gcd 𝑁) = 1)} | 
| 33 | 31, 32 | eqtr4di 2794 | . . 3
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) = {𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1}) | 
| 34 | 33 | fveq2d 6909 | . 2
⊢ (𝑁 ∈ ℕ →
(♯‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (♯‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) | 
| 35 |  | f1ocnv 6859 | . . . . 5
⊢
(((ℤRHom‘𝑌) ↾ (0..^𝑁)):(0..^𝑁)–1-1-onto→(Base‘𝑌) → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1-onto→(0..^𝑁)) | 
| 36 |  | f1of1 6846 | . . . . 5
⊢ (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1-onto→(0..^𝑁) → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁)) | 
| 37 | 16, 35, 36 | 3syl 18 | . . . 4
⊢ (𝑁 ∈ ℕ → ◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁)) | 
| 38 |  | ovexd 7467 | . . . 4
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) ∈
V) | 
| 39 | 4, 24 | unitss 20377 | . . . . 5
⊢ 𝑈 ⊆ (Base‘𝑌) | 
| 40 | 39 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℕ → 𝑈 ⊆ (Base‘𝑌)) | 
| 41 | 24 | fvexi 6919 | . . . . 5
⊢ 𝑈 ∈ V | 
| 42 | 41 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℕ → 𝑈 ∈ V) | 
| 43 |  | f1imaen2g 9056 | . . . 4
⊢ (((◡((ℤRHom‘𝑌) ↾ (0..^𝑁)):(Base‘𝑌)–1-1→(0..^𝑁) ∧ (0..^𝑁) ∈ V) ∧ (𝑈 ⊆ (Base‘𝑌) ∧ 𝑈 ∈ V)) → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈) | 
| 44 | 37, 38, 40, 42, 43 | syl22anc 838 | . . 3
⊢ (𝑁 ∈ ℕ → (◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈) | 
| 45 |  | hasheni 14388 | . . 3
⊢ ((◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈) ≈ 𝑈 → (♯‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (♯‘𝑈)) | 
| 46 | 44, 45 | syl 17 | . 2
⊢ (𝑁 ∈ ℕ →
(♯‘(◡((ℤRHom‘𝑌) ↾ (0..^𝑁)) “ 𝑈)) = (♯‘𝑈)) | 
| 47 | 1, 34, 46 | 3eqtr2rd 2783 | 1
⊢ (𝑁 ∈ ℕ →
(♯‘𝑈) =
(ϕ‘𝑁)) |