Proof of Theorem efif1olem2
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℝ) |
| 2 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 3 | | pire 26500 |
. . . . . . 7
⊢ π
∈ ℝ |
| 4 | 2, 3 | remulcli 11277 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
| 5 | | readdcl 11238 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
| 6 | 1, 4, 5 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
| 7 | | resubcl 11573 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℝ) |
| 8 | | 2pos 12369 |
. . . . . . . 8
⊢ 0 <
2 |
| 9 | | pipos 26502 |
. . . . . . . 8
⊢ 0 <
π |
| 10 | 2, 3, 8, 9 | mulgt0ii 11394 |
. . . . . . 7
⊢ 0 < (2
· π) |
| 11 | 4, 10 | elrpii 13037 |
. . . . . 6
⊢ (2
· π) ∈ ℝ+ |
| 12 | | modcl 13913 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
| 13 | 7, 11, 12 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
| 14 | 6, 13 | resubcld 11691 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ) |
| 15 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℝ) |
| 16 | | modlt 13920 |
. . . . . . 7
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
| 17 | 7, 11, 16 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
| 18 | 13, 15, 1, 17 | ltadd2dd 11420 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 ·
π))) |
| 19 | 1, 13, 6 | ltaddsubd 11863 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 · π)) ↔
𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
| 20 | 18, 19 | mpbid 232 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) |
| 21 | | modge0 13919 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → 0 ≤ ((𝐴 − 𝑧) mod (2 · π))) |
| 22 | 7, 11, 21 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 0 ≤
((𝐴 − 𝑧) mod (2 ·
π))) |
| 23 | 6, 13 | subge02d 11855 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 ≤
((𝐴 − 𝑧) mod (2 · π)) ↔
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π)))) |
| 24 | 22, 23 | mpbid 232 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))) |
| 25 | | rexr 11307 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
| 26 | | elioc2 13450 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐴 + (2 ·
π)) ∈ ℝ) → (((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) ∈ (𝐴(,](𝐴 + (2 · π))) ↔ (((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ ∧ 𝐴 <
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ∧
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))))) |
| 27 | 25, 6, 26 | syl2an2r 685 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
(𝐴(,](𝐴 + (2 · π))) ↔ (((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ ∧ 𝐴 <
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ∧
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))))) |
| 28 | 14, 20, 24, 27 | mpbir3and 1343 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
(𝐴(,](𝐴 + (2 · π)))) |
| 29 | | efif1olem1.1 |
. . 3
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) |
| 30 | 28, 29 | eleqtrrdi 2852 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷) |
| 31 | | modval 13911 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
| 32 | 7, 11, 31 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
| 33 | 32 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) =
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
| 34 | 6 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℂ) |
| 35 | 7 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℂ) |
| 36 | 4, 10 | gt0ne0ii 11799 |
. . . . . . . . . . . . . . 15
⊢ (2
· π) ≠ 0 |
| 37 | | redivcl 11986 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ ∧ (2 · π) ≠ 0) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
| 38 | 4, 36, 37 | mp3an23 1455 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 − 𝑧) ∈ ℝ → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
| 39 | 7, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
| 40 | 39 | flcld 13838 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℤ) |
| 41 | 40 | zred 12722 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℝ) |
| 42 | | remulcl 11240 |
. . . . . . . . . . 11
⊢ (((2
· π) ∈ ℝ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℝ)
→ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
| 43 | 4, 41, 42 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
| 44 | 43 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℂ) |
| 45 | 34, 35, 44 | subsubd 11648 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π)))))) = (((𝐴 + (2
· π)) − (𝐴
− 𝑧)) + ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 46 | 1 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℂ) |
| 47 | 4 | recni 11275 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
| 48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℂ) |
| 49 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℝ) |
| 50 | 49 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) |
| 51 | 46, 48, 50 | pnncand 11659 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) = ((2 · π) + 𝑧)) |
| 52 | 51 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) + ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
= (((2 · π) + 𝑧)
+ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 53 | 33, 45, 52 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) = (((2
· π) + 𝑧) + ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 54 | 53 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
| 55 | | addcl 11237 |
. . . . . . . 8
⊢ (((2
· π) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((2 · π) +
𝑧) ∈
ℂ) |
| 56 | 47, 50, 55 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) + 𝑧) ∈
ℂ) |
| 57 | 50, 56, 44 | subsub4d 11651 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
| 58 | 56, 50 | negsubdi2d 11636 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = (𝑧 − ((2 · π) + 𝑧))) |
| 59 | 48, 50 | pncand 11621 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((2
· π) + 𝑧) −
𝑧) = (2 ·
π)) |
| 60 | 59 | negeqd 11502 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = -(2 ·
π)) |
| 61 | 58, 60 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = -(2 ·
π)) |
| 62 | | neg1cn 12380 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
| 63 | 47 | mulm1i 11708 |
. . . . . . . . . 10
⊢ (-1
· (2 · π)) = -(2 · π) |
| 64 | 62, 47, 63 | mulcomli 11270 |
. . . . . . . . 9
⊢ ((2
· π) · -1) = -(2 · π) |
| 65 | 61, 64 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = ((2 · π)
· -1)) |
| 66 | 65 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 67 | 62 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -1
∈ ℂ) |
| 68 | 40 | zcnd 12723 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℂ) |
| 69 | 48, 67, 68 | subdid 11719 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 70 | 66, 69 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 71 | 54, 57, 70 | 3eqtr2d 2783 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
| 72 | 71 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (((2 · π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) / (2 ·
π))) |
| 73 | | neg1z 12653 |
. . . . . . 7
⊢ -1 ∈
ℤ |
| 74 | | zsubcl 12659 |
. . . . . . 7
⊢ ((-1
∈ ℤ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℤ)
→ (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℤ) |
| 75 | 73, 40, 74 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℤ) |
| 76 | 75 | zcnd 12723 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ) |
| 77 | | divcan3 11948 |
. . . . . 6
⊢ (((-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2
· π) ≠ 0) → (((2 · π) · (-1 −
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
/ (2 · π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
| 78 | 47, 36, 77 | mp3an23 1455 |
. . . . 5
⊢ ((-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ → (((2 · π) · (-1 −
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
/ (2 · π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
| 79 | 76, 78 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((2
· π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) / (2 ·
π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
| 80 | 72, 79 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
| 81 | 80, 75 | eqeltrd 2841 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) |
| 82 | | oveq2 7439 |
. . . . 5
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (𝑧 − 𝑦) = (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
| 83 | 82 | oveq1d 7446 |
. . . 4
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → ((𝑧 − 𝑦) / (2 · π)) = ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π))) |
| 84 | 83 | eleq1d 2826 |
. . 3
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (((𝑧 − 𝑦) / (2 · π)) ∈ ℤ ↔
((𝑧 − ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π)))) / (2
· π)) ∈ ℤ)) |
| 85 | 84 | rspcev 3622 |
. 2
⊢ ((((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷 ∧ ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
| 86 | 30, 81, 85 | syl2anc 584 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |