Proof of Theorem cos12dec
Step | Hyp | Ref
| Expression |
1 | | 1re 7765 |
. . . . . . . . . . 11
|
2 | | 2re 8790 |
. . . . . . . . . . 11
|
3 | | iccssre 9738 |
. . . . . . . . . . 11
|
4 | 1, 2, 3 | mp2an 422 |
. . . . . . . . . 10
|
5 | 4 | sseli 3093 |
. . . . . . . . 9
|
6 | 5 | 3ad2ant2 1003 |
. . . . . . . 8
|
7 | 6 | recnd 7794 |
. . . . . . 7
|
8 | 4 | sseli 3093 |
. . . . . . . . . . 11
|
9 | 8 | 3ad2ant1 1002 |
. . . . . . . . . 10
|
10 | 6, 9 | resubcld 8143 |
. . . . . . . . 9
|
11 | 10 | recnd 7794 |
. . . . . . . 8
|
12 | 11 | halfcld 8964 |
. . . . . . 7
|
13 | 7, 12 | subcld 8073 |
. . . . . 6
|
14 | 13 | coscld 11418 |
. . . . 5
|
15 | 12 | coscld 11418 |
. . . . 5
|
16 | 14, 15 | mulcld 7786 |
. . . 4
|
17 | 13 | sincld 11417 |
. . . . 5
|
18 | 12 | sincld 11417 |
. . . . 5
|
19 | 17, 18 | mulcld 7786 |
. . . 4
|
20 | 16, 19 | negsubd 8079 |
. . 3
|
21 | 10 | rehalfcld 8966 |
. . . . . . . 8
|
22 | 6, 21 | resubcld 8143 |
. . . . . . 7
|
23 | 22 | resincld 11430 |
. . . . . 6
|
24 | 21 | resincld 11430 |
. . . . . 6
|
25 | 23, 24 | remulcld 7796 |
. . . . 5
|
26 | 25 | renegcld 8142 |
. . . 4
|
27 | 22 | recoscld 11431 |
. . . . 5
|
28 | 21 | recoscld 11431 |
. . . . 5
|
29 | 27, 28 | remulcld 7796 |
. . . 4
|
30 | | 0red 7767 |
. . . . 5
|
31 | 1 | a1i 9 |
. . . . . . . . . . 11
|
32 | 31 | rehalfcld 8966 |
. . . . . . . . . 10
|
33 | | simp3 983 |
. . . . . . . . . . . . 13
|
34 | 9, 6 | posdifd 8294 |
. . . . . . . . . . . . 13
|
35 | 33, 34 | mpbid 146 |
. . . . . . . . . . . 12
|
36 | | halfpos2 8950 |
. . . . . . . . . . . . 13
|
37 | 10, 36 | syl 14 |
. . . . . . . . . . . 12
|
38 | 35, 37 | mpbid 146 |
. . . . . . . . . . 11
|
39 | | 2rp 9446 |
. . . . . . . . . . . . 13
|
40 | 39 | a1i 9 |
. . . . . . . . . . . 12
|
41 | 2 | a1i 9 |
. . . . . . . . . . . . . 14
|
42 | 1 | rexri 7823 |
. . . . . . . . . . . . . . . 16
|
43 | 2 | rexri 7823 |
. . . . . . . . . . . . . . . 16
|
44 | | iccleub 9714 |
. . . . . . . . . . . . . . . 16
|
45 | 42, 43, 44 | mp3an12 1305 |
. . . . . . . . . . . . . . 15
|
46 | 45 | 3ad2ant2 1003 |
. . . . . . . . . . . . . 14
|
47 | | iccgelb 9715 |
. . . . . . . . . . . . . . . 16
|
48 | 42, 43, 47 | mp3an12 1305 |
. . . . . . . . . . . . . . 15
|
49 | 48 | 3ad2ant1 1002 |
. . . . . . . . . . . . . 14
|
50 | 6, 31, 41, 9, 46, 49 | le2subd 8326 |
. . . . . . . . . . . . 13
|
51 | | 2m1e1 8838 |
. . . . . . . . . . . . 13
|
52 | 50, 51 | breqtrdi 3969 |
. . . . . . . . . . . 12
|
53 | 10, 31, 40, 52 | lediv1dd 9542 |
. . . . . . . . . . 11
|
54 | 30, 21, 32, 38, 53 | ltletrd 8185 |
. . . . . . . . . 10
|
55 | | 1mhlfehlf 8938 |
. . . . . . . . . . 11
|
56 | | iccgelb 9715 |
. . . . . . . . . . . . . 14
|
57 | 42, 43, 56 | mp3an12 1305 |
. . . . . . . . . . . . 13
|
58 | 57 | 3ad2ant2 1003 |
. . . . . . . . . . . 12
|
59 | 31, 21, 6, 32, 58, 53 | le2subd 8326 |
. . . . . . . . . . 11
|
60 | 55, 59 | eqbrtrrid 3964 |
. . . . . . . . . 10
|
61 | 30, 32, 22, 54, 60 | ltletrd 8185 |
. . . . . . . . 9
|
62 | 30, 21, 38 | ltled 7881 |
. . . . . . . . . . 11
|
63 | 6, 30, 41, 21, 46, 62 | le2subd 8326 |
. . . . . . . . . 10
|
64 | | 2cn 8791 |
. . . . . . . . . . 11
|
65 | 64 | subid1i 8034 |
. . . . . . . . . 10
|
66 | 63, 65 | breqtrdi 3969 |
. . . . . . . . 9
|
67 | | 0xr 7812 |
. . . . . . . . . 10
|
68 | | elioc2 9719 |
. . . . . . . . . 10
|
69 | 67, 2, 68 | mp2an 422 |
. . . . . . . . 9
|
70 | 22, 61, 66, 69 | syl3anbrc 1165 |
. . . . . . . 8
|
71 | | sin02gt0 11470 |
. . . . . . . 8
|
72 | 70, 71 | syl 14 |
. . . . . . 7
|
73 | | halfre 8933 |
. . . . . . . . . . . 12
|
74 | | halflt1 8937 |
. . . . . . . . . . . . 13
|
75 | | 1lt2 8889 |
. . . . . . . . . . . . 13
|
76 | 73, 1, 2 | lttri 7868 |
. . . . . . . . . . . . 13
|
77 | 74, 75, 76 | mp2an 422 |
. . . . . . . . . . . 12
|
78 | 73, 2, 77 | ltleii 7866 |
. . . . . . . . . . 11
|
79 | 78 | a1i 9 |
. . . . . . . . . 10
|
80 | 21, 32, 41, 53, 79 | letrd 7886 |
. . . . . . . . 9
|
81 | | elioc2 9719 |
. . . . . . . . . 10
|
82 | 67, 2, 81 | mp2an 422 |
. . . . . . . . 9
|
83 | 21, 38, 80, 82 | syl3anbrc 1165 |
. . . . . . . 8
|
84 | | sin02gt0 11470 |
. . . . . . . 8
|
85 | 83, 84 | syl 14 |
. . . . . . 7
|
86 | 23, 24, 72, 85 | mulgt0d 7885 |
. . . . . 6
|
87 | 25 | lt0neg2d 8278 |
. . . . . 6
|
88 | 86, 87 | mpbid 146 |
. . . . 5
|
89 | 26, 30, 25, 88, 86 | lttrd 7888 |
. . . 4
|
90 | 26, 25, 29, 89 | ltadd2dd 8184 |
. . 3
|
91 | 20, 90 | eqbrtrrd 3952 |
. 2
|
92 | 7, 12 | npcand 8077 |
. . . 4
|
93 | 92 | fveq2d 5425 |
. . 3
|
94 | | cosadd 11444 |
. . . 4
|
95 | 13, 12, 94 | syl2anc 408 |
. . 3
|
96 | 93, 95 | eqtr3d 2174 |
. 2
|
97 | 7, 12, 12 | subsub4d 8104 |
. . . . 5
|
98 | 11 | 2halvesd 8965 |
. . . . . 6
|
99 | 98 | oveq2d 5790 |
. . . . 5
|
100 | 9 | recnd 7794 |
. . . . . 6
|
101 | 7, 100 | nncand 8078 |
. . . . 5
|
102 | 97, 99, 101 | 3eqtrd 2176 |
. . . 4
|
103 | 102 | fveq2d 5425 |
. . 3
|
104 | | cossub 11448 |
. . . 4
|
105 | 13, 12, 104 | syl2anc 408 |
. . 3
|
106 | 103, 105 | eqtr3d 2174 |
. 2
|
107 | 91, 96, 106 | 3brtr4d 3960 |
1
|