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