Metamath Proof Explorer

Theorem sinhalfpilem

Description: Lemma for sinhalfpi and coshalfpi . (Contributed by Paul Chapman, 23-Jan-2008)

Ref Expression
Assertion sinhalfpilem ⊢ sin ⁡ π 2 = 1 ∧ cos ⁡ π 2 = 0

Proof

Step Hyp Ref Expression
1 0lt1 ⊢ 0 < 1
2 0re ⊢ 0 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 2 3 ltnsymi ⊢ 0 < 1 → ¬ 1 < 0
5 1 4 ax-mp ⊢ ¬ 1 < 0
6 lt0neg1 ⊢ 1 ∈ ℝ → 1 < 0 ↔ 0 < − 1
7 3 6 ax-mp ⊢ 1 < 0 ↔ 0 < − 1
8 5 7 mtbi ⊢ ¬ 0 < − 1
9 pire ⊢ π ∈ ℝ
10 9 rehalfcli ⊢ π 2 ∈ ℝ
11 2re ⊢ 2 ∈ ℝ
12 pipos ⊢ 0 < π
13 2pos ⊢ 0 < 2
14 9 11 12 13 divgt0ii ⊢ 0 < π 2
15 4re ⊢ 4 ∈ ℝ
16 pigt2lt4 ⊢ 2 < π ∧ π < 4
17 16 simpri ⊢ π < 4
18 9 15 17 ltleii ⊢ π ≤ 4
19 11 13 pm3.2i ⊢ 2 ∈ ℝ ∧ 0 < 2
20 ledivmul ⊢ π ∈ ℝ ∧ 2 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 → π 2 ≤ 2 ↔ π ≤ 2 ⋅ 2
21 9 11 19 20 mp3an ⊢ π 2 ≤ 2 ↔ π ≤ 2 ⋅ 2
22 2t2e4 ⊢ 2 ⋅ 2 = 4
23 22 breq2i ⊢ π ≤ 2 ⋅ 2 ↔ π ≤ 4
24 21 23 bitr2i ⊢ π ≤ 4 ↔ π 2 ≤ 2
25 18 24 mpbi ⊢ π 2 ≤ 2
26 0xr ⊢ 0 ∈ ℝ *
27 elioc2 ⊢ 0 ∈ ℝ * ∧ 2 ∈ ℝ → π 2 ∈ 0 2 ↔ π 2 ∈ ℝ ∧ 0 < π 2 ∧ π 2 ≤ 2
28 26 11 27 mp2an ⊢ π 2 ∈ 0 2 ↔ π 2 ∈ ℝ ∧ 0 < π 2 ∧ π 2 ≤ 2
29 10 14 25 28 mpbir3an ⊢ π 2 ∈ 0 2
30 sin02gt0 ⊢ π 2 ∈ 0 2 → 0 < sin ⁡ π 2
31 29 30 ax-mp ⊢ 0 < sin ⁡ π 2
32 breq2 ⊢ sin ⁡ π 2 = − 1 → 0 < sin ⁡ π 2 ↔ 0 < − 1
33 31 32 mpbii ⊢ sin ⁡ π 2 = − 1 → 0 < − 1
34 8 33 mto ⊢ ¬ sin ⁡ π 2 = − 1
35 sq1 ⊢ 1 2 = 1
36 resincl ⊢ π 2 ∈ ℝ → sin ⁡ π 2 ∈ ℝ
37 10 36 ax-mp ⊢ sin ⁡ π 2 ∈ ℝ
38 37 31 gt0ne0ii ⊢ sin ⁡ π 2 ≠ 0
39 38 neii ⊢ ¬ sin ⁡ π 2 = 0
40 2ne0 ⊢ 2 ≠ 0
41 40 neii ⊢ ¬ 2 = 0
42 9 recni ⊢ π ∈ ℂ
43 2cn ⊢ 2 ∈ ℂ
44 42 43 40 divcan2i ⊢ 2 ⁢ π 2 = π
45 44 fveq2i ⊢ sin ⁡ 2 ⁢ π 2 = sin ⁡ π
46 10 recni ⊢ π 2 ∈ ℂ
47 sin2t ⊢ π 2 ∈ ℂ → sin ⁡ 2 ⁢ π 2 = 2 ⁢ sin ⁡ π 2 ⁢ cos ⁡ π 2
48 46 47 ax-mp ⊢ sin ⁡ 2 ⁢ π 2 = 2 ⁢ sin ⁡ π 2 ⁢ cos ⁡ π 2
49 45 48 eqtr3i ⊢ sin ⁡ π = 2 ⁢ sin ⁡ π 2 ⁢ cos ⁡ π 2
50 sinpi ⊢ sin ⁡ π = 0
51 49 50 eqtr3i ⊢ 2 ⁢ sin ⁡ π 2 ⁢ cos ⁡ π 2 = 0
52 sincl ⊢ π 2 ∈ ℂ → sin ⁡ π 2 ∈ ℂ
53 46 52 ax-mp ⊢ sin ⁡ π 2 ∈ ℂ
54 coscl ⊢ π 2 ∈ ℂ → cos ⁡ π 2 ∈ ℂ
55 46 54 ax-mp ⊢ cos ⁡ π 2 ∈ ℂ
56 53 55 mulcli ⊢ sin ⁡ π 2 ⁢ cos ⁡ π 2 ∈ ℂ
57 43 56 mul0ori ⊢ 2 ⁢ sin ⁡ π 2 ⁢ cos ⁡ π 2 = 0 ↔ 2 = 0 ∨ sin ⁡ π 2 ⁢ cos ⁡ π 2 = 0
58 51 57 mpbi ⊢ 2 = 0 ∨ sin ⁡ π 2 ⁢ cos ⁡ π 2 = 0
59 41 58 mtpor ⊢ sin ⁡ π 2 ⁢ cos ⁡ π 2 = 0
60 53 55 mul0ori ⊢ sin ⁡ π 2 ⁢ cos ⁡ π 2 = 0 ↔ sin ⁡ π 2 = 0 ∨ cos ⁡ π 2 = 0
61 59 60 mpbi ⊢ sin ⁡ π 2 = 0 ∨ cos ⁡ π 2 = 0
62 39 61 mtpor ⊢ cos ⁡ π 2 = 0
63 62 oveq1i ⊢ cos ⁡ π 2 2 = 0 2
64 sq0 ⊢ 0 2 = 0
65 63 64 eqtri ⊢ cos ⁡ π 2 2 = 0
66 65 oveq2i ⊢ sin ⁡ π 2 2 + cos ⁡ π 2 2 = sin ⁡ π 2 2 + 0
67 sincossq ⊢ π 2 ∈ ℂ → sin ⁡ π 2 2 + cos ⁡ π 2 2 = 1
68 46 67 ax-mp ⊢ sin ⁡ π 2 2 + cos ⁡ π 2 2 = 1
69 66 68 eqtr3i ⊢ sin ⁡ π 2 2 + 0 = 1
70 53 sqcli ⊢ sin ⁡ π 2 2 ∈ ℂ
71 70 addid1i ⊢ sin ⁡ π 2 2 + 0 = sin ⁡ π 2 2
72 35 69 71 3eqtr2ri ⊢ sin ⁡ π 2 2 = 1 2
73 ax-1cn ⊢ 1 ∈ ℂ
74 53 73 sqeqori ⊢ sin ⁡ π 2 2 = 1 2 ↔ sin ⁡ π 2 = 1 ∨ sin ⁡ π 2 = − 1
75 72 74 mpbi ⊢ sin ⁡ π 2 = 1 ∨ sin ⁡ π 2 = − 1
76 75 ori ⊢ ¬ sin ⁡ π 2 = 1 → sin ⁡ π 2 = − 1
77 34 76 mt3 ⊢ sin ⁡ π 2 = 1
78 77 62 pm3.2i ⊢ sin ⁡ π 2 = 1 ∧ cos ⁡ π 2 = 0