Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dirkercncflem1 Structured version   Visualization version   GIF version

Theorem dirkercncflem1 40799
Description: If 𝑌 is a multiple of π then it belongs to an open inerval (𝐴(,)𝐵) such that for any other point 𝑦 in the interval, cos y/2 and sin y/2 are nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
dirkercncflem1.a 𝐴 = (𝑌 − π)
dirkercncflem1.b 𝐵 = (𝑌 + π)
dirkercncflem1.y (𝜑𝑌 ∈ ℝ)
dirkercncflem1.ymod0 (𝜑 → (𝑌 mod (2 · π)) = 0)
Assertion
Ref Expression
dirkercncflem1 (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)))
Distinct variable groups:   𝑦,𝑌   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑦)

Proof of Theorem dirkercncflem1
StepHypRef Expression
1 dirkercncflem1.a . . . 4 𝐴 = (𝑌 − π)
2 dirkercncflem1.y . . . . . 6 (𝜑𝑌 ∈ ℝ)
3 pire 24425 . . . . . . 7 π ∈ ℝ
43a1i 11 . . . . . 6 (𝜑 → π ∈ ℝ)
52, 4resubcld 10743 . . . . 5 (𝜑 → (𝑌 − π) ∈ ℝ)
65rexrd 10374 . . . 4 (𝜑 → (𝑌 − π) ∈ ℝ*)
71, 6syl5eqel 2889 . . 3 (𝜑𝐴 ∈ ℝ*)
8 dirkercncflem1.b . . . 4 𝐵 = (𝑌 + π)
92, 4readdcld 10354 . . . . 5 (𝜑 → (𝑌 + π) ∈ ℝ)
109rexrd 10374 . . . 4 (𝜑 → (𝑌 + π) ∈ ℝ*)
118, 10syl5eqel 2889 . . 3 (𝜑𝐵 ∈ ℝ*)
12 pipos 24427 . . . . . 6 0 < π
13 ltsubpos 10805 . . . . . 6 ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (0 < π ↔ (𝑌 − π) < 𝑌))
1412, 13mpbii 224 . . . . 5 ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌 − π) < 𝑌)
154, 2, 14syl2anc 575 . . . 4 (𝜑 → (𝑌 − π) < 𝑌)
161, 15syl5eqbr 4879 . . 3 (𝜑𝐴 < 𝑌)
17 ltaddpos 10803 . . . . . 6 ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (0 < π ↔ 𝑌 < (𝑌 + π)))
1812, 17mpbii 224 . . . . 5 ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 < (𝑌 + π))
194, 2, 18syl2anc 575 . . . 4 (𝜑𝑌 < (𝑌 + π))
2019, 8syl6breqr 4886 . . 3 (𝜑𝑌 < 𝐵)
217, 11, 2, 16, 20eliood 40204 . 2 (𝜑𝑌 ∈ (𝐴(,)𝐵))
22 eldifi 3931 . . . . . . . . . . 11 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
2322elioored 40256 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℝ)
2423adantl 469 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
2524recnd 10353 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
26 2cnd 11377 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
27 picn 24426 . . . . . . . . 9 π ∈ ℂ
2827a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
29 2ne0 11396 . . . . . . . . 9 2 ≠ 0
3029a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
313, 12gt0ne0ii 10849 . . . . . . . . 9 π ≠ 0
3231a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
3325, 26, 28, 30, 32divdiv1d 11117 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34 dirkercncflem1.ymod0 . . . . . . . . . . . 12 (𝜑 → (𝑌 mod (2 · π)) = 0)
35 2rp 12051 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
3635a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ+)
37 pirp 24428 . . . . . . . . . . . . . . 15 π ∈ ℝ+
3837a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ∈ ℝ+)
3936, 38rpmulcld 12102 . . . . . . . . . . . . 13 (𝜑 → (2 · π) ∈ ℝ+)
40 mod0 12899 . . . . . . . . . . . . 13 ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
412, 39, 40syl2anc 575 . . . . . . . . . . . 12 (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
4234, 41mpbid 223 . . . . . . . . . . 11 (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
43 peano2zm 11686 . . . . . . . . . . 11 ((𝑌 / (2 · π)) ∈ ℤ → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
4442, 43syl 17 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
4544ad2antrr 708 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
4644zred 11748 . . . . . . . . . . . 12 (𝜑 → ((𝑌 / (2 · π)) − 1) ∈ ℝ)
4746adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) ∈ ℝ)
481, 5syl5eqel 2889 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
4948, 39rerpdivcld 12117 . . . . . . . . . . . 12 (𝜑 → (𝐴 / (2 · π)) ∈ ℝ)
5049adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) ∈ ℝ)
5139rpred 12086 . . . . . . . . . . . . 13 (𝜑 → (2 · π) ∈ ℝ)
5251adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
5339rpne0d 12091 . . . . . . . . . . . . 13 (𝜑 → (2 · π) ≠ 0)
5453adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ≠ 0)
5524, 52, 54redivcld 11138 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) ∈ ℝ)
5651recnd 10353 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · π) ∈ ℂ)
5756, 53dividd 11084 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 · π) / (2 · π)) = 1)
5857eqcomd 2812 . . . . . . . . . . . . . . 15 (𝜑 → 1 = ((2 · π) / (2 · π)))
5958oveq2d 6890 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 / (2 · π)) − ((2 · π) / (2 · π))))
602recnd 10353 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℂ)
6160, 56, 56, 53divsubdird 11125 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (2 · π)) / (2 · π)) = ((𝑌 / (2 · π)) − ((2 · π) / (2 · π))))
6259, 61eqtr4d 2843 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 − (2 · π)) / (2 · π)))
632, 51resubcld 10743 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (2 · π)) ∈ ℝ)
6427mulid2i 10330 . . . . . . . . . . . . . . . . . . 19 (1 · π) = π
6564eqcomi 2815 . . . . . . . . . . . . . . . . . 18 π = (1 · π)
66 1lt2 11470 . . . . . . . . . . . . . . . . . . 19 1 < 2
67 1re 10325 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ
68 2re 11374 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
6967, 68, 3, 12ltmul1ii 11237 . . . . . . . . . . . . . . . . . . 19 (1 < 2 ↔ (1 · π) < (2 · π))
7066, 69mpbi 221 . . . . . . . . . . . . . . . . . 18 (1 · π) < (2 · π)
7165, 70eqbrtri 4865 . . . . . . . . . . . . . . . . 17 π < (2 · π)
7271a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → π < (2 · π))
734, 51, 2, 72ltsub2dd 10925 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌 − (2 · π)) < (𝑌 − π))
7473, 1syl6breqr 4886 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (2 · π)) < 𝐴)
7563, 48, 39, 74ltdiv1dd 12143 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 − (2 · π)) / (2 · π)) < (𝐴 / (2 · π)))
7662, 75eqbrtrd 4866 . . . . . . . . . . . 12 (𝜑 → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 · π)))
7776adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 · π)))
7848adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈ ℝ)
7939adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ+)
8022adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ (𝐴(,)𝐵))
817adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈ ℝ*)
8211adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ*)
83 elioo2 12434 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦𝑦 < 𝐵)))
8481, 82, 83syl2anc 575 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦𝑦 < 𝐵)))
8580, 84mpbid 223 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦𝑦 < 𝐵))
8685simp2d 1166 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 < 𝑦)
8778, 24, 79, 86ltdiv1dd 12143 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) < (𝑦 / (2 · π)))
8847, 50, 55, 77, 87lttrd 10483 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)))
8988adantr 468 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)))
9023ad2antlr 709 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 ∈ ℝ)
912ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑌 ∈ ℝ)
9239ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (2 · π) ∈ ℝ+)
93 simpr 473 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 < 𝑌)
9490, 91, 92, 93ltdiv1dd 12143 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (𝑌 / (2 · π)))
9560, 56, 53divcld 11086 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
9695adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℂ)
97 1cnd 10320 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
9896, 97npcand 10681 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑌 / (2 · π)) − 1) + 1) = (𝑌 / (2 · π)))
9998eqcomd 2812 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) + 1))
10099adantr 468 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) + 1))
10194, 100breqtrd 4870 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1) + 1))
102 btwnnz 11719 . . . . . . . . 9 ((((𝑌 / (2 · π)) − 1) ∈ ℤ ∧ ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
10345, 89, 101, 102syl3anc 1483 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
10442ad2antrr 708 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) ∈ ℤ)
1052ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 ∈ ℝ)
10624adantr 468 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑦 ∈ ℝ)
10779adantr 468 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (2 · π) ∈ ℝ+)
10824adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦𝑌) → 𝑦 ∈ ℝ)
1092ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦𝑌) → 𝑌 ∈ ℝ)
110 simpr 473 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦𝑌) → 𝑦𝑌)
111 eldifsni 4512 . . . . . . . . . . . . . . 15 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦𝑌)
112111necomd 3033 . . . . . . . . . . . . . 14 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑌𝑦)
113112ad2antlr 709 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦𝑌) → 𝑌𝑦)
114108, 109, 110, 113leneltd 10476 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦𝑌) → 𝑦 < 𝑌)
115114stoic1a 1852 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ 𝑦𝑌)
116105, 106ltnled 10469 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 < 𝑦 ↔ ¬ 𝑦𝑌))
117115, 116mpbird 248 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 < 𝑦)
118105, 106, 107, 117ltdiv1dd 12143 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) < (𝑦 / (2 · π)))
1198, 9syl5eqel 2889 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ)
120119, 39rerpdivcld 12117 . . . . . . . . . . . 12 (𝜑 → (𝐵 / (2 · π)) ∈ ℝ)
121120adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) ∈ ℝ)
1222, 39rerpdivcld 12117 . . . . . . . . . . . . 13 (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
123122adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℝ)
124 1red 10326 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℝ)
125123, 124readdcld 10354 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) + 1) ∈ ℝ)
126119adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ)
12785simp3d 1167 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 < 𝐵)
12824, 126, 79, 127ltdiv1dd 12143 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < (𝐵 / (2 · π)))
1298oveq1i 6884 . . . . . . . . . . . . 13 (𝐵 / (2 · π)) = ((𝑌 + π) / (2 · π))
13027a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → π ∈ ℂ)
13160, 130, 56, 53divdird 11124 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (π / (2 · π))))
1324, 39rerpdivcld 12117 . . . . . . . . . . . . . . 15 (𝜑 → (π / (2 · π)) ∈ ℝ)
133 1red 10326 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℝ)
134 2cn 11375 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℂ
135134, 27mulcomi 10333 . . . . . . . . . . . . . . . . . . 19 (2 · π) = (π · 2)
136135oveq2i 6885 . . . . . . . . . . . . . . . . . 18 (π / (2 · π)) = (π / (π · 2))
13727, 31pm3.2i 458 . . . . . . . . . . . . . . . . . . 19 (π ∈ ℂ ∧ π ≠ 0)
138 2cnne0 11509 . . . . . . . . . . . . . . . . . . 19 (2 ∈ ℂ ∧ 2 ≠ 0)
139 divdiv1 11021 . . . . . . . . . . . . . . . . . . 19 ((π ∈ ℂ ∧ (π ∈ ℂ ∧ π ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((π / π) / 2) = (π / (π · 2)))
14027, 137, 138, 139mp3an 1578 . . . . . . . . . . . . . . . . . 18 ((π / π) / 2) = (π / (π · 2))
14127, 31dividi 11043 . . . . . . . . . . . . . . . . . . 19 (π / π) = 1
142141oveq1i 6884 . . . . . . . . . . . . . . . . . 18 ((π / π) / 2) = (1 / 2)
143136, 140, 1423eqtr2i 2834 . . . . . . . . . . . . . . . . 17 (π / (2 · π)) = (1 / 2)
144 halflt1 11517 . . . . . . . . . . . . . . . . 17 (1 / 2) < 1
145143, 144eqbrtri 4865 . . . . . . . . . . . . . . . 16 (π / (2 · π)) < 1
146145a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (π / (2 · π)) < 1)
147132, 133, 122, 146ltadd2dd 10481 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 / (2 · π)) + (π / (2 · π))) < ((𝑌 / (2 · π)) + 1))
148131, 147eqbrtrd 4866 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 + π) / (2 · π)) < ((𝑌 / (2 · π)) + 1))
149129, 148syl5eqbr 4879 . . . . . . . . . . . 12 (𝜑 → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
150149adantr 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
15155, 121, 125, 128, 150lttrd 10483 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
152151adantr 468 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
153 btwnnz 11719 . . . . . . . . 9 (((𝑌 / (2 · π)) ∈ ℤ ∧ (𝑌 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
154104, 118, 152, 153syl3anc 1483 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
155103, 154pm2.61dan 838 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
15633, 155eqneltrd 2904 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
15725halfcld 11544 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
158 sineq0 24488 . . . . . . 7 ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
159157, 158syl 17 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
160156, 159mtbird 316 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
161160neqned 2985 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
16233oveq1d 6889 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑦 / 2) / π) + (1 / 2)) = ((𝑦 / (2 · π)) + (1 / 2)))
16342adantr 468 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℤ)
1641a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐴 = (𝑌 − π))
165164oveq1d 6889 . . . . . . . . . . . . 13 (𝜑 → (𝐴 + π) = ((𝑌 − π) + π))
16660, 130npcand 10681 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 − π) + π) = 𝑌)
167165, 166eqtr2d 2841 . . . . . . . . . . . 12 (𝜑𝑌 = (𝐴 + π))
168167oveq1d 6889 . . . . . . . . . . 11 (𝜑 → (𝑌 / (2 · π)) = ((𝐴 + π) / (2 · π)))
16948recnd 10353 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
170169, 130, 56, 53divdird 11124 . . . . . . . . . . 11 (𝜑 → ((𝐴 + π) / (2 · π)) = ((𝐴 / (2 · π)) + (π / (2 · π))))
171130mulid1d 10342 . . . . . . . . . . . . . . 15 (𝜑 → (π · 1) = π)
172171eqcomd 2812 . . . . . . . . . . . . . 14 (𝜑 → π = (π · 1))
173 2cnd 11377 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
174173, 130mulcomd 10346 . . . . . . . . . . . . . 14 (𝜑 → (2 · π) = (π · 2))
175172, 174oveq12d 6892 . . . . . . . . . . . . 13 (𝜑 → (π / (2 · π)) = ((π · 1) / (π · 2)))
176 1cnd 10320 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
17729a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ≠ 0)
17831a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ≠ 0)
179176, 173, 130, 177, 178divcan5d 11112 . . . . . . . . . . . . 13 (𝜑 → ((π · 1) / (π · 2)) = (1 / 2))
180175, 179eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → (π / (2 · π)) = (1 / 2))
181180oveq2d 6890 . . . . . . . . . . 11 (𝜑 → ((𝐴 / (2 · π)) + (π / (2 · π))) = ((𝐴 / (2 · π)) + (1 / 2)))
182168, 170, 1813eqtrd 2844 . . . . . . . . . 10 (𝜑 → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 / 2)))
183182adantr 468 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 / 2)))
184124rehalfcld 11546 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
18550, 55, 184, 87ltadd1dd 10923 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐴 / (2 · π)) + (1 / 2)) < ((𝑦 / (2 · π)) + (1 / 2)))
186183, 185eqbrtrd 4866 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 / 2)))
18755, 121, 184, 128ltadd1dd 10923 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝐵 / (2 · π)) + (1 / 2)))
188129a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐵 / (2 · π)) = ((𝑌 + π) / (2 · π)))
189188oveq1d 6889 . . . . . . . . . . 11 (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = (((𝑌 + π) / (2 · π)) + (1 / 2)))
190180oveq2d 6890 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 / (2 · π)) + (π / (2 · π))) = ((𝑌 / (2 · π)) + (1 / 2)))
191131, 190eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (1 / 2)))
192191oveq1d 6889 . . . . . . . . . . 11 (𝜑 → (((𝑌 + π) / (2 · π)) + (1 / 2)) = (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)))
193176halfcld 11544 . . . . . . . . . . . . 13 (𝜑 → (1 / 2) ∈ ℂ)
19495, 193, 193addassd 10347 . . . . . . . . . . . 12 (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)) = ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2))))
1951762halvesd 11545 . . . . . . . . . . . . 13 (𝜑 → ((1 / 2) + (1 / 2)) = 1)
196195oveq2d 6890 . . . . . . . . . . . 12 (𝜑 → ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2))) = ((𝑌 / (2 · π)) + 1))
197194, 196eqtrd 2840 . . . . . . . . . . 11 (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
198189, 192, 1973eqtrd 2844 . . . . . . . . . 10 (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
199198adantr 468 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
200187, 199breqtrd 4870 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1))
201 btwnnz 11719 . . . . . . . 8 (((𝑌 / (2 · π)) ∈ ℤ ∧ (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 / 2)) ∧ ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1)) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈ ℤ)
202163, 186, 200, 201syl3anc 1483 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈ ℤ)
203162, 202eqneltrd 2904 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ)
204 coseq0 40555 . . . . . . 7 ((𝑦 / 2) ∈ ℂ → ((cos‘(𝑦 / 2)) = 0 ↔ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ))
205157, 204syl 17 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((cos‘(𝑦 / 2)) = 0 ↔ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ))
206203, 205mtbird 316 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (cos‘(𝑦 / 2)) = 0)
207206neqned 2985 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
208161, 207jca 503 . . 3 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0))
209208ralrimiva 3154 . 2 (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0))
21021, 209jca 503 1 (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  cdif 3766  {csn 4370   class class class wbr 4844  cfv 6101  (class class class)co 6874  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226  *cxr 10358   < clt 10359  cle 10360  cmin 10551   / cdiv 10969  2c2 11356  cz 11643  +crp 12046  (,)cioo 12393   mod cmo 12892  sincsin 15014  cosccos 15015  πcpi 15017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-fi 8556  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-z 11644  df-dec 11760  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-ioo 12397  df-ioc 12398  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-fac 13281  df-bc 13310  df-hash 13338  df-shft 14030  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-limsup 14425  df-clim 14442  df-rlim 14443  df-sum 14640  df-ef 15018  df-sin 15020  df-cos 15021  df-pi 15023  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-hom 16177  df-cco 16178  df-rest 16288  df-topn 16289  df-0g 16307  df-gsum 16308  df-topgen 16309  df-pt 16310  df-prds 16313  df-xrs 16367  df-qtop 16372  df-imas 16373  df-xps 16375  df-mre 16451  df-mrc 16452  df-acs 16454  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-submnd 17541  df-mulg 17746  df-cntz 17951  df-cmn 18396  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-fbas 19951  df-fg 19952  df-cnfld 19955  df-top 20912  df-topon 20929  df-topsp 20951  df-bases 20964  df-cld 21037  df-ntr 21038  df-cls 21039  df-nei 21116  df-lp 21154  df-perf 21155  df-cn 21245  df-cnp 21246  df-haus 21333  df-tx 21579  df-hmeo 21772  df-fil 21863  df-fm 21955  df-flim 21956  df-flf 21957  df-xms 22338  df-ms 22339  df-tms 22340  df-cncf 22894  df-limc 23844  df-dv 23845
This theorem is referenced by:  dirkercncflem3  40801
  Copyright terms: Public domain W3C validator