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 )