Step | Hyp | Ref
| Expression |
1 | | sinf 14178 |
. . . . . 6
     |
2 | 1 | a1i 11 |
. . . . 5
       |
3 | | mulcl 9623 |
. . . . . 6
 
     |
4 | | eqid 2451 |
. . . . . 6
         |
5 | 3, 4 | fmptd 6046 |
. . . . 5
           |
6 | | fcompt 6059 |
. . . . 5
       
      
            
         |
7 | 2, 5, 6 | syl2anc 667 |
. . . 4
             
         |
8 | | eqidd 2452 |
. . . . . . 7
 
  
        |
9 | | oveq2 6298 |
. . . . . . . 8
 
     |
10 | 9 | adantl 468 |
. . . . . . 7
    
      |
11 | | simpr 463 |
. . . . . . 7
 
   |
12 | | mulcl 9623 |
. . . . . . 7
 
     |
13 | 8, 10, 11, 12 | fvmptd 5954 |
. . . . . 6
 
             |
14 | 13 | fveq2d 5869 |
. . . . 5
 
      
              |
15 | 14 | mpteq2dva 4489 |
. . . 4
                         |
16 | | oveq2 6298 |
. . . . . . 7
 
     |
17 | 16 | fveq2d 5869 |
. . . . . 6
          
    |
18 | 17 | cbvmptv 4495 |
. . . . 5
                 |
19 | 18 | a1i 11 |
. . . 4
                   |
20 | 7, 15, 19 | 3eqtrrd 2490 |
. . 3
                 |
21 | 20 | oveq2d 6306 |
. 2
      
              |
22 | | cnelprrecn 9632 |
. . . 4
    |
23 | 22 | a1i 11 |
. . 3
      |
24 | | dvsin 22934 |
. . . . . 6
   |
25 | 24 | dmeqi 5036 |
. . . . 5
   |
26 | | cosf 14179 |
. . . . . 6
     |
27 | 26 | fdmi 5734 |
. . . . 5
 |
28 | 25, 27 | eqtri 2473 |
. . . 4
   |
29 | 28 | a1i 11 |
. . 3
 
   |
30 | | id 22 |
. . . . . . . . . . 11
   |
31 | 30 | cbvmptv 4495 |
. . . . . . . . . 10
     |
32 | 31 | oveq2i 6301 |
. . . . . . . . 9
                   |
33 | 32 | a1i 11 |
. . . . . . . 8
                     |
34 | | cnex 9620 |
. . . . . . . . . . 11
 |
35 | 34 | a1i 11 |
. . . . . . . . . 10
   |
36 | | snex 4641 |
. . . . . . . . . . 11
 
 |
37 | 36 | a1i 11 |
. . . . . . . . . 10
  
  |
38 | | xpexg 6593 |
. . . . . . . . . 10
           |
39 | 35, 37, 38 | syl2anc 667 |
. . . . . . . . 9
       |
40 | 34 | mptex 6136 |
. . . . . . . . . 10
   |
41 | 40 | a1i 11 |
. . . . . . . . 9
     |
42 | | offval3 6787 |
. . . . . . . . 9
                                              |
43 | 39, 41, 42 | syl2anc 667 |
. . . . . . . 8
               
                      |
44 | | fconst6g 5772 |
. . . . . . . . . . . . 13
           |
45 | | fdm 5733 |
. . . . . . . . . . . . 13
        
      |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
 
     |
47 | | eqid 2451 |
. . . . . . . . . . . . . . 15
     |
48 | | id 22 |
. . . . . . . . . . . . . . 15
   |
49 | 47, 48 | fmpti 6045 |
. . . . . . . . . . . . . 14
       |
50 | 49 | fdmi 5734 |
. . . . . . . . . . . . 13
   |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
 
   |
52 | 46, 51 | ineq12d 3635 |
. . . . . . . . . . 11
      
      |
53 | | inidm 3641 |
. . . . . . . . . . . 12
   |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
     |
55 | 52, 54 | eqtrd 2485 |
. . . . . . . . . 10
      
    |
56 | 55 | mpteq1d 4484 |
. . . . . . . . 9
       
                                       |
57 | | fvconst2g 6118 |
. . . . . . . . . . 11
 
           |
58 | | eqidd 2452 |
. . . . . . . . . . . . 13
       |
59 | | simpr 463 |
. . . . . . . . . . . . 13
 
   |
60 | | id 22 |
. . . . . . . . . . . . 13
   |
61 | 58, 59, 60, 60 | fvmptd 5954 |
. . . . . . . . . . . 12
         |
62 | 61 | adantl 468 |
. . . . . . . . . . 11
 
         |
63 | 57, 62 | oveq12d 6308 |
. . . . . . . . . 10
 
                     |
64 | 63 | mpteq2dva 4489 |
. . . . . . . . 9
                    
    |
65 | 56, 64 | eqtrd 2485 |
. . . . . . . 8
       
                    
    |
66 | 33, 43, 65 | 3eqtrrd 2490 |
. . . . . . 7
                |
67 | 66 | oveq2d 6306 |
. . . . . 6
                    |
68 | | eqid 2451 |
. . . . . . . . 9
     |
69 | 68, 60 | fmpti 6045 |
. . . . . . . 8
       |
70 | 69 | a1i 11 |
. . . . . . 7
         |
71 | | id 22 |
. . . . . . 7
   |
72 | 22 | a1i 11 |
. . . . . . . . . . . 12
     |
73 | 72 | dvmptid 22911 |
. . . . . . . . . . 11
        |
74 | 73 | trud 1453 |
. . . . . . . . . 10
       |
75 | 74 | dmeqi 5036 |
. . . . . . . . 9
       |
76 | | ax-1cn 9597 |
. . . . . . . . . . . 12
 |
77 | 76 | rgenw 2749 |
. . . . . . . . . . 11
  |
78 | | eqid 2451 |
. . . . . . . . . . . 12
     |
79 | 78 | fmpt 6043 |
. . . . . . . . . . 11
 
        |
80 | 77, 79 | mpbi 212 |
. . . . . . . . . 10
       |
81 | 80 | fdmi 5734 |
. . . . . . . . 9
   |
82 | 75, 81 | eqtri 2473 |
. . . . . . . 8
     |
83 | 82 | a1i 11 |
. . . . . . 7
 
     |
84 | 23, 70, 71, 83 | dvcmulf 22899 |
. . . . . 6
                         |
85 | 67, 84 | eqtrd 2485 |
. . . . 5
                    |
86 | 85 | dmeqd 5037 |
. . . 4
 
                  |
87 | | ovex 6318 |
. . . . . . 7
     |
88 | 87 | a1i 11 |
. . . . . 6
       |
89 | | offval3 6787 |
. . . . . 6
                                                      |
90 | 39, 88, 89 | syl2anc 667 |
. . . . 5
                 
                          |
91 | 90 | dmeqd 5037 |
. . . 4
                  
                         |
92 | 46, 83 | ineq12d 3635 |
. . . . . . . 8
      
        |
93 | 92, 54 | eqtrd 2485 |
. . . . . . 7
      
      |
94 | 93 | mpteq1d 4484 |
. . . . . 6
       
                                             |
95 | 94 | dmeqd 5037 |
. . . . 5
 
     
                                             |
96 | | eqid 2451 |
. . . . . 6
                                         |
97 | | fvconst2g 6118 |
. . . . . . . 8
 
           |
98 | 74 | fveq1i 5866 |
. . . . . . . . . . 11
               |
99 | 98 | a1i 11 |
. . . . . . . . . 10
                 |
100 | | eqidd 2452 |
. . . . . . . . . . 11
       |
101 | | eqidd 2452 |
. . . . . . . . . . 11
 
   |
102 | 76 | a1i 11 |
. . . . . . . . . . 11
   |
103 | 100, 101,
48, 102 | fvmptd 5954 |
. . . . . . . . . 10
         |
104 | 99, 103 | eqtrd 2485 |
. . . . . . . . 9
           |
105 | 104 | adantl 468 |
. . . . . . . 8
 
           |
106 | 97, 105 | oveq12d 6308 |
. . . . . . 7
 
                       |
107 | | mulcl 9623 |
. . . . . . . . 9
 
     |
108 | 76, 107 | mpan2 677 |
. . . . . . . 8
 
   |
109 | 108 | adantr 467 |
. . . . . . 7
 
     |
110 | 106, 109 | eqeltrd 2529 |
. . . . . 6
 
                     |
111 | 96, 110 | dmmptd 5708 |
. . . . 5
 
                     |
112 | 95, 111 | eqtrd 2485 |
. . . 4
 
     
                         |
113 | 86, 91, 112 | 3eqtrd 2489 |
. . 3
 
       |
114 | 23, 23, 2, 5, 29, 113 | dvcof 22902 |
. 2
    
         
             |
115 | 24 | a1i 11 |
. . . . . 6
     |
116 | | coscn 23400 |
. . . . . . 7
     |
117 | 116 | a1i 11 |
. . . . . 6
       |
118 | 115, 117 | eqeltrd 2529 |
. . . . 5
         |
119 | 34 | mptex 6136 |
. . . . . 6
     |
120 | 119 | a1i 11 |
. . . . 5
       |
121 | | coexg 6744 |
. . . . 5
   
           
       |
122 | 118, 120,
121 | syl2anc 667 |
. . . 4
   
       |
123 | | simpl 459 |
. . . . . . 7
 
   |
124 | | 0cnd 9636 |
. . . . . . 7
 
   |
125 | 23, 71 | dvmptc 22912 |
. . . . . . 7
         |
126 | | simpr 463 |
. . . . . . 7
 
   |
127 | 76 | a1i 11 |
. . . . . . 7
 
   |
128 | 74 | a1i 11 |
. . . . . . 7
         |
129 | 23, 123, 124, 125, 126, 127, 128 | dvmptmul 22915 |
. . . . . 6
                 |
130 | 126 | mul02d 9831 |
. . . . . . . . 9
 
     |
131 | 123 | mulid2d 9661 |
. . . . . . . . 9
 
     |
132 | 130, 131 | oveq12d 6308 |
. . . . . . . 8
 
           |
133 | 123 | addid2d 9834 |
. . . . . . . 8
 
     |
134 | 132, 133 | eqtrd 2485 |
. . . . . . 7
 
         |
135 | 134 | mpteq2dva 4489 |
. . . . . 6
             |
136 | 129, 135 | eqtrd 2485 |
. . . . 5
           |
137 | 34 | mptex 6136 |
. . . . . 6
   |
138 | 137 | a1i 11 |
. . . . 5
     |
139 | 136, 138 | eqeltrd 2529 |
. . . 4
         |
140 | | offval3 6787 |
. . . 4
    
                 
               
    
  
          
                    |
141 | 122, 139,
140 | syl2anc 667 |
. . 3
    
        
          
     
          
                    |
142 | | frn 5735 |
. . . . . . . . . 10
          
    |
143 | 5, 142 | syl 17 |
. . . . . . . . 9
  
    |
144 | 143, 29 | sseqtr4d 3469 |
. . . . . . . 8
  
  
   |
145 | | dmcosseq 5096 |
. . . . . . . 8
  
  
          
    |
146 | 144, 145 | syl 17 |
. . . . . . 7
   
      
    |
147 | | ovex 6318 |
. . . . . . . . 9
   |
148 | 147, 4 | dmmpti 5707 |
. . . . . . . 8
     |
149 | 148 | a1i 11 |
. . . . . . 7
  
    |
150 | 146, 149 | eqtrd 2485 |
. . . . . 6
   
       |
151 | 150, 113 | ineq12d 3635 |
. . . . 5
    
     
          |
152 | 151, 54 | eqtrd 2485 |
. . . 4
    
     
        |
153 | 152 | mpteq1d 4484 |
. . 3
     
     
                                                           |
154 | 12 | coscld 14185 |
. . . . . 6
 
    
    |
155 | | simpl 459 |
. . . . . 6
 
   |
156 | 154, 155 | mulcomd 9664 |
. . . . 5
 
     
             |
157 | 156 | mpteq2dva 4489 |
. . . 4
      
         
      |
158 | 24 | coeq1i 4994 |
. . . . . . . . 9
    
          |
159 | 158 | a1i 11 |
. . . . . . . 8
 
   
             |
160 | 159 | fveq1d 5867 |
. . . . . . 7
 
                         |
161 | | ffun 5731 |
. . . . . . . . . 10
          
    |
162 | 5, 161 | syl 17 |
. . . . . . . . 9
  
    |
163 | 162 | adantr 467 |
. . . . . . . 8
 
       |
164 | 11, 148 | syl6eleqr 2540 |
. . . . . . . 8
 
       |
165 | | fvco 5941 |
. . . . . . . 8
     
    
               
        |
166 | 163, 164,
165 | syl2anc 667 |
. . . . . . 7
 
    
                    |
167 | 13 | fveq2d 5869 |
. . . . . . 7
 
      
              |
168 | 160, 166,
167 | 3eqtrd 2489 |
. . . . . 6
 
                     |
169 | 136 | adantr 467 |
. . . . . . 7
 
           |
170 | | eqidd 2452 |
. . . . . . 7
    
  |
171 | 169, 170,
11, 155 | fvmptd 5954 |
. . . . . 6
 
    
        |
172 | 168, 171 | oveq12d 6308 |
. . . . 5
 
       
                     
     |
173 | 172 | mpteq2dva 4489 |
. . . 4
                                
      |
174 | 9 | fveq2d 5869 |
. . . . . . 7
          
    |
175 | 174 | oveq2d 6306 |
. . . . . 6
 
                 |
176 | 175 | cbvmptv 4495 |
. . . . 5
     
     
         |
177 | 176 | a1i 11 |
. . . 4
                       |
178 | 157, 173,
177 | 3eqtr4d 2495 |
. . 3
                                       |
179 | 141, 153,
178 | 3eqtrd 2489 |
. 2
    
        
                |
180 | 21, 114, 179 | 3eqtrd 2489 |
1
      
     
          |