Proof of Theorem efif1olem2
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℝ) |
2 | | 2re 11790 |
. . . . . . 7
⊢ 2 ∈
ℝ |
3 | | pire 25203 |
. . . . . . 7
⊢ π
∈ ℝ |
4 | 2, 3 | remulcli 10735 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
5 | | readdcl 10698 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
6 | 1, 4, 5 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℝ) |
7 | | resubcl 11028 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℝ) |
8 | | 2pos 11819 |
. . . . . . . 8
⊢ 0 <
2 |
9 | | pipos 25205 |
. . . . . . . 8
⊢ 0 <
π |
10 | 2, 3, 8, 9 | mulgt0ii 10851 |
. . . . . . 7
⊢ 0 < (2
· π) |
11 | 4, 10 | elrpii 12475 |
. . . . . 6
⊢ (2
· π) ∈ ℝ+ |
12 | | modcl 13332 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
13 | 7, 11, 12 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) ∈
ℝ) |
14 | 6, 13 | resubcld 11146 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
ℝ) |
15 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℝ) |
16 | | modlt 13339 |
. . . . . . 7
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
17 | 7, 11, 16 | sylancl 589 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) < (2 ·
π)) |
18 | 13, 15, 1, 17 | ltadd2dd 10877 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 ·
π))) |
19 | 1, 13, 6 | ltaddsubd 11318 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + ((𝐴 − 𝑧) mod (2 · π))) < (𝐴 + (2 · π)) ↔
𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
20 | 18, 19 | mpbid 235 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 < ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) |
21 | | modge0 13338 |
. . . . . 6
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → 0 ≤ ((𝐴 − 𝑧) mod (2 · π))) |
22 | 7, 11, 21 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 0 ≤
((𝐴 − 𝑧) mod (2 ·
π))) |
23 | 6, 13 | subge02d 11310 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 ≤
((𝐴 − 𝑧) mod (2 · π)) ↔
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π)))) |
24 | 22, 23 | mpbid 235 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ≤
(𝐴 + (2 ·
π))) |
25 | | rexr 10765 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
26 | | elioc2 12884 |
. . . . 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 2844 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷) |
31 | | modval 13330 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ+) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
32 | 7, 11, 31 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) mod (2 · π)) = ((𝐴 − 𝑧) − ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 ·
π)))))) |
33 | 32 | oveq2d 7186 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) =
((𝐴 + (2 · π))
− ((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
34 | 6 | recnd 10747 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 + (2 · π)) ∈
ℂ) |
35 | 7 | recnd 10747 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 − 𝑧) ∈ ℂ) |
36 | 4, 10 | gt0ne0ii 11254 |
. . . . . . . . . . . . . . 15
⊢ (2
· π) ≠ 0 |
37 | | redivcl 11437 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑧) ∈ ℝ ∧ (2 · π)
∈ ℝ ∧ (2 · π) ≠ 0) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
38 | 4, 36, 37 | mp3an23 1454 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 − 𝑧) ∈ ℝ → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
39 | 7, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 − 𝑧) / (2 · π)) ∈
ℝ) |
40 | 39 | flcld 13259 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℤ) |
41 | 40 | zred 12168 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℝ) |
42 | | remulcl 10700 |
. . . . . . . . . . 11
⊢ (((2
· π) ∈ ℝ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℝ)
→ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
43 | 4, 41, 42 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℝ) |
44 | 43 | recnd 10747 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℂ) |
45 | 34, 35, 44 | subsubd 11103 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) − ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π)))))) = (((𝐴 + (2
· π)) − (𝐴
− 𝑧)) + ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
46 | 1 | recnd 10747 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝐴 ∈
ℂ) |
47 | 4 | recni 10733 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (2
· π) ∈ ℂ) |
49 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℝ) |
50 | 49 | recnd 10747 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) |
51 | 46, 48, 50 | pnncand 11114 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) = ((2 · π) + 𝑧)) |
52 | 51 | oveq1d 7185 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐴 + (2 · π)) −
(𝐴 − 𝑧)) + ((2 · π) ·
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
= (((2 · π) + 𝑧)
+ ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
53 | 33, 45, 52 | 3eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) = (((2
· π) + 𝑧) + ((2
· π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
54 | 53 | oveq2d 7186 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
55 | | addcl 10697 |
. . . . . . . 8
⊢ (((2
· π) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((2 · π) +
𝑧) ∈
ℂ) |
56 | 47, 50, 55 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) + 𝑧) ∈
ℂ) |
57 | 50, 56, 44 | subsub4d 11106 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (𝑧 − (((2 · π) +
𝑧) + ((2 · π)
· (⌊‘((𝐴
− 𝑧) / (2 ·
π))))))) |
58 | 56, 50 | negsubdi2d 11091 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = (𝑧 − ((2 · π) + 𝑧))) |
59 | 48, 50 | pncand 11076 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((2
· π) + 𝑧) −
𝑧) = (2 ·
π)) |
60 | 59 | negeqd 10958 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -(((2
· π) + 𝑧) −
𝑧) = -(2 ·
π)) |
61 | 58, 60 | eqtr3d 2775 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = -(2 ·
π)) |
62 | | neg1cn 11830 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
63 | 47 | mulm1i 11163 |
. . . . . . . . . 10
⊢ (-1
· (2 · π)) = -(2 · π) |
64 | 62, 47, 63 | mulcomli 10728 |
. . . . . . . . 9
⊢ ((2
· π) · -1) = -(2 · π) |
65 | 61, 64 | eqtr4di 2791 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((2 · π) +
𝑧)) = ((2 · π)
· -1)) |
66 | 65 | oveq1d 7185 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
67 | 62 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -1
∈ ℂ) |
68 | 40 | zcnd 12169 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(⌊‘((𝐴 −
𝑧) / (2 · π)))
∈ ℂ) |
69 | 48, 67, 68 | subdid 11174 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((2
· π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) = (((2 ·
π) · -1) − ((2 · π) · (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
70 | 66, 69 | eqtr4d 2776 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((2 · π) +
𝑧)) − ((2 ·
π) · (⌊‘((𝐴 − 𝑧) / (2 · π))))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
71 | 54, 57, 70 | 3eqtr2d 2779 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) = ((2 ·
π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))))) |
72 | 71 | oveq1d 7185 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (((2 · π) · (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) / (2 ·
π))) |
73 | | neg1z 12099 |
. . . . . . 7
⊢ -1 ∈
ℤ |
74 | | zsubcl 12105 |
. . . . . . 7
⊢ ((-1
∈ ℤ ∧ (⌊‘((𝐴 − 𝑧) / (2 · π))) ∈ ℤ)
→ (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π)))) ∈
ℤ) |
75 | 73, 40, 74 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℤ) |
76 | 75 | zcnd 12169 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ) |
77 | | divcan3 11402 |
. . . . . 6
⊢ (((-1
− (⌊‘((𝐴
− 𝑧) / (2 ·
π)))) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2
· π) ≠ 0) → (((2 · π) · (-1 −
(⌊‘((𝐴 −
𝑧) / (2 · π)))))
/ (2 · π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
78 | 47, 36, 77 | mp3an23 1454 |
. . . . 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 2773 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) = (-1 − (⌊‘((𝐴 − 𝑧) / (2 · π))))) |
81 | 80, 75 | eqeltrd 2833 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) |
82 | | oveq2 7178 |
. . . . 5
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (𝑧 − 𝑦) = (𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))))) |
83 | 82 | oveq1d 7185 |
. . . 4
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → ((𝑧 − 𝑦) / (2 · π)) = ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π))) |
84 | 83 | eleq1d 2817 |
. . 3
⊢ (𝑦 = ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π))) → (((𝑧 − 𝑦) / (2 · π)) ∈ ℤ ↔
((𝑧 − ((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π)))) / (2
· π)) ∈ ℤ)) |
85 | 84 | rspcev 3526 |
. 2
⊢ ((((𝐴 + (2 · π)) −
((𝐴 − 𝑧) mod (2 · π))) ∈
𝐷 ∧ ((𝑧 − ((𝐴 + (2 · π)) − ((𝐴 − 𝑧) mod (2 · π)))) / (2 ·
π)) ∈ ℤ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
86 | 30, 81, 85 | syl2anc 587 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |