sincos4thpi

Description: The sine and cosine of _pi / 4 . (Contributed by Paul Chapman, 25-Jan-2008)

		Ref	Expression
	Assertion	sincos4thpi	$⊢ (\sin (\frac{π}{4}) = \frac{1}{\sqrt{2}} \land \cos (\frac{π}{4}) = \frac{1}{\sqrt{2}})$

Proof

Step	Hyp	Ref	Expression
1		halfcn	$⊢ \frac{1}{2} \in ℂ$
2		ax-1cn	$⊢ 1 \in ℂ$
3		2halves	$⊢ 1 \in ℂ \to (\frac{1}{2}) + (\frac{1}{2}) = 1$
4	2 3	ax-mp	$⊢ (\frac{1}{2}) + (\frac{1}{2}) = 1$
5		sincosq1eq	$⊢ (\frac{1}{2} \in ℂ \land \frac{1}{2} \in ℂ \land (\frac{1}{2}) + (\frac{1}{2}) = 1) \to \sin (\frac{1}{2}) (\frac{π}{2}) = \cos (\frac{1}{2}) (\frac{π}{2})$
6	1 1 4 5	mp3an	$⊢ \sin (\frac{1}{2}) (\frac{π}{2}) = \cos (\frac{1}{2}) (\frac{π}{2})$
7	6	oveq2i	$⊢ \sin (\frac{1}{2}) (\frac{π}{2}) \sin (\frac{1}{2}) (\frac{π}{2}) = \sin (\frac{1}{2}) (\frac{π}{2}) \cos (\frac{1}{2}) (\frac{π}{2})$
8	7	oveq2i	$⊢ 2 \sin (\frac{1}{2}) (\frac{π}{2}) \sin (\frac{1}{2}) (\frac{π}{2}) = 2 \sin (\frac{1}{2}) (\frac{π}{2}) \cos (\frac{1}{2}) (\frac{π}{2})$
9		2cn	$⊢ 2 \in ℂ$
10		pire	$⊢ π \in ℝ$
11	10	recni	$⊢ π \in ℂ$
12		2ne0	$⊢ 2 \neq 0$
13	2 9 11 9 12 12	divmuldivi	$⊢ (\frac{1}{2}) (\frac{π}{2}) = \frac{1 π}{2 \cdot 2}$
14	11	mullidi	$⊢ 1 π = π$
15		2t2e4	$⊢ 2 \cdot 2 = 4$
16	14 15	oveq12i	$⊢ \frac{1 π}{2 \cdot 2} = \frac{π}{4}$
17	13 16	eqtri	$⊢ (\frac{1}{2}) (\frac{π}{2}) = \frac{π}{4}$
18	17	fveq2i	$⊢ \sin (\frac{1}{2}) (\frac{π}{2}) = \sin (\frac{π}{4})$
19	18 18	oveq12i	$⊢ \sin (\frac{1}{2}) (\frac{π}{2}) \sin (\frac{1}{2}) (\frac{π}{2}) = \sin (\frac{π}{4}) \sin (\frac{π}{4})$
20	19	oveq2i	$⊢ 2 \sin (\frac{1}{2}) (\frac{π}{2}) \sin (\frac{1}{2}) (\frac{π}{2}) = 2 \sin (\frac{π}{4}) \sin (\frac{π}{4})$
21	9 12	recidi	$⊢ 2 (\frac{1}{2}) = 1$
22	21	oveq1i	$⊢ 2 (\frac{1}{2}) (\frac{π}{2}) = 1 (\frac{π}{2})$
23		2re	$⊢ 2 \in ℝ$
24	10 23 12	redivcli	$⊢ \frac{π}{2} \in ℝ$
25	24	recni	$⊢ \frac{π}{2} \in ℂ$
26	9 1 25	mulassi	$⊢ 2 (\frac{1}{2}) (\frac{π}{2}) = 2 (\frac{1}{2}) (\frac{π}{2})$
27	25	mullidi	$⊢ 1 (\frac{π}{2}) = \frac{π}{2}$
28	22 26 27	3eqtr3i	$⊢ 2 (\frac{1}{2}) (\frac{π}{2}) = \frac{π}{2}$
29	28	fveq2i	$⊢ \sin 2 (\frac{1}{2}) (\frac{π}{2}) = \sin (\frac{π}{2})$
30	1 25	mulcli	$⊢ (\frac{1}{2}) (\frac{π}{2}) \in ℂ$
31		sin2t	$⊢ (\frac{1}{2}) (\frac{π}{2}) \in ℂ \to \sin 2 (\frac{1}{2}) (\frac{π}{2}) = 2 \sin (\frac{1}{2}) (\frac{π}{2}) \cos (\frac{1}{2}) (\frac{π}{2})$
32	30 31	ax-mp	$⊢ \sin 2 (\frac{1}{2}) (\frac{π}{2}) = 2 \sin (\frac{1}{2}) (\frac{π}{2}) \cos (\frac{1}{2}) (\frac{π}{2})$
33		sinhalfpi	$⊢ \sin (\frac{π}{2}) = 1$
34	29 32 33	3eqtr3i	$⊢ 2 \sin (\frac{1}{2}) (\frac{π}{2}) \cos (\frac{1}{2}) (\frac{π}{2}) = 1$
35	8 20 34	3eqtr3i	$⊢ 2 \sin (\frac{π}{4}) \sin (\frac{π}{4}) = 1$
36	35	fveq2i	$⊢ \sqrt{2 \sin (\frac{π}{4}) \sin (\frac{π}{4})} = \sqrt{1}$
37		4re	$⊢ 4 \in ℝ$
38		4ne0	$⊢ 4 \neq 0$
39	10 37 38	redivcli	$⊢ \frac{π}{4} \in ℝ$
40		resincl	$⊢ \frac{π}{4} \in ℝ \to \sin (\frac{π}{4}) \in ℝ$
41	39 40	ax-mp	$⊢ \sin (\frac{π}{4}) \in ℝ$
42	41 41	remulcli	$⊢ \sin (\frac{π}{4}) \sin (\frac{π}{4}) \in ℝ$
43		0le2	$⊢ 0 \leq 2$
44	41	msqge0i	$⊢ 0 \leq \sin (\frac{π}{4}) \sin (\frac{π}{4})$
45	23 42 43 44	sqrtmulii	$⊢ \sqrt{2 \sin (\frac{π}{4}) \sin (\frac{π}{4})} = \sqrt{2} \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})}$
46		sqrt1	$⊢ \sqrt{1} = 1$
47	36 45 46	3eqtr3ri	$⊢ 1 = \sqrt{2} \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})}$
48	42	sqrtcli	$⊢ 0 \leq \sin (\frac{π}{4}) \sin (\frac{π}{4}) \to \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} \in ℝ$
49	44 48	ax-mp	$⊢ \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} \in ℝ$
50	49	recni	$⊢ \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} \in ℂ$
51		sqrt2re	$⊢ \sqrt{2} \in ℝ$
52	51	recni	$⊢ \sqrt{2} \in ℂ$
53		sqrt00	$⊢ (2 \in ℝ \land 0 \leq 2) \to (\sqrt{2} = 0 \leftrightarrow 2 = 0)$
54	23 43 53	mp2an	$⊢ \sqrt{2} = 0 \leftrightarrow 2 = 0$
55	54	necon3bii	$⊢ \sqrt{2} \neq 0 \leftrightarrow 2 \neq 0$
56	12 55	mpbir	$⊢ \sqrt{2} \neq 0$
57	52 56	pm3.2i	$⊢ (\sqrt{2} \in ℂ \land \sqrt{2} \neq 0)$
58		divmul2	$⊢ (1 \in ℂ \land \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} \in ℂ \land (\sqrt{2} \in ℂ \land \sqrt{2} \neq 0)) \to (\frac{1}{\sqrt{2}} = \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} \leftrightarrow 1 = \sqrt{2} \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})})$
59	2 50 57 58	mp3an	$⊢ \frac{1}{\sqrt{2}} = \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} \leftrightarrow 1 = \sqrt{2} \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})}$
60	47 59	mpbir	$⊢ \frac{1}{\sqrt{2}} = \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})}$
61		0re	$⊢ 0 \in ℝ$
62		pipos	$⊢ 0 < π$
63		4pos	$⊢ 0 < 4$
64	10 37 62 63	divgt0ii	$⊢ 0 < \frac{π}{4}$
65		1re	$⊢ 1 \in ℝ$
66		pigt2lt4	$⊢ (2 < π \land π < 4)$
67	66	simpri	$⊢ π < 4$
68	10 37 37 63	ltdiv1ii	$⊢ π < 4 \leftrightarrow \frac{π}{4} < \frac{4}{4}$
69	67 68	mpbi	$⊢ \frac{π}{4} < \frac{4}{4}$
70	37	recni	$⊢ 4 \in ℂ$
71	70 38	dividi	$⊢ \frac{4}{4} = 1$
72	69 71	breqtri	$⊢ \frac{π}{4} < 1$
73	39 65 72	ltleii	$⊢ \frac{π}{4} \leq 1$
74		0xr	$⊢ 0 \in ℝ^{*}$
75		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (\frac{π}{4} \in (0, 1] \leftrightarrow (\frac{π}{4} \in ℝ \land 0 < \frac{π}{4} \land \frac{π}{4} \leq 1))$
76	74 65 75	mp2an	$⊢ \frac{π}{4} \in (0, 1] \leftrightarrow (\frac{π}{4} \in ℝ \land 0 < \frac{π}{4} \land \frac{π}{4} \leq 1)$
77	39 64 73 76	mpbir3an	$⊢ \frac{π}{4} \in (0, 1]$
78		sin01gt0	$⊢ \frac{π}{4} \in (0, 1] \to 0 < \sin (\frac{π}{4})$
79	77 78	ax-mp	$⊢ 0 < \sin (\frac{π}{4})$
80	61 41 79	ltleii	$⊢ 0 \leq \sin (\frac{π}{4})$
81	41	sqrtmsqi	$⊢ 0 \leq \sin (\frac{π}{4}) \to \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} = \sin (\frac{π}{4})$
82	80 81	ax-mp	$⊢ \sqrt{\sin (\frac{π}{4}) \sin (\frac{π}{4})} = \sin (\frac{π}{4})$
83	60 82	eqtr2i	$⊢ \sin (\frac{π}{4}) = \frac{1}{\sqrt{2}}$
84	60 82	eqtri	$⊢ \frac{1}{\sqrt{2}} = \sin (\frac{π}{4})$
85	17	fveq2i	$⊢ \cos (\frac{1}{2}) (\frac{π}{2}) = \cos (\frac{π}{4})$
86	6 18 85	3eqtr3i	$⊢ \sin (\frac{π}{4}) = \cos (\frac{π}{4})$
87	84 86	eqtr2i	$⊢ \cos (\frac{π}{4}) = \frac{1}{\sqrt{2}}$
88	83 87	pm3.2i	$⊢ (\sin (\frac{π}{4}) = \frac{1}{\sqrt{2}} \land \cos (\frac{π}{4}) = \frac{1}{\sqrt{2}})$

Metamath Proof Explorer

Theorem sincos4thpi

Proof