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 2thalfe1 ⊢ 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