Theorem sinhalfpilem

Description: Lemma for sinhalfpi and coshalfpi . (Contributed by Paul Chapman, 23-Jan-2008)

	Ref	Expression
Assertion	sinhalfpilem	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{2}\right)=1\wedge \cos \left(\frac{\mathrm{\pi }}{2}\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		0lt1	$$⊢0<1$$
2		0re	$$⊢0\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4	2 3	ltnsymi	$$⊢0<1\to \neg 1<0$$
5	1 4	ax-mp	$$⊢\neg 1<0$$
6		lt0neg1	$$⊢1\in ℝ\to \left(1<0\leftrightarrow 0<-1\right)$$
7	3 6	ax-mp	$$⊢1<0\leftrightarrow 0<-1$$
8	5 7	mtbi	$$⊢\neg 0<-1$$
9		pire	$$⊢\mathrm{\pi }\in ℝ$$
10	9	rehalfcli	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
11		2re	$$⊢2\in ℝ$$
12		pipos	$$⊢0<\mathrm{\pi }$$
13		2pos	$$⊢0<2$$
14	9 11 12 13	divgt0ii	$$⊢0<\frac{\mathrm{\pi }}{2}$$
15		4re	$$⊢4\in ℝ$$
16		pigt2lt4	$$⊢\left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$$
17	16	simpri	$$⊢\mathrm{\pi }<4$$
18	9 15 17	ltleii	$$⊢\mathrm{\pi }\le 4$$
19	11 13	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
20		ledivmul	$$⊢\left(\mathrm{\pi }\in ℝ\wedge 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{\mathrm{\pi }}{2}\le 2\leftrightarrow \mathrm{\pi }\le 2\cdot 2\right)$$
21	9 11 19 20	mp3an	$$⊢\frac{\mathrm{\pi }}{2}\le 2\leftrightarrow \mathrm{\pi }\le 2\cdot 2$$
22		2t2e4	$$⊢2\cdot 2=4$$
23	22	breq2i	$$⊢\mathrm{\pi }\le 2\cdot 2\leftrightarrow \mathrm{\pi }\le 4$$
24	21 23	bitr2i	$$⊢\mathrm{\pi }\le 4\leftrightarrow \frac{\mathrm{\pi }}{2}\le 2$$
25	18 24	mpbi	$$⊢\frac{\mathrm{\pi }}{2}\le 2$$
26		0xr	$$⊢0\in {ℝ}^{*}$$
27		elioc2	$$⊢\left(0\in {ℝ}^{*}\wedge 2\in ℝ\right)\to \left(\frac{\mathrm{\pi }}{2}\in \left(0,2\right]\leftrightarrow \left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge 0<\frac{\mathrm{\pi }}{2}\wedge \frac{\mathrm{\pi }}{2}\le 2\right)\right)$$
28	26 11 27	mp2an	$$⊢\frac{\mathrm{\pi }}{2}\in \left(0,2\right]\leftrightarrow \left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge 0<\frac{\mathrm{\pi }}{2}\wedge \frac{\mathrm{\pi }}{2}\le 2\right)$$
29	10 14 25 28	mpbir3an	$$⊢\frac{\mathrm{\pi }}{2}\in \left(0,2\right]$$
30		sin02gt0	$$⊢\frac{\mathrm{\pi }}{2}\in \left(0,2\right]\to 0<\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
31	29 30	ax-mp	$$⊢0<\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
32		breq2	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=-1\to \left(0<\sin \left(\frac{\mathrm{\pi }}{2}\right)\leftrightarrow 0<-1\right)$$
33	31 32	mpbii	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=-1\to 0<-1$$
34	8 33	mto	$$⊢\neg \sin \left(\frac{\mathrm{\pi }}{2}\right)=-1$$
35		sq1	$$⊢1^2=1$$
36		resincl	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \sin \left(\frac{\mathrm{\pi }}{2}\right)\in ℝ$$
37	10 36	ax-mp	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\in ℝ$$
38	37 31	gt0ne0ii	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\ne 0$$
39	38	neii	$$⊢\neg \sin \left(\frac{\mathrm{\pi }}{2}\right)=0$$
40		2ne0	$$⊢2\ne 0$$
41	40	neii	$$⊢\neg 2=0$$
42	9	recni	$$⊢\mathrm{\pi }\in ℂ$$
43		2cn	$$⊢2\in ℂ$$
44	42 43 40	divcan2i	$$⊢2\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }$$
45	44	fveq2i	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{2}\right)=\sin \mathrm{\pi }$$
46	10	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
47		sin2t	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to \sin 2\left(\frac{\mathrm{\pi }}{2}\right)=2\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)$$
48	46 47	ax-mp	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{2}\right)=2\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)$$
49	45 48	eqtr3i	$$⊢\sin \mathrm{\pi }=2\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)$$
50		sinpi	$$⊢\sin \mathrm{\pi }=0$$
51	49 50	eqtr3i	$$⊢2\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
52		sincl	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to \sin \left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
53	46 52	ax-mp	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
54		coscl	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to \cos \left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
55	46 54	ax-mp	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
56	53 55	mulcli	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
57	43 56	mul0ori	$$⊢2\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\leftrightarrow \left(2=0\vee \sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\right)$$
58	51 57	mpbi	$$⊢\left(2=0\vee \sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\right)$$
59	41 58	mtpor	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
60	53 55	mul0ori	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\leftrightarrow \left(\sin \left(\frac{\mathrm{\pi }}{2}\right)=0\vee \cos \left(\frac{\mathrm{\pi }}{2}\right)=0\right)$$
61	59 60	mpbi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{2}\right)=0\vee \cos \left(\frac{\mathrm{\pi }}{2}\right)=0\right)$$
62	39 61	mtpor	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
63	62	oveq1i	$$⊢{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=0^2$$
64		sq0	$$⊢0^2=0$$
65	63 64	eqtri	$$⊢{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=0$$
66	65	oveq2i	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2+{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2={\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2+0$$
67		sincossq	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to {\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2+{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=1$$
68	46 67	ax-mp	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2+{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=1$$
69	66 68	eqtr3i	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2+0=1$$
70	53	sqcli	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2\in ℂ$$
71	70	addridi	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2+0={\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2$$
72	35 69 71	3eqtr2ri	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2=1^2$$
73		ax-1cn	$$⊢1\in ℂ$$
74	53 73	sqeqori	$$⊢{\sin \left(\frac{\mathrm{\pi }}{2}\right)}^2=1^2\leftrightarrow \left(\sin \left(\frac{\mathrm{\pi }}{2}\right)=1\vee \sin \left(\frac{\mathrm{\pi }}{2}\right)=-1\right)$$
75	72 74	mpbi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{2}\right)=1\vee \sin \left(\frac{\mathrm{\pi }}{2}\right)=-1\right)$$
76	75	ori	$$⊢\neg \sin \left(\frac{\mathrm{\pi }}{2}\right)=1\to \sin \left(\frac{\mathrm{\pi }}{2}\right)=-1$$
77	34 76	mt3	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=1$$
78	77 62	pm3.2i	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{2}\right)=1\wedge \cos \left(\frac{\mathrm{\pi }}{2}\right)=0\right)$$