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 \sin A=0$$
	pilem2.4	$$⊢\phi \to \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 \sin A=0$$
4		pilem2.4	$$⊢\phi \to \sin B=0$$
5		df-pi	$$⊢\mathrm{\pi }=sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$$
6		inss1	$$⊢{ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq {ℝ}^{+}$$
7		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
8	6 7	sstri	$$⊢{ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq ℝ$$
9	8	a1i	$$⊢\phi \to {ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq ℝ$$
10		0re	$$⊢0\in ℝ$$
11		elinel1	$$⊢y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\to y\in {ℝ}^{+}$$
12	11	rpge0d	$$⊢y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\to 0\le y$$
13	12	rgen	$$⊢\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)0\le y$$
14		breq1	$$⊢x=0\to \left(x\le y\leftrightarrow 0\le y\right)$$
15	14	ralbidv	$$⊢x=0\to \left(\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y\leftrightarrow \forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)0\le y\right)$$
16	15	rspcev	$$⊢\left(0\in ℝ\wedge \forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)0\le y\right)\to \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y$$
17	10 13 16	mp2an	$$⊢\exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y$$
18	17	a1i	$$⊢\phi \to \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y$$
19		2re	$$⊢2\in ℝ$$
20	2	rpred	$$⊢\phi \to B\in ℝ$$
21		remulcl	$$⊢\left(2\in ℝ\wedge B\in ℝ\right)\to 2B\in ℝ$$
22	19 20 21	sylancr	$$⊢\phi \to 2B\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 2B-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 {\sin }^{-1}\left[\left\{0\right\}\right]\right)\leftrightarrow \left(A\in {ℝ}^{+}\wedge \sin A=0\right)$$
40	38 3 39	sylanbrc	$$⊢\phi \to A\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)$$
41	40	ne0d	$$⊢\phi \to {ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\ne \varnothing$$
42		infrecl	$$⊢\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\ne \varnothing \wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y\right)\to sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$$
43	8 17 42	mp3an13	$$⊢{ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\ne \varnothing \to sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$$
44	41 43	syl	$$⊢\phi \to sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\in ℝ$$
45		pilem1	$$⊢x\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\leftrightarrow \left(x\in {ℝ}^{+}\wedge \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(\neg 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]\leftrightarrow \left(x\in ℝ\wedge 0<x\wedge x\le 2\right)\right)$$
57	55 19 56	mp2an	$$⊢x\in \left(0,2\right]\leftrightarrow \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<\sin x$$
60	58 59	syl	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge x\le 2\right)\to 0<\sin x$$
61	60	gt0ne0d	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge x\le 2\right)\to \sin x\ne 0$$
62	61	ex	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left(x\le 2\to \sin x\ne 0\right)$$
63	50 62	syld	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left(\neg 2\le x\to \sin x\ne 0\right)$$
64	63	necon4bd	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left(\sin x=0\to 2\le x\right)$$
65	64	expimpd	$$⊢\phi \to \left(\left(x\in {ℝ}^{+}\wedge \sin x=0\right)\to 2\le x\right)$$
66	45 65	biimtrid	$$⊢\phi \to \left(x\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\to 2\le x\right)$$
67	66	ralrimiv	$$⊢\phi \to \forall x\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)2\le x$$
68		infregelb	$$⊢\left(\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\ne \varnothing \wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y\right)\wedge 2\in ℝ\right)\to \left(2\le sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\leftrightarrow \forall x\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)2\le x\right)$$
69	9 41 18 32 68	syl31anc	$$⊢\phi \to \left(2\le sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\leftrightarrow \forall x\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)2\le x\right)$$
70	67 69	mpbird	$$⊢\phi \to 2\le sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)$$
71		pilem1	$$⊢B\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\leftrightarrow \left(B\in {ℝ}^{+}\wedge \sin B=0\right)$$
72	2 4 71	sylanbrc	$$⊢\phi \to B\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)$$
73		infrelb	$$⊢\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y\wedge B\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\right)\to sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le B$$
74	9 18 72 73	syl3anc	$$⊢\phi \to sup\left({ℝ}^{+}\cap {\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\leftrightarrow 2\cdot 2\le 2B\right)$$
79	32 20 77 78	syl3anc	$$⊢\phi \to \left(2\le B\leftrightarrow 2\cdot 2\le 2B\right)$$
80	75 79	mpbid	$$⊢\phi \to 2\cdot 2\le 2B$$
81	31 80	eqbrtrrid	$$⊢\phi \to 4\le 2B$$
82	24 27 22 30 81	ltletrd	$$⊢\phi \to A<2B$$
83	24 22	posdifd	$$⊢\phi \to \left(A<2B\leftrightarrow 0<2B-A\right)$$
84	82 83	mpbid	$$⊢\phi \to 0<2B-A$$
85	25 84	elrpd	$$⊢\phi \to 2B-A\in {ℝ}^{+}$$
86	22	recnd	$$⊢\phi \to 2B\in ℂ$$
87	24	recnd	$$⊢\phi \to A\in ℂ$$
88		sinsub	$$⊢\left(2B\in ℂ\wedge A\in ℂ\right)\to \sin \left(2B-A\right)=\sin 2B\cos A-\cos 2B\sin A$$
89	86 87 88	syl2anc	$$⊢\phi \to \sin \left(2B-A\right)=\sin 2B\cos A-\cos 2B\sin A$$
90	20	recnd	$$⊢\phi \to B\in ℂ$$
91		sin2t	$$⊢B\in ℂ\to \sin 2B=2\sin B\cos B$$
92	90 91	syl	$$⊢\phi \to \sin 2B=2\sin B\cos B$$
93	4	oveq1d	$$⊢\phi \to \sin B\cos B=0\cdot \cos B$$
94	90	coscld	$$⊢\phi \to \cos B\in ℂ$$
95	94	mul02d	$$⊢\phi \to 0\cdot \cos B=0$$
96	93 95	eqtrd	$$⊢\phi \to \sin B\cos B=0$$
97	96	oveq2d	$$⊢\phi \to 2\sin B\cos B=2\cdot 0$$
98		2t0e0	$$⊢2\cdot 0=0$$
99	97 98	eqtrdi	$$⊢\phi \to 2\sin B\cos B=0$$
100	92 99	eqtrd	$$⊢\phi \to \sin 2B=0$$
101	100	oveq1d	$$⊢\phi \to \sin 2B\cos A=0\cdot \cos A$$
102	87	coscld	$$⊢\phi \to \cos A\in ℂ$$
103	102	mul02d	$$⊢\phi \to 0\cdot \cos A=0$$
104	101 103	eqtrd	$$⊢\phi \to \sin 2B\cos A=0$$
105	3	oveq2d	$$⊢\phi \to \cos 2B\sin A=\cos 2B\cdot 0$$
106	86	coscld	$$⊢\phi \to \cos 2B\in ℂ$$
107	106	mul01d	$$⊢\phi \to \cos 2B\cdot 0=0$$
108	105 107	eqtrd	$$⊢\phi \to \cos 2B\sin A=0$$
109	104 108	oveq12d	$$⊢\phi \to \sin 2B\cos A-\cos 2B\sin A=0-0$$
110		0m0e0	$$⊢0-0=0$$
111	109 110	eqtrdi	$$⊢\phi \to \sin 2B\cos A-\cos 2B\sin A=0$$
112	89 111	eqtrd	$$⊢\phi \to \sin \left(2B-A\right)=0$$
113		pilem1	$$⊢2B-A\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\leftrightarrow \left(2B-A\in {ℝ}^{+}\wedge \sin \left(2B-A\right)=0\right)$$
114	85 112 113	sylanbrc	$$⊢\phi \to 2B-A\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)$$
115		infrelb	$$⊢\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\subseteq ℝ\wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)x\le y\wedge 2B-A\in \left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right]\right)\right)\to sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le 2B-A$$
116	9 18 114 115	syl3anc	$$⊢\phi \to sup\left({ℝ}^{+}\cap {\sin }^{-1}\left[\left\{0\right\}\right],ℝ,<\right)\le 2B-A$$
117	5 116	eqbrtrid	$$⊢\phi \to \mathrm{\pi }\le 2B-A$$
118	5 44	eqeltrid	$$⊢\phi \to \mathrm{\pi }\in ℝ$$
119		leaddsub	$$⊢\left(\mathrm{\pi }\in ℝ\wedge A\in ℝ\wedge 2B\in ℝ\right)\to \left(\mathrm{\pi }+A\le 2B\leftrightarrow \mathrm{\pi }\le 2B-A\right)$$
120	118 24 22 119	syl3anc	$$⊢\phi \to \left(\mathrm{\pi }+A\le 2B\leftrightarrow \mathrm{\pi }\le 2B-A\right)$$
121	117 120	mpbird	$$⊢\phi \to \mathrm{\pi }+A\le 2B$$
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\leftrightarrow \mathrm{\pi }+A\le 2B\right)$$
124	122 20 77 123	syl3anc	$$⊢\phi \to \left(\frac{\mathrm{\pi }+A}{2}\le B\leftrightarrow \mathrm{\pi }+A\le 2B\right)$$
125	121 124	mpbird	$$⊢\phi \to \frac{\mathrm{\pi }+A}{2}\le B$$