Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 10029 |
. . . . . 6
|
2 | 1 | a1i 11 |
. . . . 5
|
3 | | ax-icn 9995 |
. . . . . . . . . 10
|
4 | 3 | a1i 11 |
. . . . . . . . 9
|
5 | | simpr 477 |
. . . . . . . . 9
|
6 | 4, 5 | mulcld 10060 |
. . . . . . . 8
|
7 | | efcl 14813 |
. . . . . . . 8
|
8 | 6, 7 | syl 17 |
. . . . . . 7
|
9 | | ine0 10465 |
. . . . . . . 8
|
10 | 9 | a1i 11 |
. . . . . . 7
|
11 | 8, 4, 10 | divcld 10801 |
. . . . . 6
|
12 | | negicn 10282 |
. . . . . . . . . 10
|
13 | | mulcl 10020 |
. . . . . . . . . 10
|
14 | 12, 5, 13 | sylancr 695 |
. . . . . . . . 9
|
15 | | efcl 14813 |
. . . . . . . . 9
|
16 | 14, 15 | syl 17 |
. . . . . . . 8
|
17 | 16, 4, 10 | divcld 10801 |
. . . . . . 7
|
18 | 17 | negcld 10379 |
. . . . . 6
|
19 | 11, 18 | addcld 10059 |
. . . . 5
|
20 | 8, 16 | addcld 10059 |
. . . . 5
|
21 | 8, 4 | mulcld 10060 |
. . . . . . . 8
|
22 | | efcl 14813 |
. . . . . . . . . 10
|
23 | 22 | adantl 482 |
. . . . . . . . 9
|
24 | | 1cnd 10056 |
. . . . . . . . . . 11
|
25 | 2 | dvmptid 23720 |
. . . . . . . . . . 11
|
26 | 3 | a1i 11 |
. . . . . . . . . . 11
|
27 | 2, 5, 24, 25, 26 | dvmptcmul 23727 |
. . . . . . . . . 10
|
28 | 3 | mulid1i 10042 |
. . . . . . . . . . 11
|
29 | 28 | mpteq2i 4741 |
. . . . . . . . . 10
|
30 | 27, 29 | syl6eq 2672 |
. . . . . . . . 9
|
31 | | eff 14812 |
. . . . . . . . . . . . 13
|
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
|
33 | 32 | feqmptd 6249 |
. . . . . . . . . . 11
|
34 | 33 | oveq2d 6666 |
. . . . . . . . . 10
|
35 | | dvef 23743 |
. . . . . . . . . . 11
|
36 | 35, 33 | syl5eq 2668 |
. . . . . . . . . 10
|
37 | 34, 36 | eqtr3d 2658 |
. . . . . . . . 9
|
38 | | fveq2 6191 |
. . . . . . . . 9
|
39 | 2, 2, 6, 4, 23, 23, 30, 37, 38, 38 | dvmptco 23735 |
. . . . . . . 8
|
40 | 9 | a1i 11 |
. . . . . . . 8
|
41 | 2, 8, 21, 39, 26, 40 | dvmptdivc 23728 |
. . . . . . 7
|
42 | 8, 4, 10 | divcan4d 10807 |
. . . . . . . 8
|
43 | 42 | mpteq2dva 4744 |
. . . . . . 7
|
44 | 41, 43 | eqtrd 2656 |
. . . . . 6
|
45 | | mulcl 10020 |
. . . . . . . . . 10
|
46 | 16, 12, 45 | sylancl 694 |
. . . . . . . . 9
|
47 | 46, 4, 10 | divcld 10801 |
. . . . . . . 8
|
48 | 12 | a1i 11 |
. . . . . . . . . 10
|
49 | 12 | a1i 11 |
. . . . . . . . . . . 12
|
50 | 2, 5, 24, 25, 49 | dvmptcmul 23727 |
. . . . . . . . . . 11
|
51 | 12 | mulid1i 10042 |
. . . . . . . . . . . 12
|
52 | 51 | mpteq2i 4741 |
. . . . . . . . . . 11
|
53 | 50, 52 | syl6eq 2672 |
. . . . . . . . . 10
|
54 | | fveq2 6191 |
. . . . . . . . . 10
|
55 | 2, 2, 14, 48, 23, 23, 53, 37, 54, 54 | dvmptco 23735 |
. . . . . . . . 9
|
56 | 2, 16, 46, 55, 26, 40 | dvmptdivc 23728 |
. . . . . . . 8
|
57 | 2, 17, 47, 56 | dvmptneg 23729 |
. . . . . . 7
|
58 | 46, 4, 10 | divneg2d 10815 |
. . . . . . . . 9
|
59 | 3, 9 | negne0i 10356 |
. . . . . . . . . . 11
|
60 | 59 | a1i 11 |
. . . . . . . . . 10
|
61 | 16, 48, 60 | divcan4d 10807 |
. . . . . . . . 9
|
62 | 58, 61 | eqtrd 2656 |
. . . . . . . 8
|
63 | 62 | mpteq2dva 4744 |
. . . . . . 7
|
64 | 57, 63 | eqtrd 2656 |
. . . . . 6
|
65 | 2, 11, 8, 44, 18, 16, 64 | dvmptadd 23723 |
. . . . 5
|
66 | | 2cnd 11093 |
. . . . 5
|
67 | | 2ne0 11113 |
. . . . . 6
|
68 | 67 | a1i 11 |
. . . . 5
|
69 | 2, 19, 20, 65, 66, 68 | dvmptdivc 23728 |
. . . 4
|
70 | | df-sin 14800 |
. . . . . 6
|
71 | 8, 16 | subcld 10392 |
. . . . . . . . . 10
|
72 | | 2cnd 11093 |
. . . . . . . . . 10
|
73 | 67 | a1i 11 |
. . . . . . . . . 10
|
74 | 71, 4, 72, 10, 73 | divdiv1d 10832 |
. . . . . . . . 9
|
75 | | 2cn 11091 |
. . . . . . . . . . 11
|
76 | 3, 75 | mulcomi 10046 |
. . . . . . . . . 10
|
77 | 76 | oveq2i 6661 |
. . . . . . . . 9
|
78 | 74, 77 | syl6eq 2672 |
. . . . . . . 8
|
79 | 8, 16, 4, 10 | divsubdird 10840 |
. . . . . . . . . 10
|
80 | 11, 17 | negsubd 10398 |
. . . . . . . . . 10
|
81 | 79, 80 | eqtr4d 2659 |
. . . . . . . . 9
|
82 | 81 | oveq1d 6665 |
. . . . . . . 8
|
83 | 78, 82 | eqtr3d 2658 |
. . . . . . 7
|
84 | 83 | mpteq2dva 4744 |
. . . . . 6
|
85 | 70, 84 | syl5eq 2668 |
. . . . 5
|
86 | 85 | oveq2d 6666 |
. . . 4
|
87 | | df-cos 14801 |
. . . . 5
|
88 | 87 | a1i 11 |
. . . 4
|
89 | 69, 86, 88 | 3eqtr4d 2666 |
. . 3
|
90 | 21, 46 | addcld 10059 |
. . . . 5
|
91 | 2, 8, 21, 39, 16, 46, 55 | dvmptadd 23723 |
. . . . 5
|
92 | 2, 20, 90, 91, 66, 68 | dvmptdivc 23728 |
. . . 4
|
93 | 88 | oveq2d 6666 |
. . . 4
|
94 | 71, 4, 10 | divcld 10801 |
. . . . . . 7
|
95 | 94, 72, 73 | divnegd 10814 |
. . . . . 6
|
96 | | sinval 14852 |
. . . . . . . . 9
|
97 | 96 | adantl 482 |
. . . . . . . 8
|
98 | 97, 78 | eqtr4d 2659 |
. . . . . . 7
|
99 | 98 | negeqd 10275 |
. . . . . 6
|
100 | 3 | negnegi 10351 |
. . . . . . . . . 10
|
101 | 100 | oveq2i 6661 |
. . . . . . . . 9
|
102 | | mulneg2 10467 |
. . . . . . . . . 10
|
103 | 71, 12, 102 | sylancl 694 |
. . . . . . . . 9
|
104 | 101, 103 | syl5eqr 2670 |
. . . . . . . 8
|
105 | | mulcl 10020 |
. . . . . . . . . . 11
|
106 | 16, 3, 105 | sylancl 694 |
. . . . . . . . . 10
|
107 | 21, 106 | negsubd 10398 |
. . . . . . . . 9
|
108 | | mulneg2 10467 |
. . . . . . . . . . 11
|
109 | 16, 3, 108 | sylancl 694 |
. . . . . . . . . 10
|
110 | 109 | oveq2d 6666 |
. . . . . . . . 9
|
111 | 8, 16, 4 | subdird 10487 |
. . . . . . . . 9
|
112 | 107, 110,
111 | 3eqtr4d 2666 |
. . . . . . . 8
|
113 | 71, 4, 10 | divrecd 10804 |
. . . . . . . . . 10
|
114 | | irec 12964 |
. . . . . . . . . . 11
|
115 | 114 | oveq2i 6661 |
. . . . . . . . . 10
|
116 | 113, 115 | syl6eq 2672 |
. . . . . . . . 9
|
117 | 116 | negeqd 10275 |
. . . . . . . 8
|
118 | 104, 112,
117 | 3eqtr4d 2666 |
. . . . . . 7
|
119 | 118 | oveq1d 6665 |
. . . . . 6
|
120 | 95, 99, 119 | 3eqtr4d 2666 |
. . . . 5
|
121 | 120 | mpteq2dva 4744 |
. . . 4
|
122 | 92, 93, 121 | 3eqtr4d 2666 |
. . 3
|
123 | 89, 122 | jca 554 |
. 2
|
124 | 123 | trud 1493 |
1
|