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