Proof of Theorem efif1olem2
Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℝ) |
2 | | 2re 12337 |
. . . . . . 7
⊢ 2 ∈
ℝ |
3 | | pire 26514 |
. . . . . . 7
⊢ π
∈ ℝ |
4 | 2, 3 | remulcli 11274 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
5 | | readdcl 11235 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
6 | 1, 4, 5 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
7 | | resubcl 11570 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℝ) |
8 | | 2pos 12366 |
. . . . . . . 8
⊢ 0 <
2 |
9 | | pipos 26516 |
. . . . . . . 8
⊢ 0 <
π |
10 | 2, 3, 8, 9 | mulgt0ii 11391 |
. . . . . . 7
⊢ 0 < (2
· π) |
11 | 4, 10 | elrpii 13034 |
. . . . . 6
⊢ (2
· π) ∈ ℝ+ |
12 | | modcl 13909 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
13 | 7, 11, 12 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
14 | 6, 13 | resubcld 11688 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ) |
15 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℝ) |
16 | | modlt 13916 |
. . . . . . 7
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
17 | 7, 11, 16 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
18 | 13, 15, 1, 17 | ltadd2dd 11417 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 ·
π))) |
19 | 1, 13, 6 | ltaddsubd 11860 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 · π)) ↔
𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
20 | 18, 19 | mpbid 232 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) |
21 | | modge0 13915 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → 0 ≤ ((𝐴 − 𝑧) mod (2 · π))) |
22 | 7, 11, 21 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 0 ≤
((𝐴 − 𝑧) mod (2 ·
π))) |
23 | 6, 13 | subge02d 11852 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 ≤
((𝐴 − 𝑧) mod (2 · π)) ↔
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π)))) |
24 | 22, 23 | mpbid 232 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))) |
25 | | rexr 11304 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
26 | | elioc2 13446 |
. . . . 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 1341 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
(𝐴(,](𝐴 + (2 · π)))) |
29 | | efif1olem1.1 |
. . 3
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) |
30 | 28, 29 | eleqtrrdi 2849 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷) |
31 | | modval 13907 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
32 | 7, 11, 31 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
33 | 32 | oveq2d 7446 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) =
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
34 | 6 | recnd 11286 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℂ) |
35 | 7 | recnd 11286 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℂ) |
36 | 4, 10 | gt0ne0ii 11796 |
. . . . . . . . . . . . . . 15
⊢ (2
· π) ≠ 0 |
37 | | redivcl 11983 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ ∧ (2 · π) ≠ 0) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
38 | 4, 36, 37 | mp3an23 1452 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 − 𝑧) ∈ ℝ → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
39 | 7, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
40 | 39 | flcld 13834 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℤ) |
41 | 40 | zred 12719 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℝ) |
42 | | remulcl 11237 |
. . . . . . . . . . 11
⊢ (((2
· π) ∈ ℝ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℝ)
→ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
43 | 4, 41, 42 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
44 | 43 | recnd 11286 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℂ) |
45 | 34, 35, 44 | subsubd 11645 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π)))))) = (((𝐴 + (2
· π)) − (𝐴
− 𝑧)) + ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
46 | 1 | recnd 11286 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℂ) |
47 | 4 | recni 11272 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℂ) |
49 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℝ) |
50 | 49 | recnd 11286 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) |
51 | 46, 48, 50 | pnncand 11656 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) = ((2 · π) + 𝑧)) |
52 | 51 | oveq1d 7445 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) + ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
= (((2 · π) + 𝑧)
+ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
53 | 33, 45, 52 | 3eqtrd 2778 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) = (((2
· π) + 𝑧) + ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
54 | 53 | oveq2d 7446 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
55 | | addcl 11234 |
. . . . . . . 8
⊢ (((2
· π) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((2 · π) +
𝑧) ∈
ℂ) |
56 | 47, 50, 55 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) + 𝑧) ∈
ℂ) |
57 | 50, 56, 44 | subsub4d 11648 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
58 | 56, 50 | negsubdi2d 11633 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = (𝑧 − ((2 · π) + 𝑧))) |
59 | 48, 50 | pncand 11618 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((2
· π) + 𝑧) −
𝑧) = (2 ·
π)) |
60 | 59 | negeqd 11499 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = -(2 ·
π)) |
61 | 58, 60 | eqtr3d 2776 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = -(2 ·
π)) |
62 | | neg1cn 12377 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
63 | 47 | mulm1i 11705 |
. . . . . . . . . 10
⊢ (-1
· (2 · π)) = -(2 · π) |
64 | 62, 47, 63 | mulcomli 11267 |
. . . . . . . . 9
⊢ ((2
· π) · -1) = -(2 · π) |
65 | 61, 64 | eqtr4di 2792 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = ((2 · π)
· -1)) |
66 | 65 | oveq1d 7445 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
67 | 62 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -1
∈ ℂ) |
68 | 40 | zcnd 12720 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℂ) |
69 | 48, 67, 68 | subdid 11716 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
70 | 66, 69 | eqtr4d 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
71 | 54, 57, 70 | 3eqtr2d 2780 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
72 | 71 | oveq1d 7445 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (((2 · π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) / (2 ·
π))) |
73 | | neg1z 12650 |
. . . . . . 7
⊢ -1 ∈
ℤ |
74 | | zsubcl 12656 |
. . . . . . 7
⊢ ((-1
∈ ℤ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℤ)
→ (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℤ) |
75 | 73, 40, 74 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℤ) |
76 | 75 | zcnd 12720 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ) |
77 | | divcan3 11945 |
. . . . . 6
⊢ (((-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2
· π) ≠ 0) → (((2 · π) · (-1 −
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
/ (2 · π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
78 | 47, 36, 77 | mp3an23 1452 |
. . . . 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 2774 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
81 | 80, 75 | eqeltrd 2838 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) |
82 | | oveq2 7438 |
. . . . 5
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (𝑧 − 𝑦) = (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
83 | 82 | oveq1d 7445 |
. . . 4
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → ((𝑧 − 𝑦) / (2 · π)) = ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π))) |
84 | 83 | eleq1d 2823 |
. . 3
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (((𝑧 − 𝑦) / (2 · π)) ∈ ℤ ↔
((𝑧 − ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π)))) / (2
· π)) ∈ ℤ)) |
85 | 84 | rspcev 3621 |
. 2
⊢ ((((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷 ∧ ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
86 | 30, 81, 85 | syl2anc 584 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |