Proof of Theorem itgsinexplem1
Step | Hyp | Ref
| Expression |
1 | | 0m0e0 10719 |
. . . . 5
   |
2 | 1 | oveq1i 6300 |
. . . 4
                                                                       |
3 | | 0re 9643 |
. . . . . 6
 |
4 | 3 | a1i 11 |
. . . . 5
   |
5 | | pire 23413 |
. . . . . 6
 |
6 | 5 | a1i 11 |
. . . . 5
   |
7 | | pipos 23415 |
. . . . . . 7
 |
8 | 3, 5, 7 | ltleii 9757 |
. . . . . 6
 |
9 | 8 | a1i 11 |
. . . . 5

  |
10 | 3, 5 | pm3.2i 457 |
. . . . . . . . . . . . 13
   |
11 | | iccssre 11716 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)    |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . 12
  ![[,] [,]](_icc.gif)   |
13 | | ax-resscn 9596 |
. . . . . . . . . . . 12
 |
14 | 12, 13 | sstri 3441 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)   |
15 | 14 | sseli 3428 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
16 | 15 | adantl 468 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)     |
17 | 15 | sincld 14184 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)        |
18 | 17 | adantl 468 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)         |
19 | | itgsinexplem1.7 |
. . . . . . . . . . . 12
   |
20 | 19 | nnnn0d 10925 |
. . . . . . . . . . 11
   |
21 | 20 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)     |
22 | 18, 21 | expcld 12416 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)             |
23 | | itgsinexplem1.1 |
. . . . . . . . . 10
           |
24 | 23 | fvmpt2 5957 |
. . . . . . . . 9
                         |
25 | 16, 22, 24 | syl2anc 667 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)                 |
26 | 25 | eqcomd 2457 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)                 |
27 | 26 | mpteq2dva 4489 |
. . . . . 6
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)         |
28 | | nfmpt1 4492 |
. . . . . . . 8
             |
29 | 23, 28 | nfcxfr 2590 |
. . . . . . 7
   |
30 | | nfcv 2592 |
. . . . . . . . 9
   |
31 | | sincn 23399 |
. . . . . . . . . 10
     |
32 | 31 | a1i 11 |
. . . . . . . . 9
       |
33 | 30, 32, 20 | expcnfg 37671 |
. . . . . . . 8
                 |
34 | 23, 33 | syl5eqel 2533 |
. . . . . . 7
       |
35 | 14 | a1i 11 |
. . . . . . 7
   ![[,] [,]](_icc.gif)    |
36 | 29, 34, 35 | cncfmptss 37665 |
. . . . . 6
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
37 | 27, 36 | eqeltrd 2529 |
. . . . 5
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
38 | 15 | coscld 14185 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)        |
39 | 38 | negcld 9973 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)         |
40 | | itgsinexplem1.2 |
. . . . . . . . . . 11
        |
41 | 40 | fvmpt2 5957 |
. . . . . . . . . 10
                   |
42 | 15, 39, 41 | syl2anc 667 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)             |
43 | 42 | eqcomd 2457 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)             |
44 | 43 | adantl 468 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)              |
45 | 44 | mpteq2dva 4489 |
. . . . . 6
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)         |
46 | | nfmpt1 4492 |
. . . . . . . 8
          |
47 | 40, 46 | nfcxfr 2590 |
. . . . . . 7
   |
48 | | coscn 23400 |
. . . . . . . . 9
     |
49 | 48 | a1i 11 |
. . . . . . . 8
       |
50 | 40 | negfcncf 21951 |
. . . . . . . 8
    
      |
51 | 49, 50 | syl 17 |
. . . . . . 7
       |
52 | 47, 51, 35 | cncfmptss 37665 |
. . . . . 6
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
53 | 45, 52 | eqeltrd 2529 |
. . . . 5
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)       |
54 | | itgsinexplem1.3 |
. . . . . 6
                     |
55 | | ssid 3451 |
. . . . . . . . . . 11
 |
56 | 55 | a1i 11 |
. . . . . . . . . 10

  |
57 | 19 | nncnd 10625 |
. . . . . . . . . 10
   |
58 | 56, 57, 56 | constcncfg 37748 |
. . . . . . . . 9
         |
59 | | nnm1nn0 10911 |
. . . . . . . . . . 11
 
   |
60 | 19, 59 | syl 17 |
. . . . . . . . . 10
     |
61 | 30, 32, 60 | expcnfg 37671 |
. . . . . . . . 9
                   |
62 | 58, 61 | mulcncf 22398 |
. . . . . . . 8
  
                  |
63 | | cosf 14179 |
. . . . . . . . . . 11
     |
64 | 63 | a1i 11 |
. . . . . . . . . 10
       |
65 | 64 | feqmptd 5918 |
. . . . . . . . 9
         |
66 | 65, 48 | syl6eqelr 2538 |
. . . . . . . 8
             |
67 | 62, 66 | mulcncf 22398 |
. . . . . . 7
                           |
68 | 54, 67 | syl5eqel 2533 |
. . . . . 6
       |
69 | | ioosscn 37591 |
. . . . . . 7
     |
70 | 69 | a1i 11 |
. . . . . 6
       |
71 | 57 | adantr 467 |
. . . . . . . 8
 
       |
72 | 69 | sseli 3428 |
. . . . . . . . . . 11
       |
73 | 72 | sincld 14184 |
. . . . . . . . . 10
           |
74 | 73 | adantl 468 |
. . . . . . . . 9
 
           |
75 | 60 | adantr 467 |
. . . . . . . . 9
 
     
   |
76 | 74, 75 | expcld 12416 |
. . . . . . . 8
 
                 |
77 | 71, 76 | mulcld 9663 |
. . . . . . 7
 
     
             |
78 | 72 | coscld 14185 |
. . . . . . . 8
           |
79 | 78 | adantl 468 |
. . . . . . 7
 
           |
80 | 77, 79 | mulcld 9663 |
. . . . . 6
 
                         |
81 | 54, 68, 70, 56, 80 | cncfmptssg 37747 |
. . . . 5
                                   |
82 | 30, 32, 70 | cncfmptss 37665 |
. . . . 5
                     |
83 | | ioossicc 11720 |
. . . . . . 7
      ![[,] [,]](_icc.gif)   |
84 | 83 | a1i 11 |
. . . . . 6
       ![[,] [,]](_icc.gif)    |
85 | | ioombl 22518 |
. . . . . . 7
     |
86 | 85 | a1i 11 |
. . . . . 6
    
  |
87 | 22, 18 | mulcld 9663 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)                   |
88 | | itgsinexplem1.4 |
. . . . . . . . . . . 12
                 |
89 | 88 | fvmpt2 5957 |
. . . . . . . . . . 11
                                     |
90 | 16, 87, 89 | syl2anc 667 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)                       |
91 | 90 | eqcomd 2457 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)                       |
92 | 91 | mpteq2dva 4489 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)         |
93 | | nfmpt1 4492 |
. . . . . . . . . 10
                   |
94 | 88, 93 | nfcxfr 2590 |
. . . . . . . . 9
   |
95 | | sinf 14178 |
. . . . . . . . . . . . . 14
     |
96 | 95 | a1i 11 |
. . . . . . . . . . . . 13
       |
97 | 96 | feqmptd 5918 |
. . . . . . . . . . . 12
         |
98 | 97, 31 | syl6eqelr 2538 |
. . . . . . . . . . 11
             |
99 | 33, 98 | mulcncf 22398 |
. . . . . . . . . 10
                       |
100 | 88, 99 | syl5eqel 2533 |
. . . . . . . . 9
       |
101 | 94, 100, 35 | cncfmptss 37665 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
102 | 92, 101 | eqeltrd 2529 |
. . . . . . 7
    ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)       |
103 | | cniccibl 22798 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)                    |
104 | 4, 6, 102, 103 | syl3anc 1268 |
. . . . . 6
    ![[,] [,]](_icc.gif)                    |
105 | 84, 86, 87, 104 | iblss 22762 |
. . . . 5
                        |
106 | 57 | adantr 467 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)     |
107 | 60 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)   
   |
108 | 18, 107 | expcld 12416 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)               |
109 | 106, 108 | mulcld 9663 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)   
             |
110 | 38 | adantl 468 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)         |
111 | 109, 110 | mulcld 9663 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)                       |
112 | 39 | adantl 468 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)          |
113 | 111, 112 | mulcld 9663 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)                              |
114 | | itgsinexplem1.5 |
. . . . . . . 8
           
                |
115 | | eqid 2451 |
. . . . . . . . . . . 12
               |
116 | 115 | negfcncf 21951 |
. . . . . . . . . . 11
    
             |
117 | 49, 116 | syl 17 |
. . . . . . . . . 10
              |
118 | 67, 117 | mulcncf 22398 |
. . . . . . . . 9
            
                     |
119 | 114, 118 | syl5eqel 2533 |
. . . . . . . 8
       |
120 | 114, 119,
35, 56, 113 | cncfmptssg 37747 |
. . . . . . 7
    ![[,] [,]](_icc.gif)            
                  ![[,] [,]](_icc.gif)       |
121 | | cniccibl 22798 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)                               |
122 | 4, 6, 120, 121 | syl3anc 1268 |
. . . . . 6
    ![[,] [,]](_icc.gif)            
                  |
123 | 84, 86, 113, 122 | iblss 22762 |
. . . . 5
                
                  |
124 | | reelprrecn 9631 |
. . . . . . 7
    |
125 | 124 | a1i 11 |
. . . . . 6
      |
126 | | recn 9629 |
. . . . . . . . 9
   |
127 | 126 | sincld 14184 |
. . . . . . . 8
       |
128 | 127 | adantl 468 |
. . . . . . 7
 

      |
129 | 20 | adantr 467 |
. . . . . . 7
 

  |
130 | 128, 129 | expcld 12416 |
. . . . . 6
 

          |
131 | 57 | adantr 467 |
. . . . . . . 8
 

  |
132 | 60 | adantr 467 |
. . . . . . . . 9
 

    |
133 | 128, 132 | expcld 12416 |
. . . . . . . 8
 

            |
134 | 131, 133 | mulcld 9663 |
. . . . . . 7
 

        
     |
135 | 126 | coscld 14185 |
. . . . . . . 8
       |
136 | 135 | adantl 468 |
. . . . . . 7
 

      |
137 | 134, 136 | mulcld 9663 |
. . . . . 6
 

                    |
138 | | sincl 14180 |
. . . . . . . . . . 11
       |
139 | 138 | adantl 468 |
. . . . . . . . . 10
 

      |
140 | 20 | adantr 467 |
. . . . . . . . . 10
 

  |
141 | 139, 140 | expcld 12416 |
. . . . . . . . 9
 

          |
142 | 141, 23 | fmptd 6046 |
. . . . . . . 8
       |
143 | 126 | adantl 468 |
. . . . . . . . . . . . . 14
 

  |
144 | | elex 3054 |
. . . . . . . . . . . . . . 15
                  
 
                  |
145 | 137, 144 | syl 17 |
. . . . . . . . . . . . . 14
 

                    |
146 | | rabid 2967 |
. . . . . . . . . . . . . 14
                                           |
147 | 143, 145,
146 | sylanbrc 670 |
. . . . . . . . . . . . 13
 

          
           |
148 | 54 | dmmpt 5330 |
. . . . . . . . . . . . 13
          
          |
149 | 147, 148 | syl6eleqr 2540 |
. . . . . . . . . . . 12
 

  |
150 | 149 | ex 436 |
. . . . . . . . . . 11
     |
151 | 150 | alrimiv 1773 |
. . . . . . . . . 10
       |
152 | | nfcv 2592 |
. . . . . . . . . . 11
   |
153 | | nfmpt1 4492 |
. . . . . . . . . . . . 13
                       |
154 | 54, 153 | nfcxfr 2590 |
. . . . . . . . . . . 12
   |
155 | 154 | nfdm 5076 |
. . . . . . . . . . 11
   |
156 | 152, 155 | dfss2f 3423 |
. . . . . . . . . 10

      |
157 | 151, 156 | sylibr 216 |
. . . . . . . . 9

  |
158 | 19 | dvsinexp 37780 |
. . . . . . . . . . 11
                                   |
159 | 23 | oveq2i 6301 |
. . . . . . . . . . 11
               |
160 | 158, 159,
54 | 3eqtr4g 2510 |
. . . . . . . . . 10
     |
161 | 160 | dmeqd 5037 |
. . . . . . . . 9
     |
162 | 157, 161 | sseqtr4d 3469 |
. . . . . . . 8

    |
163 | | dvres3 22868 |
. . . . . . . 8
    
       
             |
164 | 125, 142,
56, 162, 163 | syl22anc 1269 |
. . . . . . 7
           |
165 | 23 | reseq1i 5101 |
. . . . . . . . . 10
            
  |
166 | | resmpt 5154 |
. . . . . . . . . . 11

          
             |
167 | 13, 166 | ax-mp 5 |
. . . . . . . . . 10
          
            |
168 | 165, 167 | eqtri 2473 |
. . . . . . . . 9
             |
169 | 168 | oveq2i 6301 |
. . . . . . . 8
                 |
170 | 169 | a1i 11 |
. . . . . . 7
      
            |
171 | 160 | reseq1d 5104 |
. . . . . . . 8
         |
172 | 54 | reseq1i 5101 |
. . . . . . . . 9
                         |
173 | | resmpt 5154 |
. . . . . . . . . 10

                                            |
174 | 13, 173 | ax-mp 5 |
. . . . . . . . 9
                                           |
175 | 172, 174 | eqtri 2473 |
. . . . . . . 8
                       |
176 | 171, 175 | syl6eq 2501 |
. . . . . . 7
               
           |
177 | 164, 170,
176 | 3eqtr3d 2493 |
. . . . . 6
                                   |
178 | 12 | a1i 11 |
. . . . . 6
   ![[,] [,]](_icc.gif)    |
179 | | eqid 2451 |
. . . . . . 7
  ℂfld   ℂfld |
180 | 179 | tgioo2 21821 |
. . . . . 6
       ℂfld
↾t   |
181 | 10 | a1i 11 |
. . . . . . 7
     |
182 | | iccntr 21839 |
. . . . . . 7
         
      ![[,] [,]](_icc.gif)         |
183 | 181, 182 | syl 17 |
. . . . . 6
       
      ![[,] [,]](_icc.gif)         |
184 | 125, 130,
137, 177, 178, 180, 179, 183 | dvmptres2 22916 |
. . . . 5
     ![[,] [,]](_icc.gif)                                      |
185 | 135 | negcld 9973 |
. . . . . . 7
        |
186 | 185 | adantl 468 |
. . . . . 6
 

       |
187 | 127 | negcld 9973 |
. . . . . . . . 9
        |
188 | 187 | adantl 468 |
. . . . . . . 8
 

       |
189 | | dvcosre 37781 |
. . . . . . . . 9
                |
190 | 189 | a1i 11 |
. . . . . . . 8
                  |
191 | 125, 136,
188, 190 | dvmptneg 22920 |
. . . . . . 7
                    |
192 | 127 | negnegd 9977 |
. . . . . . . . 9
             |
193 | 192 | adantl 468 |
. . . . . . . 8
 

            |
194 | 193 | mpteq2dva 4489 |
. . . . . . 7
                 |
195 | 191, 194 | eqtrd 2485 |
. . . . . 6
                  |
196 | 125, 186,
128, 195, 178, 180, 179, 183 | dvmptres2 22916 |
. . . . 5
     ![[,] [,]](_icc.gif)                     |
197 | | fveq2 5865 |
. . . . . . . . . . 11
           |
198 | | sin0 14203 |
. . . . . . . . . . 11
     |
199 | 197, 198 | syl6eq 2501 |
. . . . . . . . . 10
       |
200 | 199 | oveq1d 6305 |
. . . . . . . . 9
               |
201 | 200 | adantl 468 |
. . . . . . . 8
 
               |
202 | 19 | adantr 467 |
. . . . . . . . 9
 
   |
203 | 202 | 0expd 12432 |
. . . . . . . 8
 
       |
204 | 201, 203 | eqtrd 2485 |
. . . . . . 7
 
           |
205 | 204 | oveq1d 6305 |
. . . . . 6
 
                         |
206 | | id 22 |
. . . . . . . . . 10
   |
207 | | 0cn 9635 |
. . . . . . . . . 10
 |
208 | 206, 207 | syl6eqel 2537 |
. . . . . . . . 9
   |
209 | | coscl 14181 |
. . . . . . . . . 10
       |
210 | 209 | negcld 9973 |
. . . . . . . . 9
        |
211 | 208, 210 | syl 17 |
. . . . . . . 8
        |
212 | 211 | adantl 468 |
. . . . . . 7
 
        |
213 | 212 | mul02d 9831 |
. . . . . 6
 
          |
214 | 205, 213 | eqtrd 2485 |
. . . . 5
 
                  |
215 | | fveq2 5865 |
. . . . . . . . . . 11
           |
216 | | sinpi 23412 |
. . . . . . . . . . 11
     |
217 | 215, 216 | syl6eq 2501 |
. . . . . . . . . 10
       |
218 | 217 | oveq1d 6305 |
. . . . . . . . 9
               |
219 | 218 | adantl 468 |
. . . . . . . 8
 

              |
220 | 19 | adantr 467 |
. . . . . . . . 9
 

  |
221 | 220 | 0expd 12432 |
. . . . . . . 8
 

      |
222 | 219, 221 | eqtrd 2485 |
. . . . . . 7
 

          |
223 | 222 | oveq1d 6305 |
. . . . . 6
 

                        |
224 | | id 22 |
. . . . . . . . . . 11
   |
225 | | picn 23414 |
. . . . . . . . . . 11
 |
226 | 224, 225 | syl6eqel 2537 |
. . . . . . . . . 10
   |
227 | 226 | coscld 14185 |
. . . . . . . . 9
       |
228 | 227 | negcld 9973 |
. . . . . . . 8
        |
229 | 228 | adantl 468 |
. . . . . . 7
 

       |
230 | 229 | mul02d 9831 |
. . . . . 6
 

         |
231 | 223, 230 | eqtrd 2485 |
. . . . 5
 

                 |
232 | 4, 6, 9, 37, 53, 81, 82, 105, 123, 184, 196, 214, 231 | itgparts 22999 |
. . . 4
                                                            |
233 | | df-neg 9863 |
. . . . 5
                                                  
                 |
234 | 233 | a1i 11 |
. . . 4
                                                                      |
235 | 2, 232, 234 | 3eqtr4a 2511 |
. . 3
                                                         |
236 | 77, 79, 79 | mulassd 9666 |
. . . . . . . . 9
 
                                                       |
237 | | sqval 12334 |
. . . . . . . . . . . . . 14
                         |
238 | 237 | eqcomd 2457 |
. . . . . . . . . . . . 13
                         |
239 | 78, 238 | syl 17 |
. . . . . . . . . . . 12
                         |
240 | 239 | adantl 468 |
. . . . . . . . . . 11
 
                         |
241 | 240 | oveq2d 6306 |
. . . . . . . . . 10
 
                                                     |
242 | 78 | sqcld 12414 |
. . . . . . . . . . . 12
               |
243 | 242 | adantl 468 |
. . . . . . . . . . 11
 
               |
244 | 71, 76, 243 | mulassd 9666 |
. . . . . . . . . 10
 
                                    
              |
245 | 241, 244 | eqtrd 2485 |
. . . . . . . . 9
 
                                                     |
246 | 76, 243 | mulcomd 9664 |
. . . . . . . . . 10
 
                                         
     |
247 | 246 | oveq2d 6306 |
. . . . . . . . 9
 
     
                                      
      |
248 | 236, 245,
247 | 3eqtrd 2489 |
. . . . . . . 8
 
                                              
      |
249 | 248 | negeqd 9869 |
. . . . . . 7
 
                               
                
      |
250 | 80, 79 | mulneg2d 10072 |
. . . . . . 7
 
                                         
               |
251 | 243, 76 | mulcld 9663 |
. . . . . . . 8
 
                     
     |
252 | 71, 251 | mulneg1d 10071 |
. . . . . . 7
 
                       
                             |
253 | 249, 250,
252 | 3eqtr4d 2495 |
. . . . . 6
 
                                                
      |
254 | 253 | itgeq2dv 22739 |
. . . . 5
                                                         
       |
255 | 57 | negcld 9973 |
. . . . . 6
    |
256 | 38 | sqcld 12414 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)            |
257 | 256 | adantl 468 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)             |
258 | 257, 108 | mulcld 9663 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)                   
     |
259 | | itgsinexplem1.6 |
. . . . . . . . . . . . 13
                       |
260 | 259 | fvmpt2 5957 |
. . . . . . . . . . . 12
                                           
     |
261 | 16, 258, 260 | syl2anc 667 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                             |
262 | 261 | eqcomd 2457 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)                   
         |
263 | 262 | mpteq2dva 4489 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)         |
264 | | nfmpt1 4492 |
. . . . . . . . . . 11
                         |
265 | 259, 264 | nfcxfr 2590 |
. . . . . . . . . 10
   |
266 | | nfcv 2592 |
. . . . . . . . . . . . 13
   |
267 | | 2nn0 10886 |
. . . . . . . . . . . . . 14
 |
268 | 267 | a1i 11 |
. . . . . . . . . . . . 13
   |
269 | 266, 49, 268 | expcnfg 37671 |
. . . . . . . . . . . 12
                 |
270 | 269, 61 | mulcncf 22398 |
. . . . . . . . . . 11
                             |
271 | 259, 270 | syl5eqel 2533 |
. . . . . . . . . 10
       |
272 | 265, 271,
35 | cncfmptss 37665 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
273 | 263, 272 | eqeltrd 2529 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)       |
274 | | cniccibl 22798 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)                  
       ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)                          |
275 | 4, 6, 273, 274 | syl3anc 1268 |
. . . . . . 7
    ![[,] [,]](_icc.gif)                          |
276 | 84, 86, 258, 275 | iblss 22762 |
. . . . . 6
                              |
277 | 255, 251,
276 | itgmulc2 22791 |
. . . . 5
                                                       
       |
278 | 254, 277 | eqtr4d 2488 |
. . . 4
                                                         
       |
279 | 278 | negeqd 9869 |
. . 3
                                                           
       |
280 | 235, 279 | eqtrd 2485 |
. 2
                                               
       |
281 | 251, 276 | itgcl 22741 |
. . . 4
                       
      |
282 | 57, 281 | mulneg1d 10071 |
. . 3
                                                               |
283 | 282 | negeqd 9869 |
. 2
                          
       
                              |
284 | 57, 281 | mulcld 9663 |
. . 3
                                |
285 | 284 | negnegd 9977 |
. 2
                                                               |
286 | 280, 283,
285 | 3eqtrd 2489 |
1
                                                     |