Metamath Proof Explorer

Theorem sinhalfpilem

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

Ref Expression
Assertion sinhalfpilem 
|- ( ( sin ` ( _pi / 2 ) ) = 1 /\ ( cos ` ( _pi / 2 ) ) = 0 )

Proof

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