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 ) ) )