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 ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) ) ∧ ( cos ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) ) )

Proof

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