| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | neg1cn 12381 | . . . 4
⊢ -1 ∈
ℂ | 
| 2 |  | 2rp 13040 | . . . . . 6
⊢ 2 ∈
ℝ+ | 
| 3 |  | nnrp 13047 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) | 
| 4 |  | rpdivcl 13061 | . . . . . 6
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (2 /
𝑁) ∈
ℝ+) | 
| 5 | 2, 3, 4 | sylancr 587 | . . . . 5
⊢ (𝑁 ∈ ℕ → (2 /
𝑁) ∈
ℝ+) | 
| 6 | 5 | rpcnd 13080 | . . . 4
⊢ (𝑁 ∈ ℕ → (2 /
𝑁) ∈
ℂ) | 
| 7 |  | cxpcl 26717 | . . . 4
⊢ ((-1
∈ ℂ ∧ (2 / 𝑁) ∈ ℂ) →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) | 
| 8 | 1, 6, 7 | sylancr 587 | . . 3
⊢ (𝑁 ∈ ℕ →
(-1↑𝑐(2 / 𝑁)) ∈ ℂ) | 
| 9 | 1 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℕ → -1 ∈
ℂ) | 
| 10 |  | neg1ne0 12383 | . . . . 5
⊢ -1 ≠
0 | 
| 11 | 10 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℕ → -1 ≠
0) | 
| 12 | 9, 11, 6 | cxpne0d 26756 | . . 3
⊢ (𝑁 ∈ ℕ →
(-1↑𝑐(2 / 𝑁)) ≠ 0) | 
| 13 |  | eldifsn 4785 | . . 3
⊢
((-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}) ↔
((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧
(-1↑𝑐(2 / 𝑁)) ≠ 0)) | 
| 14 | 8, 12, 13 | sylanbrc 583 | . 2
⊢ (𝑁 ∈ ℕ →
(-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖
{0})) | 
| 15 | 1 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ -1 ∈ ℂ) | 
| 16 | 10 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ -1 ≠ 0) | 
| 17 |  | nn0cn 12538 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℂ) | 
| 18 |  | mulcl 11240 | . . . . . . . . . 10
⊢ (((2 /
𝑁) ∈ ℂ ∧
𝑥 ∈ ℂ) →
((2 / 𝑁) · 𝑥) ∈
ℂ) | 
| 19 | 6, 17, 18 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((2 / 𝑁) ·
𝑥) ∈
ℂ) | 
| 20 | 15, 16, 19 | cxpefd 26755 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (-1↑𝑐((2 / 𝑁) · 𝑥)) = (exp‘(((2 / 𝑁) · 𝑥) · (log‘-1)))) | 
| 21 | 20 | eqeq1d 2738 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((-1↑𝑐((2 / 𝑁) · 𝑥)) = 1 ↔ (exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))) =
1)) | 
| 22 |  | logcl 26611 | . . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0) → (log‘-1) ∈
ℂ) | 
| 23 | 1, 10, 22 | mp2an 692 | . . . . . . . . 9
⊢
(log‘-1) ∈ ℂ | 
| 24 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((((2 /
𝑁) · 𝑥) ∈ ℂ ∧
(log‘-1) ∈ ℂ) → (((2 / 𝑁) · 𝑥) · (log‘-1)) ∈
ℂ) | 
| 25 | 19, 23, 24 | sylancl 586 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (((2 / 𝑁) ·
𝑥) · (log‘-1))
∈ ℂ) | 
| 26 |  | efeq1 26571 | . . . . . . . 8
⊢ ((((2 /
𝑁) · 𝑥) · (log‘-1))
∈ ℂ → ((exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))) = 1 ↔ ((((2
/ 𝑁) · 𝑥) · (log‘-1)) / (i
· (2 · π))) ∈ ℤ)) | 
| 27 | 25, 26 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((exp‘(((2 / 𝑁) · 𝑥) · (log‘-1))) = 1 ↔ ((((2
/ 𝑁) · 𝑥) · (log‘-1)) / (i
· (2 · π))) ∈ ℤ)) | 
| 28 |  | 2cn 12342 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 29 | 28 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 2 ∈ ℂ) | 
| 30 |  | nncn 12275 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 𝑁 ∈
ℂ) | 
| 32 | 17 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℂ) | 
| 33 |  | nnne0 12301 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 𝑁 ≠
0) | 
| 35 | 29, 31, 32, 34 | div13d 12068 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((2 / 𝑁) ·
𝑥) = ((𝑥 / 𝑁) · 2)) | 
| 36 |  | logm1 26632 | . . . . . . . . . . . . 13
⊢
(log‘-1) = (i · π) | 
| 37 | 36 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (log‘-1) = (i · π)) | 
| 38 | 35, 37 | oveq12d 7450 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (((2 / 𝑁) ·
𝑥) · (log‘-1))
= (((𝑥 / 𝑁) · 2) · (i ·
π))) | 
| 39 | 32, 31, 34 | divcld 12044 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (𝑥 / 𝑁) ∈
ℂ) | 
| 40 |  | ax-icn 11215 | . . . . . . . . . . . . . 14
⊢ i ∈
ℂ | 
| 41 |  | picn 26502 | . . . . . . . . . . . . . 14
⊢ π
∈ ℂ | 
| 42 | 40, 41 | mulcli 11269 | . . . . . . . . . . . . 13
⊢ (i
· π) ∈ ℂ | 
| 43 | 42 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (i · π) ∈ ℂ) | 
| 44 | 39, 29, 43 | mulassd 11285 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (((𝑥 / 𝑁) · 2) · (i
· π)) = ((𝑥 /
𝑁) · (2 · (i
· π)))) | 
| 45 | 40 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ i ∈ ℂ) | 
| 46 | 41 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ π ∈ ℂ) | 
| 47 | 29, 45, 46 | mul12d 11471 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (2 · (i · π)) = (i · (2 ·
π))) | 
| 48 | 47 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((𝑥 / 𝑁) · (2 · (i
· π))) = ((𝑥 /
𝑁) · (i · (2
· π)))) | 
| 49 | 38, 44, 48 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (((2 / 𝑁) ·
𝑥) · (log‘-1))
= ((𝑥 / 𝑁) · (i · (2 ·
π)))) | 
| 50 | 49 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((((2 / 𝑁) ·
𝑥) · (log‘-1))
/ (i · (2 · π))) = (((𝑥 / 𝑁) · (i · (2 · π))) /
(i · (2 · π)))) | 
| 51 | 28, 41 | mulcli 11269 | . . . . . . . . . . . 12
⊢ (2
· π) ∈ ℂ | 
| 52 | 40, 51 | mulcli 11269 | . . . . . . . . . . 11
⊢ (i
· (2 · π)) ∈ ℂ | 
| 53 | 52 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (i · (2 · π)) ∈ ℂ) | 
| 54 |  | ine0 11699 | . . . . . . . . . . . 12
⊢ i ≠
0 | 
| 55 |  | 2ne0 12371 | . . . . . . . . . . . . 13
⊢ 2 ≠
0 | 
| 56 |  | pire 26501 | . . . . . . . . . . . . . 14
⊢ π
∈ ℝ | 
| 57 |  | pipos 26503 | . . . . . . . . . . . . . 14
⊢ 0 <
π | 
| 58 | 56, 57 | gt0ne0ii 11800 | . . . . . . . . . . . . 13
⊢ π ≠
0 | 
| 59 | 28, 41, 55, 58 | mulne0i 11907 | . . . . . . . . . . . 12
⊢ (2
· π) ≠ 0 | 
| 60 | 40, 51, 54, 59 | mulne0i 11907 | . . . . . . . . . . 11
⊢ (i
· (2 · π)) ≠ 0 | 
| 61 | 60 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (i · (2 · π)) ≠ 0) | 
| 62 | 39, 53, 61 | divcan4d 12050 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (((𝑥 / 𝑁) · (i · (2
· π))) / (i · (2 · π))) = (𝑥 / 𝑁)) | 
| 63 | 50, 62 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((((2 / 𝑁) ·
𝑥) · (log‘-1))
/ (i · (2 · π))) = (𝑥 / 𝑁)) | 
| 64 | 63 | eleq1d 2825 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (((((2 / 𝑁) ·
𝑥) · (log‘-1))
/ (i · (2 · π))) ∈ ℤ ↔ (𝑥 / 𝑁) ∈ ℤ)) | 
| 65 | 21, 27, 64 | 3bitrd 305 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((-1↑𝑐((2 / 𝑁) · 𝑥)) = 1 ↔ (𝑥 / 𝑁) ∈ ℤ)) | 
| 66 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (2 / 𝑁) ∈
ℂ) | 
| 67 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) | 
| 68 | 15, 66, 67 | cxpmul2d 26752 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (-1↑𝑐((2 / 𝑁) · 𝑥)) = ((-1↑𝑐(2 / 𝑁))↑𝑥)) | 
| 69 |  | cnfldexp 21418 | . . . . . . . . 9
⊢
(((-1↑𝑐(2 / 𝑁)) ∈ ℂ ∧ 𝑥 ∈ ℕ0) → (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2
/ 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑𝑥)) | 
| 70 | 8, 69 | sylan 580 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2
/ 𝑁))) = ((-1↑𝑐(2 / 𝑁))↑𝑥)) | 
| 71 |  | cnring 21404 | . . . . . . . . . 10
⊢
ℂfld ∈ Ring | 
| 72 |  | cnfldbas 21369 | . . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) | 
| 73 |  | cnfld0 21406 | . . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) | 
| 74 |  | cndrng 21412 | . . . . . . . . . . . 12
⊢
ℂfld ∈ DivRing | 
| 75 | 72, 73, 74 | drngui 20736 | . . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) | 
| 76 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) | 
| 77 | 75, 76 | unitsubm 20387 | . . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) | 
| 78 | 71, 77 | mp1i 13 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) | 
| 79 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖
{0})) | 
| 80 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) | 
| 81 |  | proot1ex.g | . . . . . . . . . 10
⊢ 𝐺 =
((mulGrp‘ℂfld) ↾s (ℂ ∖
{0})) | 
| 82 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.g‘𝐺) = (.g‘𝐺) | 
| 83 | 80, 81, 82 | submmulg 19137 | . . . . . . . . 9
⊢
(((ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld)) ∧ 𝑥 ∈ ℕ0 ∧
(-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0})) →
(𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2
/ 𝑁))) = (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁)))) | 
| 84 | 78, 67, 79, 83 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (𝑥(.g‘(mulGrp‘ℂfld))(-1↑𝑐(2
/ 𝑁))) = (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁)))) | 
| 85 | 68, 70, 84 | 3eqtr2rd 2783 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) =
(-1↑𝑐((2 / 𝑁) · 𝑥))) | 
| 86 | 85 | eqeq1d 2738 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ ((𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1 ↔
(-1↑𝑐((2 / 𝑁) · 𝑥)) = 1)) | 
| 87 |  | nnz 12636 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 88 | 87 | adantr 480 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 𝑁 ∈
ℤ) | 
| 89 |  | nn0z 12640 | . . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℤ) | 
| 90 | 89 | adantl 481 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℤ) | 
| 91 |  | dvdsval2 16294 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝑥 ∈ ℤ) → (𝑁 ∥ 𝑥 ↔ (𝑥 / 𝑁) ∈ ℤ)) | 
| 92 | 88, 34, 90, 91 | syl3anc 1372 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (𝑁 ∥ 𝑥 ↔ (𝑥 / 𝑁) ∈ ℤ)) | 
| 93 | 65, 86, 92 | 3bitr4rd 312 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0)
→ (𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1)) | 
| 94 | 93 | ralrimiva 3145 | . . . 4
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
ℕ0 (𝑁
∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2
/ 𝑁))) =
1)) | 
| 95 | 75, 81 | unitgrp 20384 | . . . . . 6
⊢
(ℂfld ∈ Ring → 𝐺 ∈ Grp) | 
| 96 | 71, 95 | mp1i 13 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Grp) | 
| 97 |  | nnnn0 12535 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 98 | 75, 81 | unitgrpbas 20383 | . . . . . 6
⊢ (ℂ
∖ {0}) = (Base‘𝐺) | 
| 99 |  | proot1ex.o | . . . . . 6
⊢ 𝑂 = (od‘𝐺) | 
| 100 |  | cnfld1 21407 | . . . . . . . 8
⊢ 1 =
(1r‘ℂfld) | 
| 101 | 75, 81, 100 | unitgrpid 20386 | . . . . . . 7
⊢
(ℂfld ∈ Ring → 1 = (0g‘𝐺)) | 
| 102 | 71, 101 | ax-mp 5 | . . . . . 6
⊢ 1 =
(0g‘𝐺) | 
| 103 | 98, 99, 82, 102 | odeq 19569 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧
(-1↑𝑐(2 / 𝑁)) ∈ (ℂ ∖ {0}) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 = (𝑂‘(-1↑𝑐(2 /
𝑁))) ↔ ∀𝑥 ∈ ℕ0
(𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1))) | 
| 104 | 96, 14, 97, 103 | syl3anc 1372 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 = (𝑂‘(-1↑𝑐(2 /
𝑁))) ↔ ∀𝑥 ∈ ℕ0
(𝑁 ∥ 𝑥 ↔ (𝑥(.g‘𝐺)(-1↑𝑐(2 / 𝑁))) = 1))) | 
| 105 | 94, 104 | mpbird 257 | . . 3
⊢ (𝑁 ∈ ℕ → 𝑁 = (𝑂‘(-1↑𝑐(2 /
𝑁)))) | 
| 106 | 105 | eqcomd 2742 | . 2
⊢ (𝑁 ∈ ℕ → (𝑂‘(-1↑𝑐(2 /
𝑁))) = 𝑁) | 
| 107 | 98, 99 | odf 19556 | . . . 4
⊢ 𝑂:(ℂ ∖
{0})⟶ℕ0 | 
| 108 |  | ffn 6735 | . . . 4
⊢ (𝑂:(ℂ ∖
{0})⟶ℕ0 → 𝑂 Fn (ℂ ∖ {0})) | 
| 109 | 107, 108 | ax-mp 5 | . . 3
⊢ 𝑂 Fn (ℂ ∖
{0}) | 
| 110 |  | fniniseg 7079 | . . 3
⊢ (𝑂 Fn (ℂ ∖ {0}) →
((-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}) ↔ ((-1↑𝑐(2 /
𝑁)) ∈ (ℂ ∖
{0}) ∧ (𝑂‘(-1↑𝑐(2 /
𝑁))) = 𝑁))) | 
| 111 | 109, 110 | mp1i 13 | . 2
⊢ (𝑁 ∈ ℕ →
((-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}) ↔ ((-1↑𝑐(2 /
𝑁)) ∈ (ℂ ∖
{0}) ∧ (𝑂‘(-1↑𝑐(2 /
𝑁))) = 𝑁))) | 
| 112 | 14, 106, 111 | mpbir2and 713 | 1
⊢ (𝑁 ∈ ℕ →
(-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁})) |