Proof of Theorem sin0pilem1
Step | Hyp | Ref
| Expression |
1 | | cosz12 13456 |
. 2
|
2 | | simpr 109 |
. . . . 5
|
3 | | 2re 8937 |
. . . . . . . . . . . 12
|
4 | 3 | a1i 9 |
. . . . . . . . . . 11
|
5 | | elioore 9858 |
. . . . . . . . . . . 12
|
6 | 5 | ad2antrr 485 |
. . . . . . . . . . 11
|
7 | 4, 6 | remulcld 7939 |
. . . . . . . . . 10
|
8 | | elioore 9858 |
. . . . . . . . . . 11
|
9 | 8 | adantl 275 |
. . . . . . . . . 10
|
10 | 7, 9 | resubcld 8289 |
. . . . . . . . 9
|
11 | | eliooord 9874 |
. . . . . . . . . . . 12
|
12 | 11 | simprd 113 |
. . . . . . . . . . 11
|
13 | 12 | adantl 275 |
. . . . . . . . . 10
|
14 | 9, 7 | posdifd 8440 |
. . . . . . . . . 10
|
15 | 13, 14 | mpbid 146 |
. . . . . . . . 9
|
16 | 11 | simpld 111 |
. . . . . . . . . . . . . . . 16
|
17 | 16 | adantl 275 |
. . . . . . . . . . . . . . 15
|
18 | 6, 9, 7, 17 | ltsub2dd 8466 |
. . . . . . . . . . . . . 14
|
19 | 6 | recnd 7937 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | mulid2d 7927 |
. . . . . . . . . . . . . . 15
|
21 | 20 | oveq2d 5867 |
. . . . . . . . . . . . . 14
|
22 | 18, 21 | breqtrrd 4015 |
. . . . . . . . . . . . 13
|
23 | 4 | recnd 7937 |
. . . . . . . . . . . . . 14
|
24 | | 1cnd 7925 |
. . . . . . . . . . . . . 14
|
25 | 23, 24, 19 | subdird 8323 |
. . . . . . . . . . . . 13
|
26 | 22, 25 | breqtrrd 4015 |
. . . . . . . . . . . 12
|
27 | | 2m1e1 8985 |
. . . . . . . . . . . . . 14
|
28 | 27 | oveq1i 5861 |
. . . . . . . . . . . . 13
|
29 | 28, 20 | eqtrid 2215 |
. . . . . . . . . . . 12
|
30 | 26, 29 | breqtrd 4013 |
. . . . . . . . . . 11
|
31 | | eliooord 9874 |
. . . . . . . . . . . . 13
|
32 | 31 | simprd 113 |
. . . . . . . . . . . 12
|
33 | 32 | ad2antrr 485 |
. . . . . . . . . . 11
|
34 | 10, 6, 4, 30, 33 | lttrd 8034 |
. . . . . . . . . 10
|
35 | 10, 4, 34 | ltled 8027 |
. . . . . . . . 9
|
36 | | 0xr 7955 |
. . . . . . . . . 10
|
37 | | elioc2 9882 |
. . . . . . . . . 10
|
38 | 36, 3, 37 | mp2an 424 |
. . . . . . . . 9
|
39 | 10, 15, 35, 38 | syl3anbrc 1176 |
. . . . . . . 8
|
40 | | sin02gt0 11715 |
. . . . . . . 8
|
41 | 39, 40 | syl 14 |
. . . . . . 7
|
42 | 7 | recnd 7937 |
. . . . . . . . . . . 12
|
43 | 9 | recnd 7937 |
. . . . . . . . . . . . 13
|
44 | 42, 43 | subcld 8219 |
. . . . . . . . . . . 12
|
45 | | sinsub 11692 |
. . . . . . . . . . . 12
|
46 | 42, 44, 45 | syl2anc 409 |
. . . . . . . . . . 11
|
47 | 42, 43 | nncand 8224 |
. . . . . . . . . . . 12
|
48 | 47 | fveq2d 5498 |
. . . . . . . . . . 11
|
49 | | cos2t 11702 |
. . . . . . . . . . . . . . . 16
|
50 | 19, 49 | syl 14 |
. . . . . . . . . . . . . . 15
|
51 | | simplr 525 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | 51 | sq0id 10557 |
. . . . . . . . . . . . . . . . . . 19
|
53 | 52 | oveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
|
54 | | 2t0e0 9026 |
. . . . . . . . . . . . . . . . . 18
|
55 | 53, 54 | eqtrdi 2219 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | oveq1d 5866 |
. . . . . . . . . . . . . . . 16
|
57 | | df-neg 8082 |
. . . . . . . . . . . . . . . 16
|
58 | 56, 57 | eqtr4di 2221 |
. . . . . . . . . . . . . . 15
|
59 | 50, 58 | eqtrd 2203 |
. . . . . . . . . . . . . 14
|
60 | 59 | oveq1d 5866 |
. . . . . . . . . . . . 13
|
61 | 44 | sincld 11662 |
. . . . . . . . . . . . . 14
|
62 | 61 | mulm1d 8318 |
. . . . . . . . . . . . 13
|
63 | 60, 62 | eqtrd 2203 |
. . . . . . . . . . . 12
|
64 | 63 | oveq2d 5867 |
. . . . . . . . . . 11
|
65 | 46, 48, 64 | 3eqtr3d 2211 |
. . . . . . . . . 10
|
66 | 42 | sincld 11662 |
. . . . . . . . . . . 12
|
67 | 44 | coscld 11663 |
. . . . . . . . . . . 12
|
68 | 66, 67 | mulcld 7929 |
. . . . . . . . . . 11
|
69 | 68, 61 | subnegd 8226 |
. . . . . . . . . 10
|
70 | 65, 69 | eqtrd 2203 |
. . . . . . . . 9
|
71 | | sin2t 11701 |
. . . . . . . . . . . . . 14
|
72 | 19, 71 | syl 14 |
. . . . . . . . . . . . 13
|
73 | 51 | oveq2d 5867 |
. . . . . . . . . . . . . . . 16
|
74 | 19 | sincld 11662 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | mul01d 8301 |
. . . . . . . . . . . . . . . 16
|
76 | 73, 75 | eqtrd 2203 |
. . . . . . . . . . . . . . 15
|
77 | 76 | oveq2d 5867 |
. . . . . . . . . . . . . 14
|
78 | 77, 54 | eqtrdi 2219 |
. . . . . . . . . . . . 13
|
79 | 72, 78 | eqtrd 2203 |
. . . . . . . . . . . 12
|
80 | 79 | oveq1d 5866 |
. . . . . . . . . . 11
|
81 | 67 | mul02d 8300 |
. . . . . . . . . . 11
|
82 | 80, 81 | eqtrd 2203 |
. . . . . . . . . 10
|
83 | 82 | oveq1d 5866 |
. . . . . . . . 9
|
84 | 70, 83 | eqtrd 2203 |
. . . . . . . 8
|
85 | 61 | addid2d 8058 |
. . . . . . . 8
|
86 | 84, 85 | eqtrd 2203 |
. . . . . . 7
|
87 | 41, 86 | breqtrrd 4015 |
. . . . . 6
|
88 | 87 | ralrimiva 2543 |
. . . . 5
|
89 | 2, 88 | jca 304 |
. . . 4
|
90 | 89 | ex 114 |
. . 3
|
91 | 90 | reximia 2565 |
. 2
|
92 | 1, 91 | ax-mp 5 |
1
|