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 mullidi ⊢ ( 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 mullidi ⊢ ( 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 ) ) )