Proof of Theorem sqwvfoura
Step | Hyp | Ref
| Expression |
1 | | pire 23492 |
. . . . . 6
 |
2 | 1 | renegcli 9955 |
. . . . 5
  |
3 | 2 | a1i 11 |
. . . 4
    |
4 | 1 | a1i 11 |
. . . 4
   |
5 | | 0re 9661 |
. . . . . 6
 |
6 | | negpilt0 37580 |
. . . . . . 7
  |
7 | 2, 5, 6 | ltleii 9775 |
. . . . . 6
  |
8 | | pipos 23494 |
. . . . . . 7
 |
9 | 5, 1, 8 | ltleii 9775 |
. . . . . 6
 |
10 | 2, 1 | elicc2i 11725 |
. . . . . 6
    ![[,] [,]](_icc.gif) 
     |
11 | 5, 7, 9, 10 | mpbir3an 1212 |
. . . . 5
   ![[,] [,]](_icc.gif)   |
12 | 11 | a1i 11 |
. . . 4
    ![[,] [,]](_icc.gif)    |
13 | | 1red 9676 |
. . . . . . . . . . 11
   |
14 | 13 | renegcld 10067 |
. . . . . . . . . . 11
    |
15 | 13, 14 | ifcld 3915 |
. . . . . . . . . 10
           |
16 | 15 | adantl 473 |
. . . . . . . . 9
 

   
      |
17 | | sqwvfoura.f |
. . . . . . . . 9
           |
18 | 16, 17 | fmptd 6061 |
. . . . . . . 8
       |
19 | 18 | adantr 472 |
. . . . . . 7
 
            |
20 | | elioore 11691 |
. . . . . . . 8
        |
21 | 20 | adantl 473 |
. . . . . . 7
 
        |
22 | 19, 21 | ffvelrnd 6038 |
. . . . . 6
 
            |
23 | | sqwvfoura.n |
. . . . . . . . . 10
   |
24 | 23 | nn0red 10950 |
. . . . . . . . 9
   |
25 | 24 | adantr 472 |
. . . . . . . 8
 
        |
26 | 25, 21 | remulcld 9689 |
. . . . . . 7
 
      
   |
27 | 26 | recoscld 14275 |
. . . . . 6
 
              |
28 | 22, 27 | remulcld 9689 |
. . . . 5
 
                    |
29 | 28 | recnd 9687 |
. . . 4
 
                    |
30 | | elioore 11691 |
. . . . . . . . . 10
        |
31 | 30, 15 | syl 17 |
. . . . . . . . . 10
                |
32 | 17 | fvmpt2 5972 |
. . . . . . . . . 10
                         |
33 | 30, 31, 32 | syl2anc 673 |
. . . . . . . . 9
                    |
34 | 1 | a1i 11 |
. . . . . . . . . . 11
        |
35 | | sqwvfoura.t |
. . . . . . . . . . . . . 14
   |
36 | | 2rp 11330 |
. . . . . . . . . . . . . . 15
 |
37 | | pirp 23495 |
. . . . . . . . . . . . . . 15
 |
38 | | rpmulcl 11347 |
. . . . . . . . . . . . . . 15
       |
39 | 36, 37, 38 | mp2an 686 |
. . . . . . . . . . . . . 14
   |
40 | 35, 39 | eqeltri 2545 |
. . . . . . . . . . . . 13
 |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
        |
42 | 30, 41 | modcld 12135 |
. . . . . . . . . . 11
      
   |
43 | | picn 23493 |
. . . . . . . . . . . . . . . . 17
 |
44 | 43 | 2timesi 10753 |
. . . . . . . . . . . . . . . 16
     |
45 | 35, 44 | eqtri 2493 |
. . . . . . . . . . . . . . 15
   |
46 | 45 | oveq2i 6319 |
. . . . . . . . . . . . . 14
     
   |
47 | 2 | recni 9673 |
. . . . . . . . . . . . . . 15
  |
48 | 47, 43, 43 | addassi 9669 |
. . . . . . . . . . . . . 14
   
       |
49 | 43 | negidi 9963 |
. . . . . . . . . . . . . . . . 17
    |
50 | 43, 47, 49 | addcomli 9843 |
. . . . . . . . . . . . . . . 16
    |
51 | 50 | oveq1i 6318 |
. . . . . . . . . . . . . . 15
   
    |
52 | 43 | addid2i 9839 |
. . . . . . . . . . . . . . 15
   |
53 | 51, 52 | eqtri 2493 |
. . . . . . . . . . . . . 14
   
  |
54 | 46, 48, 53 | 3eqtr2ri 2500 |
. . . . . . . . . . . . 13
    |
55 | 2 | a1i 11 |
. . . . . . . . . . . . . 14
         |
56 | | 2re 10701 |
. . . . . . . . . . . . . . . . 17
 |
57 | 56, 1 | remulcli 9675 |
. . . . . . . . . . . . . . . 16
   |
58 | 35, 57 | eqeltri 2545 |
. . . . . . . . . . . . . . 15
 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
        |
60 | 2 | rexri 9711 |
. . . . . . . . . . . . . . . 16
  |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . 15
         |
62 | | 0red 9662 |
. . . . . . . . . . . . . . . 16
        |
63 | 62 | rexrd 9708 |
. . . . . . . . . . . . . . 15
        |
64 | | id 22 |
. . . . . . . . . . . . . . 15
             |
65 | | ioogtlb 37688 |
. . . . . . . . . . . . . . 15
            |
66 | 61, 63, 64, 65 | syl3anc 1292 |
. . . . . . . . . . . . . 14
         |
67 | 55, 30, 59, 66 | ltadd1dd 10245 |
. . . . . . . . . . . . 13
             |
68 | 54, 67 | syl5eqbr 4429 |
. . . . . . . . . . . 12
          |
69 | 58 | recni 9673 |
. . . . . . . . . . . . . . . . 17
 |
70 | 69 | mulid2i 9664 |
. . . . . . . . . . . . . . . 16
   |
71 | 70 | eqcomi 2480 |
. . . . . . . . . . . . . . 15
   |
72 | 71 | oveq2i 6319 |
. . . . . . . . . . . . . 14
       |
73 | 72 | oveq1i 6318 |
. . . . . . . . . . . . 13
           |
74 | 30, 59 | readdcld 9688 |
. . . . . . . . . . . . . 14
          |
75 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
        |
76 | 62, 34, 74, 75, 68 | lttrd 9813 |
. . . . . . . . . . . . . . 15
          |
77 | 62, 74, 76 | ltled 9800 |
. . . . . . . . . . . . . 14
          |
78 | | iooltub 37706 |
. . . . . . . . . . . . . . . . 17
           |
79 | 61, 63, 64, 78 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
        |
80 | 30, 62, 59, 79 | ltadd1dd 10245 |
. . . . . . . . . . . . . . 15
            |
81 | 69 | a1i 11 |
. . . . . . . . . . . . . . . 16
        |
82 | 81 | addid2d 9852 |
. . . . . . . . . . . . . . 15
          |
83 | 80, 82 | breqtrd 4420 |
. . . . . . . . . . . . . 14
          |
84 | | modid 12154 |
. . . . . . . . . . . . . 14
               
     |
85 | 74, 41, 77, 83, 84 | syl22anc 1293 |
. . . . . . . . . . . . 13
        
     |
86 | | 1zzd 10992 |
. . . . . . . . . . . . . 14
        |
87 | | modcyc 12165 |
. . . . . . . . . . . . . 14
 
           |
88 | 30, 41, 86, 87 | syl3anc 1292 |
. . . . . . . . . . . . 13
                |
89 | 73, 85, 88 | 3eqtr3a 2529 |
. . . . . . . . . . . 12
            |
90 | 68, 89 | breqtrd 4420 |
. . . . . . . . . . 11
          |
91 | 34, 42, 90 | ltnsymd 9801 |
. . . . . . . . . 10
      
   |
92 | 91 | iffalsed 3883 |
. . . . . . . . 9
                 |
93 | 33, 92 | eqtrd 2505 |
. . . . . . . 8
             |
94 | 93 | oveq1d 6323 |
. . . . . . 7
                       
     |
95 | 94 | adantl 473 |
. . . . . 6
 
                       
     |
96 | 95 | mpteq2dva 4482 |
. . . . 5
               
               
      |
97 | | 1cnd 9677 |
. . . . . . 7
   |
98 | 97 | negcld 9992 |
. . . . . 6
    |
99 | 24 | adantr 472 |
. . . . . . . 8
 
        |
100 | 30 | adantl 473 |
. . . . . . . 8
 
        |
101 | 99, 100 | remulcld 9689 |
. . . . . . 7
 
      
   |
102 | 101 | recoscld 14275 |
. . . . . 6
 
              |
103 | | ioossicc 11745 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)   |
104 | 103 | a1i 11 |
. . . . . . 7
         ![[,] [,]](_icc.gif)    |
105 | | ioombl 22597 |
. . . . . . . 8
      |
106 | 105 | a1i 11 |
. . . . . . 7
        |
107 | 24 | adantr 472 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)     |
108 | | iccssre 11741 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)    |
109 | 2, 5, 108 | mp2an 686 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)   |
110 | 109 | sseli 3414 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    |
111 | 110 | adantl 473 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)     |
112 | 107, 111 | remulcld 9689 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)   
   |
113 | 112 | recoscld 14275 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)           |
114 | | 0red 9662 |
. . . . . . . 8
   |
115 | | coscn 23479 |
. . . . . . . . . 10
     |
116 | 115 | a1i 11 |
. . . . . . . . 9
       |
117 | | ax-resscn 9614 |
. . . . . . . . . . . . 13
 |
118 | 109, 117 | sstri 3427 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)   |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)    |
120 | 24 | recnd 9687 |
. . . . . . . . . . 11
   |
121 | | ssid 3437 |
. . . . . . . . . . . 12
 |
122 | 121 | a1i 11 |
. . . . . . . . . . 11

  |
123 | 119, 120,
122 | constcncfg 37845 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       |
124 | 119, 122 | idcncfg 37846 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       |
125 | 123, 124 | mulcncf 22476 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       |
126 | 116, 125 | cncfmpt1f 22023 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)       |
127 | | cniccibl 22877 |
. . . . . . . 8
   
   ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)            |
128 | 3, 114, 126, 127 | syl3anc 1292 |
. . . . . . 7
     ![[,] [,]](_icc.gif)     
      |
129 | 104, 106,
113, 128 | iblss 22841 |
. . . . . 6
          
      |
130 | 98, 102, 129 | iblmulc2 22867 |
. . . . 5
            
       |
131 | 96, 130 | eqeltrd 2549 |
. . . 4
               
       |
132 | | elioore 11691 |
. . . . . . . . . 10
       |
133 | 132, 15 | syl 17 |
. . . . . . . . . 10
               |
134 | 132, 133,
32 | syl2anc 673 |
. . . . . . . . 9
                   |
135 | 40 | a1i 11 |
. . . . . . . . . . . 12
       |
136 | | 0red 9662 |
. . . . . . . . . . . . 13
       |
137 | 136 | rexrd 9708 |
. . . . . . . . . . . . . 14
       |
138 | 1 | rexri 9711 |
. . . . . . . . . . . . . . 15
 |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
       |
140 | | id 22 |
. . . . . . . . . . . . . 14
           |
141 | | ioogtlb 37688 |
. . . . . . . . . . . . . 14
         |
142 | 137, 139,
140, 141 | syl3anc 1292 |
. . . . . . . . . . . . 13
       |
143 | 136, 132,
142 | ltled 9800 |
. . . . . . . . . . . 12
       |
144 | 1 | a1i 11 |
. . . . . . . . . . . . 13
       |
145 | 58 | a1i 11 |
. . . . . . . . . . . . 13
       |
146 | | iooltub 37706 |
. . . . . . . . . . . . . 14
         |
147 | 137, 139,
140, 146 | syl3anc 1292 |
. . . . . . . . . . . . 13
       |
148 | | 2timesgt 37590 |
. . . . . . . . . . . . . . . 16

    |
149 | 37, 148 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   |
150 | 149, 35 | breqtrri 4421 |
. . . . . . . . . . . . . 14
 |
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
       |
152 | 132, 144,
145, 147, 151 | lttrd 9813 |
. . . . . . . . . . . 12
       |
153 | | modid 12154 |
. . . . . . . . . . . 12
    
 
    |
154 | 132, 135,
143, 152, 153 | syl22anc 1293 |
. . . . . . . . . . 11
     
   |
155 | 154, 147 | eqbrtrd 4416 |
. . . . . . . . . 10
     
   |
156 | 155 | iftrued 3880 |
. . . . . . . . 9
               |
157 | 134, 156 | eqtrd 2505 |
. . . . . . . 8
           |
158 | 157 | oveq1d 6323 |
. . . . . . 7
                           |
159 | 158 | adantl 473 |
. . . . . 6
 
                           |
160 | 159 | mpteq2dva 4482 |
. . . . 5
                            
      |
161 | 24 | adantr 472 |
. . . . . . . 8
 
       |
162 | 132 | adantl 473 |
. . . . . . . 8
 
       |
163 | 161, 162 | remulcld 9689 |
. . . . . . 7
 
     
   |
164 | 163 | recoscld 14275 |
. . . . . 6
 
             |
165 | | ioossicc 11745 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)   |
166 | 165 | a1i 11 |
. . . . . . 7
       ![[,] [,]](_icc.gif)    |
167 | | ioombl 22597 |
. . . . . . . 8
     |
168 | 167 | a1i 11 |
. . . . . . 7
    
  |
169 | 24 | adantr 472 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)     |
170 | | iccssre 11741 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    |
171 | 5, 1, 170 | mp2an 686 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)   |
172 | 171 | sseli 3414 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
173 | 172 | adantl 473 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)     |
174 | 169, 173 | remulcld 9689 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)   
   |
175 | 174 | recoscld 14275 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)           |
176 | 171, 117 | sstri 3427 |
. . . . . . . . . . . 12
  ![[,] [,]](_icc.gif)   |
177 | 176 | a1i 11 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
178 | 177, 120,
122 | constcncfg 37845 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
179 | 177, 122 | idcncfg 37846 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
180 | 178, 179 | mulcncf 22476 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
181 | 116, 180 | cncfmpt1f 22023 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)     
      ![[,] [,]](_icc.gif)       |
182 | | cniccibl 22877 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
      |
183 | 114, 4, 181, 182 | syl3anc 1292 |
. . . . . . 7
    ![[,] [,]](_icc.gif)     
      |
184 | 166, 168,
175, 183 | iblss 22841 |
. . . . . 6
         
      |
185 | 97, 164, 184 | iblmulc2 22867 |
. . . . 5
                  |
186 | 160, 185 | eqeltrd 2549 |
. . . 4
                      |
187 | 3, 4, 12, 29, 131, 186 | itgsplitioo 22874 |
. . 3
                
                    
                          |
188 | 187 | oveq1d 6323 |
. 2
                                        
                           |
189 | 95 | itgeq2dv 22818 |
. . . . 5
                
                       |
190 | 98, 102, 129 | itgmulc2 22870 |
. . . . 5
                              
      |
191 | | oveq1 6315 |
. . . . . . . . . . . . . 14
 
     |
192 | | ioosscn 37687 |
. . . . . . . . . . . . . . . 16
      |
193 | 192 | sseli 3414 |
. . . . . . . . . . . . . . 15
        |
194 | 193 | mul02d 9849 |
. . . . . . . . . . . . . 14
          |
195 | 191, 194 | sylan9eq 2525 |
. . . . . . . . . . . . 13
            |
196 | 195 | fveq2d 5883 |
. . . . . . . . . . . 12
           
        |
197 | | cos0 14281 |
. . . . . . . . . . . 12
     |
198 | 196, 197 | syl6eq 2521 |
. . . . . . . . . . 11
           
    |
199 | 198 | adantll 728 |
. . . . . . . . . 10
   
         
    |
200 | 199 | itgeq2dv 22818 |
. . . . . . . . 9
 
           
             |
201 | | ioovolcl 22601 |
. . . . . . . . . . . . 13
               |
202 | 2, 5, 201 | mp2an 686 |
. . . . . . . . . . . 12
          |
203 | 202 | a1i 11 |
. . . . . . . . . . 11
            |
204 | | itgconst 22855 |
. . . . . . . . . . 11
               
                      |
205 | 106, 203,
97, 204 | syl3anc 1292 |
. . . . . . . . . 10
                      |
206 | 205 | adantr 472 |
. . . . . . . . 9
 
                      |
207 | | volioo 37922 |
. . . . . . . . . . . . . . 15
   
               |
208 | 2, 5, 7, 207 | mp3an 1390 |
. . . . . . . . . . . . . 14
             |
209 | | 0cn 9653 |
. . . . . . . . . . . . . . 15
 |
210 | 209, 43 | subnegi 9973 |
. . . . . . . . . . . . . 14
      |
211 | 208, 210,
52 | 3eqtri 2497 |
. . . . . . . . . . . . 13
          |
212 | 211 | a1i 11 |
. . . . . . . . . . . 12
            |
213 | 212 | oveq2d 6324 |
. . . . . . . . . . 11
                |
214 | 43 | a1i 11 |
. . . . . . . . . . . 12
   |
215 | 214 | mulid2d 9679 |
. . . . . . . . . . 11
  
  |
216 | 213, 215 | eqtrd 2505 |
. . . . . . . . . 10
              |
217 | 216 | adantr 472 |
. . . . . . . . 9
 
              |
218 | 200, 206,
217 | 3eqtrd 2509 |
. . . . . . . 8
 
           
     |
219 | 218 | oveq2d 6324 |
. . . . . . 7
 
             
         |
220 | 43 | mulm1i 10084 |
. . . . . . . 8
     |
221 | 220 | a1i 11 |
. . . . . . 7
 
       |
222 | | iftrue 3878 |
. . . . . . . . 9
  
       |
223 | 222 | eqcomd 2477 |
. . . . . . . 8
          |
224 | 223 | adantl 473 |
. . . . . . 7
 
          |
225 | 219, 221,
224 | 3eqtrd 2509 |
. . . . . 6
 
             
        
   |
226 | 24 | adantr 472 |
. . . . . . . 8
 

  |
227 | 23 | nn0ge0d 10952 |
. . . . . . . . 9

  |
228 | 227 | adantr 472 |
. . . . . . . 8
 

  |
229 | | neqne 2651 |
. . . . . . . . 9
   |
230 | 229 | adantl 473 |
. . . . . . . 8
 
   |
231 | 226, 228,
230 | ne0gt0d 9789 |
. . . . . . 7
 

  |
232 | | 1cnd 9677 |
. . . . . . . . . 10
 

  |
233 | 232 | negcld 9992 |
. . . . . . . . 9
 

   |
234 | 233 | mul01d 9850 |
. . . . . . . 8
 

     |
235 | 120 | adantr 472 |
. . . . . . . . . . 11
 

  |
236 | 2 | a1i 11 |
. . . . . . . . . . 11
 

   |
237 | | 0red 9662 |
. . . . . . . . . . 11
 

  |
238 | 7 | a1i 11 |
. . . . . . . . . . 11
 

   |
239 | | simpr 468 |
. . . . . . . . . . . 12
 

  |
240 | 239 | gt0ne0d 10199 |
. . . . . . . . . . 11
 

  |
241 | 235, 236,
237, 238, 240 | itgcoscmulx 37943 |
. . . . . . . . . 10
 

          
                      |
242 | 120 | mul01d 9850 |
. . . . . . . . . . . . . . . 16
     |
243 | 242 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
    
        |
244 | | sin0 14280 |
. . . . . . . . . . . . . . 15
     |
245 | 243, 244 | syl6eq 2521 |
. . . . . . . . . . . . . 14
    
    |
246 | 120, 214 | mulneg2d 10093 |
. . . . . . . . . . . . . . . 16
   
     |
247 | 246 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
    
            |
248 | 120, 214 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
  
  |
249 | | sinneg 14277 |
. . . . . . . . . . . . . . . 16
                   |
250 | 248, 249 | syl 17 |
. . . . . . . . . . . . . . 15
     
           |
251 | 247, 250 | eqtrd 2505 |
. . . . . . . . . . . . . 14
    
            |
252 | 245, 251 | oveq12d 6326 |
. . . . . . . . . . . . 13
     
                     |
253 | | 0cnd 9654 |
. . . . . . . . . . . . . 14
   |
254 | 248 | sincld 14261 |
. . . . . . . . . . . . . 14
    
    |
255 | 253, 254 | subnegd 10012 |
. . . . . . . . . . . . 13
                    |
256 | 254 | addid2d 9852 |
. . . . . . . . . . . . 13
                 |
257 | 252, 255,
256 | 3eqtrd 2509 |
. . . . . . . . . . . 12
     
             
    |
258 | 257 | adantr 472 |
. . . . . . . . . . 11
 

                       |
259 | 258 | oveq1d 6323 |
. . . . . . . . . 10
 

     
               
     |
260 | 23 | nn0zd 11061 |
. . . . . . . . . . . . . 14
   |
261 | | sinkpi 23553 |
. . . . . . . . . . . . . 14
         |
262 | 260, 261 | syl 17 |
. . . . . . . . . . . . 13
    
    |
263 | 262 | oveq1d 6323 |
. . . . . . . . . . . 12
     
       |
264 | 263 | adantr 472 |
. . . . . . . . . . 11
 

            |
265 | 235, 240 | div0d 10404 |
. . . . . . . . . . 11
 

    |
266 | 264, 265 | eqtrd 2505 |
. . . . . . . . . 10
 

          |
267 | 241, 259,
266 | 3eqtrd 2509 |
. . . . . . . . 9
 

          
     |
268 | 267 | oveq2d 6324 |
. . . . . . . 8
 

                      |
269 | 240 | neneqd 2648 |
. . . . . . . . 9
 

  |
270 | 269 | iffalsed 3883 |
. . . . . . . 8
 

 
      |
271 | 234, 268,
270 | 3eqtr4d 2515 |
. . . . . . 7
 

                         |
272 | 231, 271 | syldan 478 |
. . . . . 6
 
             
        
   |
273 | 225, 272 | pm2.61dan 808 |
. . . . 5
                          |
274 | 189, 190,
273 | 3eqtr2d 2511 |
. . . 4
                
        
   |
275 | 159 | itgeq2dv 22818 |
. . . . 5
               
                     |
276 | 97, 164, 184 | itgmulc2 22870 |
. . . . 5
           
                     |
277 | 164, 184 | itgcl 22820 |
. . . . . . 7
                |
278 | 277 | mulid2d 9679 |
. . . . . 6
           
                   |
279 | | simpl 464 |
. . . . . . . . . . . . . 14
         |
280 | 279 | oveq1d 6323 |
. . . . . . . . . . . . 13
             |
281 | 132 | recnd 9687 |
. . . . . . . . . . . . . . 15
       |
282 | 281 | adantl 473 |
. . . . . . . . . . . . . 14
         |
283 | 282 | mul02d 9849 |
. . . . . . . . . . . . 13
           |
284 | 280, 283 | eqtrd 2505 |
. . . . . . . . . . . 12
           |
285 | 284 | fveq2d 5883 |
. . . . . . . . . . 11
          
        |
286 | 285, 197 | syl6eq 2521 |
. . . . . . . . . 10
          
    |
287 | 286 | adantll 728 |
. . . . . . . . 9
   
        
    |
288 | 287 | itgeq2dv 22818 |
. . . . . . . 8
 
          
            |
289 | | ioovolcl 22601 |
. . . . . . . . . . 11
             |
290 | 5, 1, 289 | mp2an 686 |
. . . . . . . . . 10
         |
291 | | ax-1cn 9615 |
. . . . . . . . . 10
 |
292 | | itgconst 22855 |
. . . . . . . . . 10
     
                            |
293 | 167, 290,
291, 292 | mp3an 1390 |
. . . . . . . . 9
                  |
294 | 293 | a1i 11 |
. . . . . . . 8
 
                    |
295 | 43 | mulid2i 9664 |
. . . . . . . . . 10
   |
296 | | volioo 37922 |
. . . . . . . . . . . . . 14
               |
297 | 5, 1, 9, 296 | mp3an 1390 |
. . . . . . . . . . . . 13
           |
298 | 43 | subid1i 9966 |
. . . . . . . . . . . . 13
   |
299 | 297, 298 | eqtri 2493 |
. . . . . . . . . . . 12
         |
300 | 299 | oveq2i 6319 |
. . . . . . . . . . 11
             |
301 | 300 | a1i 11 |
. . . . . . . . . 10
               |
302 | | iftrue 3878 |
. . . . . . . . . 10
  
     |
303 | 295, 301,
302 | 3eqtr4a 2531 |
. . . . . . . . 9
                  |
304 | 303 | adantl 473 |
. . . . . . . 8
 
                  |
305 | 288, 294,
304 | 3eqtrd 2509 |
. . . . . . 7
 
          
          |
306 | 262, 245 | oveq12d 6326 |
. . . . . . . . . . . . 13
     
             |
307 | 253 | subidd 9993 |
. . . . . . . . . . . . 13
     |
308 | 306, 307 | eqtrd 2505 |
. . . . . . . . . . . 12
     
           |
309 | 308 | oveq1d 6323 |
. . . . . . . . . . 11
                     |
310 | 309 | adantr 472 |
. . . . . . . . . 10
 

     
              |
311 | 310, 265 | eqtrd 2505 |
. . . . . . . . 9
 

     
            |
312 | 1 | a1i 11 |
. . . . . . . . . 10
 

  |
313 | 9 | a1i 11 |
. . . . . . . . . 10
 

  |
314 | 235, 237,
312, 313, 240 | itgcoscmulx 37943 |
. . . . . . . . 9
 

         
                     |
315 | 269 | iffalsed 3883 |
. . . . . . . . 9
 

 
 
   |
316 | 311, 314,
315 | 3eqtr4d 2515 |
. . . . . . . 8
 

         
          |
317 | 231, 316 | syldan 478 |
. . . . . . 7
 
          
          |
318 | 305, 317 | pm2.61dan 808 |
. . . . . 6
                     |
319 | 278, 318 | eqtrd 2505 |
. . . . 5
           
           |
320 | 275, 276,
319 | 3eqtr2d 2511 |
. . . 4
               
           |
321 | 274, 320 | oveq12d 6326 |
. . 3
                                               
         |
322 | 321 | oveq1d 6323 |
. 2
                  
                        
                 |
323 | 222, 302 | oveq12d 6326 |
. . . . . . 7
                   |
324 | 323, 50 | syl6eq 2521 |
. . . . . 6
                |
325 | | iffalse 3881 |
. . . . . . . 8
         |
326 | | iffalse 3881 |
. . . . . . . 8
        |
327 | 325, 326 | oveq12d 6326 |
. . . . . . 7
      
           |
328 | | 00id 9826 |
. . . . . . 7
   |
329 | 327, 328 | syl6eq 2521 |
. . . . . 6
      
         |
330 | 324, 329 | pm2.61i 169 |
. . . . 5
              |
331 | 330 | oveq1i 6318 |
. . . 4
              
   |
332 | 5, 8 | gtneii 9764 |
. . . . 5
 |
333 | 43, 332 | div0i 10363 |
. . . 4
   |
334 | 331, 333 | eqtri 2493 |
. . 3
              
 |
335 | 334 | a1i 11 |
. 2
                  |
336 | 188, 322,
335 | 3eqtrd 2509 |
1
                         |