Proof of Theorem dirkercncflem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dirkercncflem1.a | . . . 4
⊢ 𝐴 = (𝑌 − π) | 
| 2 |  | dirkercncflem1.y | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 3 |  | pire 26501 | . . . . . . 7
⊢ π
∈ ℝ | 
| 4 | 3 | a1i 11 | . . . . . 6
⊢ (𝜑 → π ∈
ℝ) | 
| 5 | 2, 4 | resubcld 11692 | . . . . 5
⊢ (𝜑 → (𝑌 − π) ∈
ℝ) | 
| 6 | 5 | rexrd 11312 | . . . 4
⊢ (𝜑 → (𝑌 − π) ∈
ℝ*) | 
| 7 | 1, 6 | eqeltrid 2844 | . . 3
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 8 |  | dirkercncflem1.b | . . . 4
⊢ 𝐵 = (𝑌 + π) | 
| 9 | 2, 4 | readdcld 11291 | . . . . 5
⊢ (𝜑 → (𝑌 + π) ∈ ℝ) | 
| 10 | 9 | rexrd 11312 | . . . 4
⊢ (𝜑 → (𝑌 + π) ∈
ℝ*) | 
| 11 | 8, 10 | eqeltrid 2844 | . . 3
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 12 |  | pipos 26503 | . . . . . 6
⊢ 0 <
π | 
| 13 |  | ltsubpos 11756 | . . . . . 6
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → (0 < π ↔ (𝑌 − π) < 𝑌)) | 
| 14 | 12, 13 | mpbii 233 | . . . . 5
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → (𝑌
− π) < 𝑌) | 
| 15 | 4, 2, 14 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑌 − π) < 𝑌) | 
| 16 | 1, 15 | eqbrtrid 5177 | . . 3
⊢ (𝜑 → 𝐴 < 𝑌) | 
| 17 |  | ltaddpos 11754 | . . . . . 6
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → (0 < π ↔ 𝑌 < (𝑌 + π))) | 
| 18 | 12, 17 | mpbii 233 | . . . . 5
⊢ ((π
∈ ℝ ∧ 𝑌
∈ ℝ) → 𝑌
< (𝑌 +
π)) | 
| 19 | 4, 2, 18 | syl2anc 584 | . . . 4
⊢ (𝜑 → 𝑌 < (𝑌 + π)) | 
| 20 | 19, 8 | breqtrrdi 5184 | . . 3
⊢ (𝜑 → 𝑌 < 𝐵) | 
| 21 | 7, 11, 2, 16, 20 | eliood 45516 | . 2
⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵)) | 
| 22 |  | eldifi 4130 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵)) | 
| 23 | 22 | elioored 45567 | . . . . . . . . . 10
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℝ) | 
| 24 | 23 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ) | 
| 25 | 24 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ) | 
| 26 |  | 2cnd 12345 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈
ℂ) | 
| 27 |  | picn 26502 | . . . . . . . . 9
⊢ π
∈ ℂ | 
| 28 | 27 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈
ℂ) | 
| 29 |  | 2ne0 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0) | 
| 31 | 3, 12 | gt0ne0ii 11800 | . . . . . . . . 9
⊢ π ≠
0 | 
| 32 | 31 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0) | 
| 33 | 25, 26, 28, 30, 32 | divdiv1d 12075 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π))) | 
| 34 |  | dirkercncflem1.ymod0 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 mod (2 · π)) =
0) | 
| 35 |  | 2rp 13040 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ+ | 
| 36 | 35 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 37 |  | pirp 26504 | . . . . . . . . . . . . . . 15
⊢ π
∈ ℝ+ | 
| 38 | 37 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → π ∈
ℝ+) | 
| 39 | 36, 38 | rpmulcld 13094 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · π) ∈
ℝ+) | 
| 40 |  | mod0 13917 | . . . . . . . . . . . . 13
⊢ ((𝑌 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) | 
| 41 | 2, 39, 40 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) | 
| 42 | 34, 41 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℤ) | 
| 43 |  | peano2zm 12662 | . . . . . . . . . . 11
⊢ ((𝑌 / (2 · π)) ∈
ℤ → ((𝑌 / (2
· π)) − 1) ∈ ℤ) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈
ℤ) | 
| 45 | 44 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) ∈
ℤ) | 
| 46 | 44 | zred 12724 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈
ℝ) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) ∈
ℝ) | 
| 48 | 1, 5 | eqeltrid 2844 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 49 | 48, 39 | rerpdivcld 13109 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 / (2 · π)) ∈
ℝ) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) ∈
ℝ) | 
| 51 | 39 | rpred 13078 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · π) ∈
ℝ) | 
| 52 | 51 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈
ℝ) | 
| 53 | 39 | rpne0d 13083 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · π) ≠
0) | 
| 54 | 53 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ≠
0) | 
| 55 | 24, 52, 54 | redivcld 12096 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) ∈
ℝ) | 
| 56 | 51 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · π) ∈
ℂ) | 
| 57 | 56, 53 | dividd 12042 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · π) / (2
· π)) = 1) | 
| 58 | 57 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 = ((2 · π) /
(2 · π))) | 
| 59 | 58 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 / (2 · π)) −
((2 · π) / (2 · π)))) | 
| 60 | 2 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ ℂ) | 
| 61 | 60, 56, 56, 53 | divsubdird 12083 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 ·
π)) = ((𝑌 / (2 ·
π)) − ((2 · π) / (2 · π)))) | 
| 62 | 59, 61 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 − (2 · π)) / (2
· π))) | 
| 63 | 2, 51 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (2 · π)) ∈
ℝ) | 
| 64 | 27 | mullidi 11267 | . . . . . . . . . . . . . . . . . . 19
⊢ (1
· π) = π | 
| 65 | 64 | eqcomi 2745 | . . . . . . . . . . . . . . . . . 18
⊢ π = (1
· π) | 
| 66 |  | 1lt2 12438 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 <
2 | 
| 67 |  | 1re 11262 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ | 
| 68 |  | 2re 12341 | . . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ | 
| 69 | 67, 68, 3, 12 | ltmul1ii 12197 | . . . . . . . . . . . . . . . . . . 19
⊢ (1 < 2
↔ (1 · π) < (2 · π)) | 
| 70 | 66, 69 | mpbi 230 | . . . . . . . . . . . . . . . . . 18
⊢ (1
· π) < (2 · π) | 
| 71 | 65, 70 | eqbrtri 5163 | . . . . . . . . . . . . . . . . 17
⊢ π <
(2 · π) | 
| 72 | 71 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → π < (2 ·
π)) | 
| 73 | 4, 51, 2, 72 | ltsub2dd 11877 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 − (2 · π)) < (𝑌 − π)) | 
| 74 | 73, 1 | breqtrrdi 5184 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (2 · π)) < 𝐴) | 
| 75 | 63, 48, 39, 74 | ltdiv1dd 13135 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 ·
π)) < (𝐴 / (2
· π))) | 
| 76 | 62, 75 | eqbrtrd 5164 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 ·
π))) | 
| 77 | 76 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 ·
π))) | 
| 78 | 48 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈ ℝ) | 
| 79 | 39 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈
ℝ+) | 
| 80 | 22 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ (𝐴(,)𝐵)) | 
| 81 | 7 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈
ℝ*) | 
| 82 | 11 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈
ℝ*) | 
| 83 |  | elioo2 13429 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵))) | 
| 84 | 81, 82, 83 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵))) | 
| 85 | 80, 84 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵)) | 
| 86 | 85 | simp2d 1143 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 < 𝑦) | 
| 87 | 78, 24, 79, 86 | ltdiv1dd 13135 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) < (𝑦 / (2 ·
π))) | 
| 88 | 47, 50, 55, 77, 87 | lttrd 11423 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 ·
π))) | 
| 89 | 88 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 ·
π))) | 
| 90 | 23 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 ∈ ℝ) | 
| 91 | 2 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑌 ∈ ℝ) | 
| 92 | 39 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (2 · π) ∈
ℝ+) | 
| 93 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 < 𝑌) | 
| 94 | 90, 91, 92, 93 | ltdiv1dd 13135 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (𝑌 / (2 · π))) | 
| 95 | 60, 56, 53 | divcld 12044 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℂ) | 
| 96 | 95 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈
ℂ) | 
| 97 |  | 1cnd 11257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈
ℂ) | 
| 98 | 96, 97 | npcand 11625 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑌 / (2 · π)) − 1) + 1) =
(𝑌 / (2 ·
π))) | 
| 99 | 98 | eqcomd 2742 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) +
1)) | 
| 100 | 99 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) +
1)) | 
| 101 | 94, 100 | breqtrd 5168 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1)
+ 1)) | 
| 102 |  | btwnnz 12696 | . . . . . . . . 9
⊢ ((((𝑌 / (2 · π)) − 1)
∈ ℤ ∧ ((𝑌 /
(2 · π)) − 1) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) <
(((𝑌 / (2 · π))
− 1) + 1)) → ¬ (𝑦 / (2 · π)) ∈
ℤ) | 
| 103 | 45, 89, 101, 102 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈
ℤ) | 
| 104 | 42 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) ∈
ℤ) | 
| 105 | 2 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 ∈ ℝ) | 
| 106 | 24 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑦 ∈ ℝ) | 
| 107 | 79 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (2 · π) ∈
ℝ+) | 
| 108 | 24 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 ∈ ℝ) | 
| 109 | 2 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ∈ ℝ) | 
| 110 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 ≤ 𝑌) | 
| 111 |  | eldifsni 4789 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ≠ 𝑌) | 
| 112 | 111 | necomd 2995 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑌 ≠ 𝑦) | 
| 113 | 112 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ≠ 𝑦) | 
| 114 | 108, 109,
110, 113 | leneltd 11416 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 < 𝑌) | 
| 115 | 114 | stoic1a 1771 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ 𝑦 ≤ 𝑌) | 
| 116 | 105, 106 | ltnled 11409 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑌)) | 
| 117 | 115, 116 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 < 𝑦) | 
| 118 | 105, 106,
107, 117 | ltdiv1dd 13135 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) < (𝑦 / (2 ·
π))) | 
| 119 | 8, 9 | eqeltrid 2844 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 120 | 119, 39 | rerpdivcld 13109 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / (2 · π)) ∈
ℝ) | 
| 121 | 120 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) ∈
ℝ) | 
| 122 | 2, 39 | rerpdivcld 13109 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℝ) | 
| 123 | 122 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈
ℝ) | 
| 124 |  | 1red 11263 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈
ℝ) | 
| 125 | 123, 124 | readdcld 11291 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) + 1) ∈
ℝ) | 
| 126 | 119 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ) | 
| 127 | 85 | simp3d 1144 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 < 𝐵) | 
| 128 | 24, 126, 79, 127 | ltdiv1dd 13135 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < (𝐵 / (2 · π))) | 
| 129 | 8 | oveq1i 7442 | . . . . . . . . . . . . 13
⊢ (𝐵 / (2 · π)) = ((𝑌 + π) / (2 ·
π)) | 
| 130 | 27 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → π ∈
ℂ) | 
| 131 | 60, 130, 56, 53 | divdird 12082 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (π /
(2 · π)))) | 
| 132 | 4, 39 | rerpdivcld 13109 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (π / (2 · π))
∈ ℝ) | 
| 133 |  | 1red 11263 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) | 
| 134 |  | 2cn 12342 | . . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℂ | 
| 135 | 134, 27 | mulcomi 11270 | . . . . . . . . . . . . . . . . . . 19
⊢ (2
· π) = (π · 2) | 
| 136 | 135 | oveq2i 7443 | . . . . . . . . . . . . . . . . . 18
⊢ (π /
(2 · π)) = (π / (π · 2)) | 
| 137 | 27, 31 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . 19
⊢ (π
∈ ℂ ∧ π ≠ 0) | 
| 138 |  | 2cnne0 12477 | . . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 139 |  | divdiv1 11979 | . . . . . . . . . . . . . . . . . . 19
⊢ ((π
∈ ℂ ∧ (π ∈ ℂ ∧ π ≠ 0) ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((π / π) / 2) = (π / (π ·
2))) | 
| 140 | 27, 137, 138, 139 | mp3an 1462 | . . . . . . . . . . . . . . . . . 18
⊢ ((π /
π) / 2) = (π / (π · 2)) | 
| 141 | 27, 31 | dividi 12001 | . . . . . . . . . . . . . . . . . . 19
⊢ (π /
π) = 1 | 
| 142 | 141 | oveq1i 7442 | . . . . . . . . . . . . . . . . . 18
⊢ ((π /
π) / 2) = (1 / 2) | 
| 143 | 136, 140,
142 | 3eqtr2i 2770 | . . . . . . . . . . . . . . . . 17
⊢ (π /
(2 · π)) = (1 / 2) | 
| 144 |  | halflt1 12485 | . . . . . . . . . . . . . . . . 17
⊢ (1 / 2)
< 1 | 
| 145 | 143, 144 | eqbrtri 5163 | . . . . . . . . . . . . . . . 16
⊢ (π /
(2 · π)) < 1 | 
| 146 | 145 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (π / (2 · π))
< 1) | 
| 147 | 132, 133,
122, 146 | ltadd2dd 11421 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 ·
π))) < ((𝑌 / (2
· π)) + 1)) | 
| 148 | 131, 147 | eqbrtrd 5164 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + π) / (2 · π)) < ((𝑌 / (2 · π)) +
1)) | 
| 149 | 129, 148 | eqbrtrid 5177 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) | 
| 150 | 149 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) | 
| 151 | 55, 121, 125, 128, 150 | lttrd 11423 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) | 
| 152 | 151 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) +
1)) | 
| 153 |  | btwnnz 12696 | . . . . . . . . 9
⊢ (((𝑌 / (2 · π)) ∈
ℤ ∧ (𝑌 / (2
· π)) < (𝑦 /
(2 · π)) ∧ (𝑦
/ (2 · π)) < ((𝑌 / (2 · π)) + 1)) → ¬
(𝑦 / (2 · π))
∈ ℤ) | 
| 154 | 104, 118,
152, 153 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈
ℤ) | 
| 155 | 103, 154 | pm2.61dan 812 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈
ℤ) | 
| 156 | 33, 155 | eqneltrd 2860 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈
ℤ) | 
| 157 | 25 | halfcld 12513 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ) | 
| 158 |  | sineq0 26567 | . . . . . . 7
⊢ ((𝑦 / 2) ∈ ℂ →
((sin‘(𝑦 / 2)) = 0
↔ ((𝑦 / 2) / π)
∈ ℤ)) | 
| 159 | 157, 158 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈
ℤ)) | 
| 160 | 156, 159 | mtbird 325 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0) | 
| 161 | 160 | neqned 2946 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0) | 
| 162 | 33 | oveq1d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑦 / 2) / π) + (1 / 2)) = ((𝑦 / (2 · π)) + (1 /
2))) | 
| 163 | 42 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈
ℤ) | 
| 164 | 1 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 = (𝑌 − π)) | 
| 165 | 164 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + π) = ((𝑌 − π) + π)) | 
| 166 | 60, 130 | npcand 11625 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − π) + π) = 𝑌) | 
| 167 | 165, 166 | eqtr2d 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 = (𝐴 + π)) | 
| 168 | 167 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 + π) / (2 ·
π))) | 
| 169 | 48 | recnd 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 170 | 169, 130,
56, 53 | divdird 12082 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + π) / (2 · π)) = ((𝐴 / (2 · π)) + (π /
(2 · π)))) | 
| 171 | 130 | mulridd 11279 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (π · 1) =
π) | 
| 172 | 171 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (𝜑 → π = (π ·
1)) | 
| 173 |  | 2cnd 12345 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) | 
| 174 | 173, 130 | mulcomd 11283 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · π) = (π
· 2)) | 
| 175 | 172, 174 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝜑 → (π / (2 · π))
= ((π · 1) / (π · 2))) | 
| 176 |  | 1cnd 11257 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℂ) | 
| 177 | 29 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 0) | 
| 178 | 31 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → π ≠
0) | 
| 179 | 176, 173,
130, 177, 178 | divcan5d 12070 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((π · 1) / (π
· 2)) = (1 / 2)) | 
| 180 | 175, 179 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → (π / (2 · π))
= (1 / 2)) | 
| 181 | 180 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 / (2 · π)) + (π / (2 ·
π))) = ((𝐴 / (2 ·
π)) + (1 / 2))) | 
| 182 | 168, 170,
181 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 /
2))) | 
| 183 | 182 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 /
2))) | 
| 184 | 124 | rehalfcld 12515 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈
ℝ) | 
| 185 | 50, 55, 184, 87 | ltadd1dd 11875 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐴 / (2 · π)) + (1 / 2)) <
((𝑦 / (2 · π)) +
(1 / 2))) | 
| 186 | 183, 185 | eqbrtrd 5164 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 /
2))) | 
| 187 | 55, 121, 184, 128 | ltadd1dd 11875 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝐵 / (2 · π)) + (1 /
2))) | 
| 188 | 129 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 / (2 · π)) = ((𝑌 + π) / (2 ·
π))) | 
| 189 | 188 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = (((𝑌 + π) / (2 · π)) +
(1 / 2))) | 
| 190 | 180 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 ·
π))) = ((𝑌 / (2 ·
π)) + (1 / 2))) | 
| 191 | 131, 190 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (1 /
2))) | 
| 192 | 191 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝑌 + π) / (2 · π)) + (1 / 2)) =
(((𝑌 / (2 · π)) +
(1 / 2)) + (1 / 2))) | 
| 193 | 176 | halfcld 12513 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℂ) | 
| 194 | 95, 193, 193 | addassd 11284 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2))
= ((𝑌 / (2 · π))
+ ((1 / 2) + (1 / 2)))) | 
| 195 | 176 | 2halvesd 12514 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((1 / 2) + (1 / 2)) =
1) | 
| 196 | 195 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2)))
= ((𝑌 / (2 · π))
+ 1)) | 
| 197 | 194, 196 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2))
= ((𝑌 / (2 · π))
+ 1)) | 
| 198 | 189, 192,
197 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) +
1)) | 
| 199 | 198 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) +
1)) | 
| 200 | 187, 199 | breqtrd 5168 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) +
1)) | 
| 201 |  | btwnnz 12696 | . . . . . . . 8
⊢ (((𝑌 / (2 · π)) ∈
ℤ ∧ (𝑌 / (2
· π)) < ((𝑦 /
(2 · π)) + (1 / 2)) ∧ ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1))
→ ¬ ((𝑦 / (2
· π)) + (1 / 2)) ∈ ℤ) | 
| 202 | 163, 186,
200, 201 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈
ℤ) | 
| 203 | 162, 202 | eqneltrd 2860 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (((𝑦 / 2) / π) + (1 / 2)) ∈
ℤ) | 
| 204 |  | coseq0 45884 | . . . . . . 7
⊢ ((𝑦 / 2) ∈ ℂ →
((cos‘(𝑦 / 2)) = 0
↔ (((𝑦 / 2) / π) +
(1 / 2)) ∈ ℤ)) | 
| 205 | 157, 204 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((cos‘(𝑦 / 2)) = 0 ↔ (((𝑦 / 2) / π) + (1 / 2)) ∈
ℤ)) | 
| 206 | 203, 205 | mtbird 325 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (cos‘(𝑦 / 2)) = 0) | 
| 207 | 206 | neqned 2946 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) | 
| 208 | 161, 207 | jca 511 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)) | 
| 209 | 208 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)) | 
| 210 | 21, 209 | jca 511 | 1
⊢ (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠
0))) |