Metamath Proof Explorer


Theorem sincos4thpi

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

Ref Expression
Assertion sincos4thpi
|- ( ( sin ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) ) /\ ( cos ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) ) )

Proof

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