# Metamath Proof Explorer

## Theorem pilem3

Description: Lemma for pire , pigt2lt4 and sinpi . Existence part. (Contributed by Paul Chapman, 23-Jan-2008) (Proof shortened by Mario Carneiro, 18-Jun-2014) (Revised by AV, 14-Sep-2020) (Proof shortened by BJ, 30-Jun-2022)

Ref Expression
Assertion pilem3 ${⊢}\left(\mathrm{\pi }\in \left(2,4\right)\wedge \mathrm{sin}\mathrm{\pi }=0\right)$

### Proof

Step Hyp Ref Expression
1 2re ${⊢}2\in ℝ$
2 1 a1i ${⊢}\top \to 2\in ℝ$
3 4re ${⊢}4\in ℝ$
4 3 a1i ${⊢}\top \to 4\in ℝ$
5 0red ${⊢}\top \to 0\in ℝ$
6 2lt4 ${⊢}2<4$
7 6 a1i ${⊢}\top \to 2<4$
8 iccssre ${⊢}\left(2\in ℝ\wedge 4\in ℝ\right)\to \left[2,4\right]\subseteq ℝ$
9 1 3 8 mp2an ${⊢}\left[2,4\right]\subseteq ℝ$
10 ax-resscn ${⊢}ℝ\subseteq ℂ$
11 9 10 sstri ${⊢}\left[2,4\right]\subseteq ℂ$
12 11 a1i ${⊢}\top \to \left[2,4\right]\subseteq ℂ$
13 sincn ${⊢}\mathrm{sin}:ℂ\underset{cn}{⟶}ℂ$
14 13 a1i ${⊢}\top \to \mathrm{sin}:ℂ\underset{cn}{⟶}ℂ$
15 9 sseli ${⊢}{y}\in \left[2,4\right]\to {y}\in ℝ$
16 15 resincld ${⊢}{y}\in \left[2,4\right]\to \mathrm{sin}{y}\in ℝ$
17 16 adantl ${⊢}\left(\top \wedge {y}\in \left[2,4\right]\right)\to \mathrm{sin}{y}\in ℝ$
18 sin4lt0 ${⊢}\mathrm{sin}4<0$
19 sincos2sgn ${⊢}\left(0<\mathrm{sin}2\wedge \mathrm{cos}2<0\right)$
20 19 simpli ${⊢}0<\mathrm{sin}2$
21 18 20 pm3.2i ${⊢}\left(\mathrm{sin}4<0\wedge 0<\mathrm{sin}2\right)$
22 21 a1i ${⊢}\top \to \left(\mathrm{sin}4<0\wedge 0<\mathrm{sin}2\right)$
23 2 4 5 7 12 14 17 22 ivth2 ${⊢}\top \to \exists {x}\in \left(2,4\right)\phantom{\rule{.4em}{0ex}}\mathrm{sin}{x}=0$
24 23 mptru ${⊢}\exists {x}\in \left(2,4\right)\phantom{\rule{.4em}{0ex}}\mathrm{sin}{x}=0$
25 df-pi ${⊢}\mathrm{\pi }=sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$
26 inss1 ${⊢}{ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq {ℝ}^{+}$
27 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
28 26 27 sstri ${⊢}{ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ$
29 0re ${⊢}0\in ℝ$
30 26 sseli ${⊢}{z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\to {z}\in {ℝ}^{+}$
31 30 rpge0d ${⊢}{z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\to 0\le {z}$
32 31 rgen ${⊢}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}0\le {z}$
33 breq1 ${⊢}{y}=0\to \left({y}\le {z}↔0\le {z}\right)$
34 33 ralbidv ${⊢}{y}=0\to \left(\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}↔\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}0\le {z}\right)$
35 34 rspcev ${⊢}\left(0\in ℝ\wedge \forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}0\le {z}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}$
36 29 32 35 mp2an ${⊢}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}$
37 elioore ${⊢}{x}\in \left(2,4\right)\to {x}\in ℝ$
38 37 adantr ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {x}\in ℝ$
39 0red ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to 0\in ℝ$
40 1 a1i ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to 2\in ℝ$
41 2pos ${⊢}0<2$
42 41 a1i ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to 0<2$
43 eliooord ${⊢}{x}\in \left(2,4\right)\to \left(2<{x}\wedge {x}<4\right)$
44 43 simpld ${⊢}{x}\in \left(2,4\right)\to 2<{x}$
45 44 adantr ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to 2<{x}$
46 39 40 38 42 45 lttrd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to 0<{x}$
47 38 46 elrpd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {x}\in {ℝ}^{+}$
48 simpr ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{sin}{x}=0$
49 pilem1 ${⊢}{x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)↔\left({x}\in {ℝ}^{+}\wedge \mathrm{sin}{x}=0\right)$
50 47 48 49 sylanbrc ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)$
51 infrelb ${⊢}\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}\wedge {x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le {x}$
52 28 36 50 51 mp3an12i ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le {x}$
53 25 52 eqbrtrid ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }\le {x}$
54 simpll ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to {x}\in \left(2,4\right)$
55 simpr ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)$
56 pilem1 ${⊢}{y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)↔\left({y}\in {ℝ}^{+}\wedge \mathrm{sin}{y}=0\right)$
57 55 56 sylib ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to \left({y}\in {ℝ}^{+}\wedge \mathrm{sin}{y}=0\right)$
58 57 simpld ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to {y}\in {ℝ}^{+}$
59 simplr ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to \mathrm{sin}{x}=0$
60 57 simprd ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to \mathrm{sin}{y}=0$
61 54 58 59 60 pilem2 ${⊢}\left(\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\wedge {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\right)\to \frac{\mathrm{\pi }+{x}}{2}\le {y}$
62 61 ralrimiva ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}\frac{\mathrm{\pi }+{x}}{2}\le {y}$
63 28 a1i ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ$
64 50 ne0d ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing$
65 36 a1i ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}$
66 infrecl ${⊢}\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}\right)\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$
67 28 36 66 mp3an13 ${⊢}{ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing \to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$
68 64 67 syl ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$
69 25 68 eqeltrid ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }\in ℝ$
70 69 38 readdcld ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }+{x}\in ℝ$
71 70 rehalfcld ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \frac{\mathrm{\pi }+{x}}{2}\in ℝ$
72 infregelb ${⊢}\left(\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{y}\le {z}\right)\wedge \frac{\mathrm{\pi }+{x}}{2}\in ℝ\right)\to \left(\frac{\mathrm{\pi }+{x}}{2}\le sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)↔\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}\frac{\mathrm{\pi }+{x}}{2}\le {y}\right)$
73 63 64 65 71 72 syl31anc ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \left(\frac{\mathrm{\pi }+{x}}{2}\le sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)↔\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}\frac{\mathrm{\pi }+{x}}{2}\le {y}\right)$
74 62 73 mpbird ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \frac{\mathrm{\pi }+{x}}{2}\le sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$
75 74 25 breqtrrdi ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \frac{\mathrm{\pi }+{x}}{2}\le \mathrm{\pi }$
76 69 recnd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }\in ℂ$
77 38 recnd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {x}\in ℂ$
78 76 77 addcomd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }+{x}={x}+\mathrm{\pi }$
79 78 oveq1d ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \frac{\mathrm{\pi }+{x}}{2}=\frac{{x}+\mathrm{\pi }}{2}$
80 79 breq1d ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \left(\frac{\mathrm{\pi }+{x}}{2}\le \mathrm{\pi }↔\frac{{x}+\mathrm{\pi }}{2}\le \mathrm{\pi }\right)$
81 avgle2 ${⊢}\left({x}\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left({x}\le \mathrm{\pi }↔\frac{{x}+\mathrm{\pi }}{2}\le \mathrm{\pi }\right)$
82 38 69 81 syl2anc ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \left({x}\le \mathrm{\pi }↔\frac{{x}+\mathrm{\pi }}{2}\le \mathrm{\pi }\right)$
83 80 82 bitr4d ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \left(\frac{\mathrm{\pi }+{x}}{2}\le \mathrm{\pi }↔{x}\le \mathrm{\pi }\right)$
84 75 83 mpbid ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {x}\le \mathrm{\pi }$
85 69 38 letri3d ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \left(\mathrm{\pi }={x}↔\left(\mathrm{\pi }\le {x}\wedge {x}\le \mathrm{\pi }\right)\right)$
86 53 84 85 mpbir2and ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }={x}$
87 simpl ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to {x}\in \left(2,4\right)$
88 86 87 eqeltrd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{\pi }\in \left(2,4\right)$
89 86 fveq2d ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{sin}\mathrm{\pi }=\mathrm{sin}{x}$
90 89 48 eqtrd ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \mathrm{sin}\mathrm{\pi }=0$
91 88 90 jca ${⊢}\left({x}\in \left(2,4\right)\wedge \mathrm{sin}{x}=0\right)\to \left(\mathrm{\pi }\in \left(2,4\right)\wedge \mathrm{sin}\mathrm{\pi }=0\right)$
92 91 rexlimiva ${⊢}\exists {x}\in \left(2,4\right)\phantom{\rule{.4em}{0ex}}\mathrm{sin}{x}=0\to \left(\mathrm{\pi }\in \left(2,4\right)\wedge \mathrm{sin}\mathrm{\pi }=0\right)$
93 24 92 ax-mp ${⊢}\left(\mathrm{\pi }\in \left(2,4\right)\wedge \mathrm{sin}\mathrm{\pi }=0\right)$