Proof of Theorem efif1olem2
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℝ) |
2 | | 2re 12047 |
. . . . . . 7
⊢ 2 ∈
ℝ |
3 | | pire 25615 |
. . . . . . 7
⊢ π
∈ ℝ |
4 | 2, 3 | remulcli 10991 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
5 | | readdcl 10954 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
6 | 1, 4, 5 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
7 | | resubcl 11285 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℝ) |
8 | | 2pos 12076 |
. . . . . . . 8
⊢ 0 <
2 |
9 | | pipos 25617 |
. . . . . . . 8
⊢ 0 <
π |
10 | 2, 3, 8, 9 | mulgt0ii 11108 |
. . . . . . 7
⊢ 0 < (2
· π) |
11 | 4, 10 | elrpii 12733 |
. . . . . 6
⊢ (2
· π) ∈ ℝ+ |
12 | | modcl 13593 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
13 | 7, 11, 12 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
14 | 6, 13 | resubcld 11403 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ) |
15 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℝ) |
16 | | modlt 13600 |
. . . . . . 7
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
17 | 7, 11, 16 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
18 | 13, 15, 1, 17 | ltadd2dd 11134 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 ·
π))) |
19 | 1, 13, 6 | ltaddsubd 11575 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 · π)) ↔
𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
20 | 18, 19 | mpbid 231 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) |
21 | | modge0 13599 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → 0 ≤ ((𝐴 − 𝑧) mod (2 · π))) |
22 | 7, 11, 21 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 0 ≤
((𝐴 − 𝑧) mod (2 ·
π))) |
23 | 6, 13 | subge02d 11567 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 ≤
((𝐴 − 𝑧) mod (2 · π)) ↔
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π)))) |
24 | 22, 23 | mpbid 231 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))) |
25 | | rexr 11021 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
26 | | elioc2 13142 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐴 + (2 ·
π)) ∈ ℝ) → (((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) ∈ (𝐴(,](𝐴 + (2 · π))) ↔ (((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ ∧ 𝐴 <
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ∧
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))))) |
27 | 25, 6, 26 | syl2an2r 682 |
. . . 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 2850 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷) |
31 | | modval 13591 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
32 | 7, 11, 31 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
33 | 32 | oveq2d 7291 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) =
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
34 | 6 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℂ) |
35 | 7 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℂ) |
36 | 4, 10 | gt0ne0ii 11511 |
. . . . . . . . . . . . . . 15
⊢ (2
· π) ≠ 0 |
37 | | redivcl 11694 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ ∧ (2 · π) ≠ 0) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
38 | 4, 36, 37 | mp3an23 1452 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 − 𝑧) ∈ ℝ → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
39 | 7, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
40 | 39 | flcld 13518 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℤ) |
41 | 40 | zred 12426 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℝ) |
42 | | remulcl 10956 |
. . . . . . . . . . 11
⊢ (((2
· π) ∈ ℝ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℝ)
→ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
43 | 4, 41, 42 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
44 | 43 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℂ) |
45 | 34, 35, 44 | subsubd 11360 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π)))))) = (((𝐴 + (2
· π)) − (𝐴
− 𝑧)) + ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
46 | 1 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℂ) |
47 | 4 | recni 10989 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℂ) |
49 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℝ) |
50 | 49 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) |
51 | 46, 48, 50 | pnncand 11371 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) = ((2 · π) + 𝑧)) |
52 | 51 | oveq1d 7290 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) + ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
= (((2 · π) + 𝑧)
+ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
53 | 33, 45, 52 | 3eqtrd 2782 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) = (((2
· π) + 𝑧) + ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
54 | 53 | oveq2d 7291 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
55 | | addcl 10953 |
. . . . . . . 8
⊢ (((2
· π) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((2 · π) +
𝑧) ∈
ℂ) |
56 | 47, 50, 55 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) + 𝑧) ∈
ℂ) |
57 | 50, 56, 44 | subsub4d 11363 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
58 | 56, 50 | negsubdi2d 11348 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = (𝑧 − ((2 · π) + 𝑧))) |
59 | 48, 50 | pncand 11333 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((2
· π) + 𝑧) −
𝑧) = (2 ·
π)) |
60 | 59 | negeqd 11215 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = -(2 ·
π)) |
61 | 58, 60 | eqtr3d 2780 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = -(2 ·
π)) |
62 | | neg1cn 12087 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
63 | 47 | mulm1i 11420 |
. . . . . . . . . 10
⊢ (-1
· (2 · π)) = -(2 · π) |
64 | 62, 47, 63 | mulcomli 10984 |
. . . . . . . . 9
⊢ ((2
· π) · -1) = -(2 · π) |
65 | 61, 64 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = ((2 · π)
· -1)) |
66 | 65 | oveq1d 7290 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
67 | 62 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -1
∈ ℂ) |
68 | 40 | zcnd 12427 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℂ) |
69 | 48, 67, 68 | subdid 11431 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
70 | 66, 69 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
71 | 54, 57, 70 | 3eqtr2d 2784 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
72 | 71 | oveq1d 7290 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (((2 · π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) / (2 ·
π))) |
73 | | neg1z 12356 |
. . . . . . 7
⊢ -1 ∈
ℤ |
74 | | zsubcl 12362 |
. . . . . . 7
⊢ ((-1
∈ ℤ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℤ)
→ (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℤ) |
75 | 73, 40, 74 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℤ) |
76 | 75 | zcnd 12427 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ) |
77 | | divcan3 11659 |
. . . . . 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 2778 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
81 | 80, 75 | eqeltrd 2839 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) |
82 | | oveq2 7283 |
. . . . 5
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (𝑧 − 𝑦) = (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
83 | 82 | oveq1d 7290 |
. . . 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 3561 |
. 2
⊢ ((((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷 ∧ ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
86 | 30, 81, 85 | syl2anc 584 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |