# Metamath Proof Explorer

## Theorem pilem2

Description: Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 12-Jun-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses pilem2.1 ${⊢}{\phi }\to {A}\in \left(2,4\right)$
pilem2.2 ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
pilem2.3 ${⊢}{\phi }\to \mathrm{sin}{A}=0$
pilem2.4 ${⊢}{\phi }\to \mathrm{sin}{B}=0$
Assertion pilem2 ${⊢}{\phi }\to \frac{\mathrm{\pi }+{A}}{2}\le {B}$

### Proof

Step Hyp Ref Expression
1 pilem2.1 ${⊢}{\phi }\to {A}\in \left(2,4\right)$
2 pilem2.2 ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
3 pilem2.3 ${⊢}{\phi }\to \mathrm{sin}{A}=0$
4 pilem2.4 ${⊢}{\phi }\to \mathrm{sin}{B}=0$
5 df-pi ${⊢}\mathrm{\pi }=sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$
6 inss1 ${⊢}{ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq {ℝ}^{+}$
7 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
8 6 7 sstri ${⊢}{ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ$
9 8 a1i ${⊢}{\phi }\to {ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ$
10 0re ${⊢}0\in ℝ$
11 elinel1 ${⊢}{y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\to {y}\in {ℝ}^{+}$
12 11 rpge0d ${⊢}{y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\to 0\le {y}$
13 12 rgen ${⊢}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}0\le {y}$
14 breq1 ${⊢}{x}=0\to \left({x}\le {y}↔0\le {y}\right)$
15 14 ralbidv ${⊢}{x}=0\to \left(\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}0\le {y}\right)$
16 15 rspcev ${⊢}\left(0\in ℝ\wedge \forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}0\le {y}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}$
17 10 13 16 mp2an ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}$
18 17 a1i ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}$
19 2re ${⊢}2\in ℝ$
20 2 rpred ${⊢}{\phi }\to {B}\in ℝ$
21 remulcl ${⊢}\left(2\in ℝ\wedge {B}\in ℝ\right)\to 2{B}\in ℝ$
22 19 20 21 sylancr ${⊢}{\phi }\to 2{B}\in ℝ$
23 elioore ${⊢}{A}\in \left(2,4\right)\to {A}\in ℝ$
24 1 23 syl ${⊢}{\phi }\to {A}\in ℝ$
25 22 24 resubcld ${⊢}{\phi }\to 2{B}-{A}\in ℝ$
26 4re ${⊢}4\in ℝ$
27 26 a1i ${⊢}{\phi }\to 4\in ℝ$
28 eliooord ${⊢}{A}\in \left(2,4\right)\to \left(2<{A}\wedge {A}<4\right)$
29 1 28 syl ${⊢}{\phi }\to \left(2<{A}\wedge {A}<4\right)$
30 29 simprd ${⊢}{\phi }\to {A}<4$
31 2t2e4 ${⊢}2\cdot 2=4$
32 19 a1i ${⊢}{\phi }\to 2\in ℝ$
33 0red ${⊢}{\phi }\to 0\in ℝ$
34 2pos ${⊢}0<2$
35 34 a1i ${⊢}{\phi }\to 0<2$
36 29 simpld ${⊢}{\phi }\to 2<{A}$
37 33 32 24 35 36 lttrd ${⊢}{\phi }\to 0<{A}$
38 24 37 elrpd ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
39 pilem1 ${⊢}{A}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)↔\left({A}\in {ℝ}^{+}\wedge \mathrm{sin}{A}=0\right)$
40 38 3 39 sylanbrc ${⊢}{\phi }\to {A}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)$
41 40 ne0d ${⊢}{\phi }\to {ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing$
42 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 {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$
43 8 17 42 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 ℝ$
44 41 43 syl ${⊢}{\phi }\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$
45 pilem1 ${⊢}{x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)↔\left({x}\in {ℝ}^{+}\wedge \mathrm{sin}{x}=0\right)$
46 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
47 46 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℝ$
48 letric ${⊢}\left(2\in ℝ\wedge {x}\in ℝ\right)\to \left(2\le {x}\vee {x}\le 2\right)$
49 19 47 48 sylancr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(2\le {x}\vee {x}\le 2\right)$
50 49 ord ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(¬2\le {x}\to {x}\le 2\right)$
51 46 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {x}\le 2\right)\to {x}\in ℝ$
52 rpgt0 ${⊢}{x}\in {ℝ}^{+}\to 0<{x}$
53 52 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {x}\le 2\right)\to 0<{x}$
54 simpr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {x}\le 2\right)\to {x}\le 2$
55 0xr ${⊢}0\in {ℝ}^{*}$
56 elioc2 ${⊢}\left(0\in {ℝ}^{*}\wedge 2\in ℝ\right)\to \left({x}\in \left(0,2\right]↔\left({x}\in ℝ\wedge 0<{x}\wedge {x}\le 2\right)\right)$
57 55 19 56 mp2an ${⊢}{x}\in \left(0,2\right]↔\left({x}\in ℝ\wedge 0<{x}\wedge {x}\le 2\right)$
58 51 53 54 57 syl3anbrc ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {x}\le 2\right)\to {x}\in \left(0,2\right]$
59 sin02gt0 ${⊢}{x}\in \left(0,2\right]\to 0<\mathrm{sin}{x}$
60 58 59 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {x}\le 2\right)\to 0<\mathrm{sin}{x}$
61 60 gt0ne0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {x}\le 2\right)\to \mathrm{sin}{x}\ne 0$
62 61 ex ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left({x}\le 2\to \mathrm{sin}{x}\ne 0\right)$
63 50 62 syld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(¬2\le {x}\to \mathrm{sin}{x}\ne 0\right)$
64 63 necon4bd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\mathrm{sin}{x}=0\to 2\le {x}\right)$
65 64 expimpd ${⊢}{\phi }\to \left(\left({x}\in {ℝ}^{+}\wedge \mathrm{sin}{x}=0\right)\to 2\le {x}\right)$
66 45 65 syl5bi ${⊢}{\phi }\to \left({x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\to 2\le {x}\right)$
67 66 ralrimiv ${⊢}{\phi }\to \forall {x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}2\le {x}$
68 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 {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge 2\in ℝ\right)\to \left(2\le sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)↔\forall {x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}2\le {x}\right)$
69 9 41 18 32 68 syl31anc ${⊢}{\phi }\to \left(2\le sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)↔\forall {x}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}2\le {x}\right)$
70 67 69 mpbird ${⊢}{\phi }\to 2\le sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$
71 pilem1 ${⊢}{B}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)↔\left({B}\in {ℝ}^{+}\wedge \mathrm{sin}{B}=0\right)$
72 2 4 71 sylanbrc ${⊢}{\phi }\to {B}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)$
73 infrelb ${⊢}\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {B}\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 {B}$
74 9 18 72 73 syl3anc ${⊢}{\phi }\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le {B}$
75 32 44 20 70 74 letrd ${⊢}{\phi }\to 2\le {B}$
76 19 34 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
77 76 a1i ${⊢}{\phi }\to \left(2\in ℝ\wedge 0<2\right)$
78 lemul2 ${⊢}\left(2\in ℝ\wedge {B}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(2\le {B}↔2\cdot 2\le 2{B}\right)$
79 32 20 77 78 syl3anc ${⊢}{\phi }\to \left(2\le {B}↔2\cdot 2\le 2{B}\right)$
80 75 79 mpbid ${⊢}{\phi }\to 2\cdot 2\le 2{B}$
81 31 80 eqbrtrrid ${⊢}{\phi }\to 4\le 2{B}$
82 24 27 22 30 81 ltletrd ${⊢}{\phi }\to {A}<2{B}$
83 24 22 posdifd ${⊢}{\phi }\to \left({A}<2{B}↔0<2{B}-{A}\right)$
84 82 83 mpbid ${⊢}{\phi }\to 0<2{B}-{A}$
85 25 84 elrpd ${⊢}{\phi }\to 2{B}-{A}\in {ℝ}^{+}$
86 22 recnd ${⊢}{\phi }\to 2{B}\in ℂ$
87 24 recnd ${⊢}{\phi }\to {A}\in ℂ$
88 sinsub ${⊢}\left(2{B}\in ℂ\wedge {A}\in ℂ\right)\to \mathrm{sin}\left(2{B}-{A}\right)=\mathrm{sin}2{B}\mathrm{cos}{A}-\mathrm{cos}2{B}\mathrm{sin}{A}$
89 86 87 88 syl2anc ${⊢}{\phi }\to \mathrm{sin}\left(2{B}-{A}\right)=\mathrm{sin}2{B}\mathrm{cos}{A}-\mathrm{cos}2{B}\mathrm{sin}{A}$
90 20 recnd ${⊢}{\phi }\to {B}\in ℂ$
91 sin2t ${⊢}{B}\in ℂ\to \mathrm{sin}2{B}=2\mathrm{sin}{B}\mathrm{cos}{B}$
92 90 91 syl ${⊢}{\phi }\to \mathrm{sin}2{B}=2\mathrm{sin}{B}\mathrm{cos}{B}$
93 4 oveq1d ${⊢}{\phi }\to \mathrm{sin}{B}\mathrm{cos}{B}=0\cdot \mathrm{cos}{B}$
94 90 coscld ${⊢}{\phi }\to \mathrm{cos}{B}\in ℂ$
95 94 mul02d ${⊢}{\phi }\to 0\cdot \mathrm{cos}{B}=0$
96 93 95 eqtrd ${⊢}{\phi }\to \mathrm{sin}{B}\mathrm{cos}{B}=0$
97 96 oveq2d ${⊢}{\phi }\to 2\mathrm{sin}{B}\mathrm{cos}{B}=2\cdot 0$
98 2t0e0 ${⊢}2\cdot 0=0$
99 97 98 syl6eq ${⊢}{\phi }\to 2\mathrm{sin}{B}\mathrm{cos}{B}=0$
100 92 99 eqtrd ${⊢}{\phi }\to \mathrm{sin}2{B}=0$
101 100 oveq1d ${⊢}{\phi }\to \mathrm{sin}2{B}\mathrm{cos}{A}=0\cdot \mathrm{cos}{A}$
102 87 coscld ${⊢}{\phi }\to \mathrm{cos}{A}\in ℂ$
103 102 mul02d ${⊢}{\phi }\to 0\cdot \mathrm{cos}{A}=0$
104 101 103 eqtrd ${⊢}{\phi }\to \mathrm{sin}2{B}\mathrm{cos}{A}=0$
105 3 oveq2d ${⊢}{\phi }\to \mathrm{cos}2{B}\mathrm{sin}{A}=\mathrm{cos}2{B}\cdot 0$
106 86 coscld ${⊢}{\phi }\to \mathrm{cos}2{B}\in ℂ$
107 106 mul01d ${⊢}{\phi }\to \mathrm{cos}2{B}\cdot 0=0$
108 105 107 eqtrd ${⊢}{\phi }\to \mathrm{cos}2{B}\mathrm{sin}{A}=0$
109 104 108 oveq12d ${⊢}{\phi }\to \mathrm{sin}2{B}\mathrm{cos}{A}-\mathrm{cos}2{B}\mathrm{sin}{A}=0-0$
110 0m0e0 ${⊢}0-0=0$
111 109 110 syl6eq ${⊢}{\phi }\to \mathrm{sin}2{B}\mathrm{cos}{A}-\mathrm{cos}2{B}\mathrm{sin}{A}=0$
112 89 111 eqtrd ${⊢}{\phi }\to \mathrm{sin}\left(2{B}-{A}\right)=0$
113 pilem1 ${⊢}2{B}-{A}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)↔\left(2{B}-{A}\in {ℝ}^{+}\wedge \mathrm{sin}\left(2{B}-{A}\right)=0\right)$
114 85 112 113 sylanbrc ${⊢}{\phi }\to 2{B}-{A}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)$
115 infrelb ${⊢}\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right]\right)\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge 2{B}-{A}\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 2{B}-{A}$
116 9 18 114 115 syl3anc ${⊢}{\phi }\to sup\left({ℝ}^{+}\cap {\mathrm{sin}}^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le 2{B}-{A}$
117 5 116 eqbrtrid ${⊢}{\phi }\to \mathrm{\pi }\le 2{B}-{A}$
118 5 44 eqeltrid ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
119 leaddsub ${⊢}\left(\mathrm{\pi }\in ℝ\wedge {A}\in ℝ\wedge 2{B}\in ℝ\right)\to \left(\mathrm{\pi }+{A}\le 2{B}↔\mathrm{\pi }\le 2{B}-{A}\right)$
120 118 24 22 119 syl3anc ${⊢}{\phi }\to \left(\mathrm{\pi }+{A}\le 2{B}↔\mathrm{\pi }\le 2{B}-{A}\right)$
121 117 120 mpbird ${⊢}{\phi }\to \mathrm{\pi }+{A}\le 2{B}$
122 118 24 readdcld ${⊢}{\phi }\to \mathrm{\pi }+{A}\in ℝ$
123 ledivmul ${⊢}\left(\mathrm{\pi }+{A}\in ℝ\wedge {B}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{\mathrm{\pi }+{A}}{2}\le {B}↔\mathrm{\pi }+{A}\le 2{B}\right)$
124 122 20 77 123 syl3anc ${⊢}{\phi }\to \left(\frac{\mathrm{\pi }+{A}}{2}\le {B}↔\mathrm{\pi }+{A}\le 2{B}\right)$
125 121 124 mpbird ${⊢}{\phi }\to \frac{\mathrm{\pi }+{A}}{2}\le {B}$