Proof of Theorem dirkercncflem1
Step | Hyp | Ref
| Expression |
1 | | dirkercncflem1.a |
. . . 4
⊢ 𝐴 = (𝑌 − π) |
2 | | dirkercncflem1.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
3 | | pire 24014 |
. . . . . . 7
⊢ π
∈ ℝ |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → π ∈
ℝ) |
5 | 2, 4 | resubcld 10337 |
. . . . 5
⊢ (𝜑 → (𝑌 − π) ∈
ℝ) |
6 | 5 | rexrd 9968 |
. . . 4
⊢ (𝜑 → (𝑌 − π) ∈
ℝ*) |
7 | 1, 6 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
8 | | dirkercncflem1.b |
. . . 4
⊢ 𝐵 = (𝑌 + π) |
9 | 2, 4 | readdcld 9948 |
. . . . 5
⊢ (𝜑 → (𝑌 + π) ∈ ℝ) |
10 | 9 | rexrd 9968 |
. . . 4
⊢ (𝜑 → (𝑌 + π) ∈
ℝ*) |
11 | 8, 10 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
12 | | pipos 24016 |
. . . . . 6
⊢ 0 <
π |
13 | | ltsubpos 10399 |
. . . . . 6
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → (0 < π ↔ (𝑌 − π) < 𝑌)) |
14 | 12, 13 | mpbii 222 |
. . . . 5
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → (𝑌
− π) < 𝑌) |
15 | 4, 2, 14 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑌 − π) < 𝑌) |
16 | 1, 15 | syl5eqbr 4618 |
. . 3
⊢ (𝜑 → 𝐴 < 𝑌) |
17 | | ltaddpos 10397 |
. . . . . 6
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → (0 < π ↔ 𝑌 < (𝑌 + π))) |
18 | 12, 17 | mpbii 222 |
. . . . 5
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → 𝑌
< (𝑌 +
π)) |
19 | 4, 2, 18 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝑌 < (𝑌 + π)) |
20 | 19, 8 | syl6breqr 4625 |
. . 3
⊢ (𝜑 → 𝑌 < 𝐵) |
21 | 7, 11, 2, 16, 20 | eliood 38567 |
. 2
⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵)) |
22 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵)) |
23 | | elioore 12076 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℝ) |
25 | 24 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ) |
26 | 25 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ) |
27 | | 2cnd 10970 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈
ℂ) |
28 | | picn 24015 |
. . . . . . . . 9
⊢ π
∈ ℂ |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈
ℂ) |
30 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0) |
32 | 3, 12 | gt0ne0ii 10443 |
. . . . . . . . 9
⊢ π ≠
0 |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0) |
34 | 26, 27, 29, 31, 33 | divdiv1d 10711 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π))) |
35 | | dirkercncflem1.ymod0 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 mod (2 · π)) =
0) |
36 | | 2rp 11713 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ+ |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ+) |
38 | | pirp 24017 |
. . . . . . . . . . . . . . 15
⊢ π
∈ ℝ+ |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → π ∈
ℝ+) |
40 | 37, 39 | rpmulcld 11764 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · π) ∈
ℝ+) |
41 | | mod0 12537 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) |
42 | 2, 40, 41 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) |
43 | 35, 42 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℤ) |
44 | | peano2zm 11297 |
. . . . . . . . . . 11
⊢ ((𝑌 / (2 · π)) ∈
ℤ → ((𝑌 / (2
· π)) − 1) ∈ ℤ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈
ℤ) |
46 | 45 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) ∈
ℤ) |
47 | 45 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈
ℝ) |
48 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) ∈
ℝ) |
49 | 1, 5 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
50 | 49, 40 | rerpdivcld 11779 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 / (2 · π)) ∈
ℝ) |
51 | 50 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) ∈
ℝ) |
52 | 40 | rpred 11748 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · π) ∈
ℝ) |
53 | 52 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈
ℝ) |
54 | 40 | rpne0d 11753 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · π) ≠
0) |
55 | 54 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ≠
0) |
56 | 25, 53, 55 | redivcld 10732 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) ∈
ℝ) |
57 | 52 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · π) ∈
ℂ) |
58 | 57, 54 | dividd 10678 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · π) / (2
· π)) = 1) |
59 | 58 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 = ((2 · π) /
(2 · π))) |
60 | 59 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 / (2 · π)) −
((2 · π) / (2 · π)))) |
61 | 2 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ ℂ) |
62 | 61, 57, 57, 54 | divsubdird 10719 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 ·
π)) = ((𝑌 / (2 ·
π)) − ((2 · π) / (2 · π)))) |
63 | 60, 62 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 − (2 · π)) / (2
· π))) |
64 | 2, 52 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (2 · π)) ∈
ℝ) |
65 | 28 | mulid2i 9922 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1
· π) = π |
66 | 65 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢ π = (1
· π) |
67 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
2 |
68 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
69 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
70 | 68, 69, 3, 12 | ltmul1ii 10831 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 < 2
↔ (1 · π) < (2 · π)) |
71 | 67, 70 | mpbi 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (1
· π) < (2 · π) |
72 | 66, 71 | eqbrtri 4604 |
. . . . . . . . . . . . . . . . 17
⊢ π <
(2 · π) |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → π < (2 ·
π)) |
74 | 4, 52, 2, 73 | ltsub2dd 10519 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 − (2 · π)) < (𝑌 − π)) |
75 | 74, 1 | syl6breqr 4625 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (2 · π)) < 𝐴) |
76 | 64, 49, 40, 75 | ltdiv1dd 11805 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 ·
π)) < (𝐴 / (2
· π))) |
77 | 63, 76 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 ·
π))) |
78 | 77 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 ·
π))) |
79 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈ ℝ) |
80 | 40 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈
ℝ+) |
81 | 22 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ (𝐴(,)𝐵)) |
82 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈
ℝ*) |
83 | 11 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈
ℝ*) |
84 | | elioo2 12087 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵))) |
85 | 82, 83, 84 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵))) |
86 | 81, 85 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵)) |
87 | 86 | simp2d 1067 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 < 𝑦) |
88 | 79, 25, 80, 87 | ltdiv1dd 11805 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) < (𝑦 / (2 ·
π))) |
89 | 48, 51, 56, 78, 88 | lttrd 10077 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 ·
π))) |
90 | 89 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 ·
π))) |
91 | 24 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 ∈ ℝ) |
92 | 2 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑌 ∈ ℝ) |
93 | 40 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (2 · π) ∈
ℝ+) |
94 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 < 𝑌) |
95 | 91, 92, 93, 94 | ltdiv1dd 11805 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (𝑌 / (2 · π))) |
96 | 61, 57, 54 | divcld 10680 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℂ) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈
ℂ) |
98 | | 1cnd 9935 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈
ℂ) |
99 | 97, 98 | npcand 10275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑌 / (2 · π)) − 1) + 1) =
(𝑌 / (2 ·
π))) |
100 | 99 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) +
1)) |
101 | 100 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) +
1)) |
102 | 95, 101 | breqtrd 4609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1)
+ 1)) |
103 | | btwnnz 11329 |
. . . . . . . . 9
⊢ ((((𝑌 / (2 · π)) − 1)
∈ ℤ ∧ ((𝑌 /
(2 · π)) − 1) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) <
(((𝑌 / (2 · π))
− 1) + 1)) → ¬ (𝑦 / (2 · π)) ∈
ℤ) |
104 | 46, 90, 102, 103 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈
ℤ) |
105 | 43 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) ∈
ℤ) |
106 | 2 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 ∈ ℝ) |
107 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑦 ∈ ℝ) |
108 | 80 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (2 · π) ∈
ℝ+) |
109 | 25 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 ∈ ℝ) |
110 | 2 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ∈ ℝ) |
111 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 ≤ 𝑌) |
112 | | eldifsni 4261 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ≠ 𝑌) |
113 | 112 | necomd 2837 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑌 ≠ 𝑦) |
114 | 113 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ≠ 𝑦) |
115 | 109, 110,
111, 114 | leneltd 10070 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 < 𝑌) |
116 | 115 | stoic1a 1688 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ 𝑦 ≤ 𝑌) |
117 | 106, 107 | ltnled 10063 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑌)) |
118 | 116, 117 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 < 𝑦) |
119 | 106, 107,
108, 118 | ltdiv1dd 11805 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) < (𝑦 / (2 ·
π))) |
120 | 8, 9 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℝ) |
121 | 120, 40 | rerpdivcld 11779 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / (2 · π)) ∈
ℝ) |
122 | 121 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) ∈
ℝ) |
123 | 2, 40 | rerpdivcld 11779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℝ) |
124 | 123 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈
ℝ) |
125 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈
ℝ) |
126 | 124, 125 | readdcld 9948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) + 1) ∈
ℝ) |
127 | 120 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ) |
128 | 86 | simp3d 1068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 < 𝐵) |
129 | 25, 127, 80, 128 | ltdiv1dd 11805 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < (𝐵 / (2 · π))) |
130 | 8 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ (𝐵 / (2 · π)) = ((𝑌 + π) / (2 ·
π)) |
131 | 28 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → π ∈
ℂ) |
132 | 61, 131, 57, 54 | divdird 10718 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (π /
(2 · π)))) |
133 | 4, 40 | rerpdivcld 11779 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (π / (2 · π))
∈ ℝ) |
134 | | 1red 9934 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) |
135 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℂ |
136 | 135, 28 | mulcomi 9925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· π) = (π · 2) |
137 | 136 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (π /
(2 · π)) = (π / (π · 2)) |
138 | 28, 32 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π
∈ ℂ ∧ π ≠ 0) |
139 | | 2cnne0 11119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
140 | | divdiv1 10615 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((π
∈ ℂ ∧ (π ∈ ℂ ∧ π ≠ 0) ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((π / π) / 2) = (π / (π ·
2))) |
141 | 28, 138, 139, 140 | mp3an 1416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((π /
π) / 2) = (π / (π · 2)) |
142 | 28, 32 | dividi 10637 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π /
π) = 1 |
143 | 142 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . 18
⊢ ((π /
π) / 2) = (1 / 2) |
144 | 137, 141,
143 | 3eqtr2i 2638 |
. . . . . . . . . . . . . . . . 17
⊢ (π /
(2 · π)) = (1 / 2) |
145 | | halflt1 11127 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 2)
< 1 |
146 | 144, 145 | eqbrtri 4604 |
. . . . . . . . . . . . . . . 16
⊢ (π /
(2 · π)) < 1 |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (π / (2 · π))
< 1) |
148 | 133, 134,
123, 147 | ltadd2dd 10075 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 ·
π))) < ((𝑌 / (2
· π)) + 1)) |
149 | 132, 148 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + π) / (2 · π)) < ((𝑌 / (2 · π)) +
1)) |
150 | 130, 149 | syl5eqbr 4618 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) |
151 | 150 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) |
152 | 56, 122, 126, 129, 151 | lttrd 10077 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) |
153 | 152 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) |
154 | | btwnnz 11329 |
. . . . . . . . 9
⊢ (((𝑌 / (2 · π)) ∈
ℤ ∧ (𝑌 / (2
· π)) < (𝑦 /
(2 · π)) ∧ (𝑦
/ (2 · π)) < ((𝑌 / (2 · π)) + 1)) → ¬
(𝑦 / (2 · π))
∈ ℤ) |
155 | 105, 119,
153, 154 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈
ℤ) |
156 | 104, 155 | pm2.61dan 828 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈
ℤ) |
157 | 34, 156 | eqneltrd 2707 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈
ℤ) |
158 | 26 | halfcld 11154 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ) |
159 | | sineq0 24077 |
. . . . . . 7
⊢ ((𝑦 / 2) ∈ ℂ →
((sin‘(𝑦 / 2)) = 0
↔ ((𝑦 / 2) / π)
∈ ℤ)) |
160 | 158, 159 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈
ℤ)) |
161 | 157, 160 | mtbird 314 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0) |
162 | 161 | neqned 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0) |
163 | 34 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑦 / 2) / π) + (1 / 2)) = ((𝑦 / (2 · π)) + (1 /
2))) |
164 | 43 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈
ℤ) |
165 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 = (𝑌 − π)) |
166 | 165 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + π) = ((𝑌 − π) + π)) |
167 | 61, 131 | npcand 10275 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − π) + π) = 𝑌) |
168 | 166, 167 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 = (𝐴 + π)) |
169 | 168 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 + π) / (2 ·
π))) |
170 | 49 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
171 | 170, 131,
57, 54 | divdird 10718 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + π) / (2 · π)) = ((𝐴 / (2 · π)) + (π /
(2 · π)))) |
172 | 131 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (π · 1) =
π) |
173 | 172 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → π = (π ·
1)) |
174 | | 2cnd 10970 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
175 | 174, 131 | mulcomd 9940 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · π) = (π
· 2)) |
176 | 173, 175 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (π / (2 · π))
= ((π · 1) / (π · 2))) |
177 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℂ) |
178 | 30 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 0) |
179 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → π ≠
0) |
180 | 177, 174,
131, 178, 179 | divcan5d 10706 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((π · 1) / (π
· 2)) = (1 / 2)) |
181 | 176, 180 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → (π / (2 · π))
= (1 / 2)) |
182 | 181 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 / (2 · π)) + (π / (2 ·
π))) = ((𝐴 / (2 ·
π)) + (1 / 2))) |
183 | 169, 171,
182 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 /
2))) |
184 | 183 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 /
2))) |
185 | 125 | rehalfcld 11156 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈
ℝ) |
186 | 51, 56, 185, 88 | ltadd1dd 10517 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐴 / (2 · π)) + (1 / 2)) <
((𝑦 / (2 · π)) +
(1 / 2))) |
187 | 184, 186 | eqbrtrd 4605 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 /
2))) |
188 | 56, 122, 185, 129 | ltadd1dd 10517 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝐵 / (2 · π)) + (1 /
2))) |
189 | 130 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / (2 · π)) = ((𝑌 + π) / (2 ·
π))) |
190 | 189 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = (((𝑌 + π) / (2 · π)) +
(1 / 2))) |
191 | 181 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 ·
π))) = ((𝑌 / (2 ·
π)) + (1 / 2))) |
192 | 132, 191 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (1 /
2))) |
193 | 192 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑌 + π) / (2 · π)) + (1 / 2)) =
(((𝑌 / (2 · π)) +
(1 / 2)) + (1 / 2))) |
194 | 177 | halfcld 11154 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
195 | 96, 194, 194 | addassd 9941 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2))
= ((𝑌 / (2 · π))
+ ((1 / 2) + (1 / 2)))) |
196 | 177 | 2halvesd 11155 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1 / 2) + (1 / 2)) =
1) |
197 | 196 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2)))
= ((𝑌 / (2 · π))
+ 1)) |
198 | 195, 197 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2))
= ((𝑌 / (2 · π))
+ 1)) |
199 | 190, 193,
198 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) +
1)) |
200 | 199 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) +
1)) |
201 | 188, 200 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) +
1)) |
202 | | btwnnz 11329 |
. . . . . . . 8
⊢ (((𝑌 / (2 · π)) ∈
ℤ ∧ (𝑌 / (2
· π)) < ((𝑦 /
(2 · π)) + (1 / 2)) ∧ ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1))
→ ¬ ((𝑦 / (2
· π)) + (1 / 2)) ∈ ℤ) |
203 | 164, 187,
201, 202 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈
ℤ) |
204 | 163, 203 | eqneltrd 2707 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (((𝑦 / 2) / π) + (1 / 2)) ∈
ℤ) |
205 | | coseq0 38747 |
. . . . . . 7
⊢ ((𝑦 / 2) ∈ ℂ →
((cos‘(𝑦 / 2)) = 0
↔ (((𝑦 / 2) / π) +
(1 / 2)) ∈ ℤ)) |
206 | 158, 205 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((cos‘(𝑦 / 2)) = 0 ↔ (((𝑦 / 2) / π) + (1 / 2)) ∈
ℤ)) |
207 | 204, 206 | mtbird 314 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (cos‘(𝑦 / 2)) = 0) |
208 | 207 | neqned 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) |
209 | 162, 208 | jca 553 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)) |
210 | 209 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)) |
211 | 21, 210 | jca 553 |
1
⊢ (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠
0))) |