Proof of Theorem fourierdlem30
Step | Hyp | Ref
| Expression |
1 | | fourierdlem30.b |
. . . . . . . . . . 11
   |
2 | | fourierdlem30.r |
. . . . . . . . . . . 12
   |
3 | 2 | recnd 9669 |
. . . . . . . . . . 11
   |
4 | | 0red 9644 |
. . . . . . . . . . . . 13
   |
5 | | 1red 9658 |
. . . . . . . . . . . . 13
   |
6 | | 0lt1 10136 |
. . . . . . . . . . . . . 14
 |
7 | 6 | a1i 11 |
. . . . . . . . . . . . 13
   |
8 | | fourierdlem30.x |
. . . . . . . . . . . . . . . . . . 19
     |
9 | | fourierdlem30.a |
. . . . . . . . . . . . . . . . . . . 20
   |
10 | 9 | abscld 13498 |
. . . . . . . . . . . . . . . . . . 19
       |
11 | 8, 10 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . 18
   |
12 | | fourierdlem30.y |
. . . . . . . . . . . . . . . . . . 19
     |
13 | | fourierdlem30.c |
. . . . . . . . . . . . . . . . . . . 20
   |
14 | 13 | abscld 13498 |
. . . . . . . . . . . . . . . . . . 19
       |
15 | 12, 14 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . 18
   |
16 | 11, 15 | readdcld 9670 |
. . . . . . . . . . . . . . . . 17
     |
17 | | fourierdlem30.z |
. . . . . . . . . . . . . . . . . 18
           |
18 | | fourierlemreimleblemlte22.f |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
19 | | fourierdlem30.g |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
20 | 19 | negcld 9973 |
. . . . . . . . . . . . . . . . . . . . 21
 
    |
21 | 18, 20 | mulcld 9663 |
. . . . . . . . . . . . . . . . . . . 20
 
 
    |
22 | | fourierdlem30.ibl |
. . . . . . . . . . . . . . . . . . . 20
         |
23 | 21, 22 | itgcl 22741 |
. . . . . . . . . . . . . . . . . . 19
         |
24 | 23 | abscld 13498 |
. . . . . . . . . . . . . . . . . 18
             |
25 | 17, 24 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . 17
   |
26 | 16, 25 | readdcld 9670 |
. . . . . . . . . . . . . . . 16
       |
27 | | fourierdlem30.e |
. . . . . . . . . . . . . . . . 17
   |
28 | 27 | rpred 11341 |
. . . . . . . . . . . . . . . 16
   |
29 | 27 | rpne0d 11346 |
. . . . . . . . . . . . . . . 16
   |
30 | 26, 28, 29 | redivcld 10435 |
. . . . . . . . . . . . . . 15
         |
31 | 30, 5 | readdcld 9670 |
. . . . . . . . . . . . . 14
           |
32 | 9 | absge0d 13506 |
. . . . . . . . . . . . . . . . . . 19

      |
33 | 32, 8 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . 18

  |
34 | 13 | absge0d 13506 |
. . . . . . . . . . . . . . . . . . 19

      |
35 | 34, 12 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . 18

  |
36 | 11, 15, 33, 35 | addge0d 10189 |
. . . . . . . . . . . . . . . . 17

    |
37 | 23 | absge0d 13506 |
. . . . . . . . . . . . . . . . . 18

            |
38 | 37, 17 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . 17

  |
39 | 16, 25, 36, 38 | addge0d 10189 |
. . . . . . . . . . . . . . . 16

 
    |
40 | 26, 27, 39 | divge0d 11378 |
. . . . . . . . . . . . . . 15

        |
41 | 5, 30 | addge02d 10202 |
. . . . . . . . . . . . . . 15
       
           |
42 | 40, 41 | mpbid 214 |
. . . . . . . . . . . . . 14

          |
43 | | fourierdlem30.ler |
. . . . . . . . . . . . . 14
        
  |
44 | 5, 31, 2, 42, 43 | letrd 9792 |
. . . . . . . . . . . . 13

  |
45 | 4, 5, 2, 7, 44 | ltletrd 9795 |
. . . . . . . . . . . 12
   |
46 | 45 | gt0ne0d 10178 |
. . . . . . . . . . 11
   |
47 | 1, 3, 46 | divnegd 10396 |
. . . . . . . . . 10
         |
48 | 47 | oveq2d 6306 |
. . . . . . . . 9
             |
49 | 1 | negcld 9973 |
. . . . . . . . . 10
    |
50 | 9, 49, 3, 46 | divassd 10418 |
. . . . . . . . 9
             |
51 | 48, 50 | eqtr4d 2488 |
. . . . . . . 8
             |
52 | | fourierdlem30.d |
. . . . . . . . . . 11
   |
53 | 52, 3, 46 | divnegd 10396 |
. . . . . . . . . 10
         |
54 | 53 | oveq2d 6306 |
. . . . . . . . 9
             |
55 | 52 | negcld 9973 |
. . . . . . . . . 10
    |
56 | 13, 55, 3, 46 | divassd 10418 |
. . . . . . . . 9
             |
57 | 54, 56 | eqtr4d 2488 |
. . . . . . . 8
             |
58 | 51, 57 | oveq12d 6308 |
. . . . . . 7
       
                   |
59 | 9, 49 | mulcld 9663 |
. . . . . . . 8
      |
60 | 13, 55 | mulcld 9663 |
. . . . . . . 8
      |
61 | 59, 60, 3, 46 | divsubdird 10422 |
. . . . . . 7
      
                  |
62 | 58, 61 | eqtr4d 2488 |
. . . . . 6
       
                 |
63 | 3, 46 | reccld 10376 |
. . . . . . . 8
     |
64 | 63, 21, 22 | itgmulc2 22791 |
. . . . . . 7
                
      |
65 | 23, 3, 46 | divrec2d 10387 |
. . . . . . 7
                     |
66 | 3 | adantr 467 |
. . . . . . . . . . 11
 
   |
67 | 46 | adantr 467 |
. . . . . . . . . . 11
 
   |
68 | 19, 66, 67 | divnegd 10396 |
. . . . . . . . . 10
 
         |
69 | 68 | oveq2d 6306 |
. . . . . . . . 9
 
 
           |
70 | 18, 20, 66, 67 | divassd 10418 |
. . . . . . . . 9
 
             |
71 | 21, 66, 67 | divrec2d 10387 |
. . . . . . . . 9
 
               |
72 | 69, 70, 71 | 3eqtr2d 2491 |
. . . . . . . 8
 
 
             |
73 | 72 | itgeq2dv 22739 |
. . . . . . 7
              
      |
74 | 64, 65, 73 | 3eqtr4rd 2496 |
. . . . . 6
                   |
75 | 62, 74 | oveq12d 6308 |
. . . . 5
        
                                    |
76 | 59, 60 | subcld 9986 |
. . . . . 6
     
     |
77 | 76, 23, 3, 46 | divsubdird 10422 |
. . . . 5
                                         |
78 | 75, 77 | eqtr4d 2488 |
. . . 4
        
                                  |
79 | 78 | fveq2d 5869 |
. . 3
           
                        
              |
80 | 76, 23 | subcld 9986 |
. . . 4
      
            |
81 | 80, 3, 46 | absdivd 13517 |
. . 3
          
                                        |
82 | 4, 2, 45 | ltled 9783 |
. . . . 5

  |
83 | 2, 82 | absidd 13484 |
. . . 4
       |
84 | 83 | oveq2d 6306 |
. . 3
          
                         
              |
85 | 79, 81, 84 | 3eqtrd 2489 |
. 2
           
                        
              |
86 | 80 | abscld 13498 |
. . . 4
         
             |
87 | 86, 2, 46 | redivcld 10435 |
. . 3
          
              |
88 | 10, 14 | readdcld 9670 |
. . . . 5
             |
89 | 88, 24 | readdcld 9670 |
. . . 4
                         |
90 | 89, 2, 46 | redivcld 10435 |
. . 3
                           |
91 | 2, 45 | elrpd 11338 |
. . . 4
   |
92 | 76 | abscld 13498 |
. . . . . 6
               |
93 | 92, 24 | readdcld 9670 |
. . . . 5
                           |
94 | 76, 23 | abs2dif2d 13520 |
. . . . 5
         
          
        
                 |
95 | 59 | abscld 13498 |
. . . . . . . 8
    
     |
96 | 60 | abscld 13498 |
. . . . . . . 8
    
     |
97 | 95, 96 | readdcld 9670 |
. . . . . . 7
     
             |
98 | 59, 60 | abs2dif2d 13520 |
. . . . . . 7
            
           
      |
99 | 9, 49 | absmuld 13516 |
. . . . . . . . 9
    
                |
100 | 49 | abscld 13498 |
. . . . . . . . . . 11
        |
101 | 1 | absnegd 13511 |
. . . . . . . . . . . 12
            |
102 | | fourierdlem30.12 |
. . . . . . . . . . . 12
    
  |
103 | 101, 102 | eqbrtrd 4423 |
. . . . . . . . . . 11
     
  |
104 | 100, 5, 10, 32, 103 | lemul2ad 10547 |
. . . . . . . . . 10
                    |
105 | 10 | recnd 9669 |
. . . . . . . . . . 11
       |
106 | 105 | mulid1d 9660 |
. . . . . . . . . 10
             |
107 | 104, 106 | breqtrd 4427 |
. . . . . . . . 9
                  |
108 | 99, 107 | eqbrtrd 4423 |
. . . . . . . 8
    
  
      |
109 | 13, 55 | absmuld 13516 |
. . . . . . . . 9
    
                |
110 | 55 | abscld 13498 |
. . . . . . . . . . 11
        |
111 | 52 | absnegd 13511 |
. . . . . . . . . . . 12
            |
112 | | fourierdlem30.14 |
. . . . . . . . . . . 12
    
  |
113 | 111, 112 | eqbrtrd 4423 |
. . . . . . . . . . 11
     
  |
114 | 110, 5, 14, 34, 113 | lemul2ad 10547 |
. . . . . . . . . 10
                    |
115 | 14 | recnd 9669 |
. . . . . . . . . . 11
       |
116 | 115 | mulid1d 9660 |
. . . . . . . . . 10
             |
117 | 114, 116 | breqtrd 4427 |
. . . . . . . . 9
                  |
118 | 109, 117 | eqbrtrd 4423 |
. . . . . . . 8
    
  
      |
119 | 95, 96, 10, 14, 108, 118 | le2addd 10232 |
. . . . . . 7
     
                       |
120 | 92, 97, 88, 98, 119 | letrd 9792 |
. . . . . 6
            
            |
121 | 92, 88, 24, 120 | leadd1dd 10227 |
. . . . 5
                                                 |
122 | 86, 93, 89, 94, 121 | letrd 9792 |
. . . 4
         
          
                        |
123 | 86, 89, 91, 122 | lediv1dd 11396 |
. . 3
          
                                      |
124 | 30 | ltp1d 10537 |
. . . . . . 7
      
          |
125 | 4, 30, 31, 40, 124 | lelttrd 9793 |
. . . . . 6
           |
126 | 125 | gt0ne0d 10178 |
. . . . 5
           |
127 | 89, 31, 126 | redivcld 10435 |
. . . 4
                                   |
128 | 30, 40 | ge0p1rpd 11368 |
. . . . 5
           |
129 | 8 | eqcomi 2460 |
. . . . . . . 8
     |
130 | 12 | eqcomi 2460 |
. . . . . . . 8
     |
131 | 129, 130 | oveq12i 6302 |
. . . . . . 7
             |
132 | 17 | eqcomi 2460 |
. . . . . . 7
           |
133 | 131, 132 | oveq12i 6302 |
. . . . . 6
                           |
134 | 39, 133 | syl6breqr 4443 |
. . . . 5

                        |
135 | 128, 91, 89, 134, 43 | lediv2ad 11363 |
. . . 4
                                                           |
136 | 133 | oveq1i 6300 |
. . . . 5
                                               |
137 | | oveq1 6297 |
. . . . . . . . 9
                               |
138 | 137 | adantl 468 |
. . . . . . . 8
 
 
  
                          |
139 | 30 | recnd 9669 |
. . . . . . . . . . 11
         |
140 | 5 | recnd 9669 |
. . . . . . . . . . 11
   |
141 | 139, 140 | addcld 9662 |
. . . . . . . . . 10
           |
142 | 141 | adantr 467 |
. . . . . . . . 9
 
 
  
          |
143 | | oveq1 6297 |
. . . . . . . . . . . . . 14
               |
144 | 143 | adantl 468 |
. . . . . . . . . . . . 13
 
 
  
          |
145 | 27 | rpcnd 11343 |
. . . . . . . . . . . . . . 15
   |
146 | 145 | adantr 467 |
. . . . . . . . . . . . . 14
 
 
  
  |
147 | 29 | adantr 467 |
. . . . . . . . . . . . . 14
 
 
  
  |
148 | 146, 147 | div0d 10382 |
. . . . . . . . . . . . 13
 
 
  
    |
149 | 144, 148 | eqtrd 2485 |
. . . . . . . . . . . 12
 
 
  
        |
150 | 149 | oveq1d 6305 |
. . . . . . . . . . 11
 
 
  
            |
151 | | 0p1e1 10721 |
. . . . . . . . . . 11
   |
152 | 150, 151 | syl6eq 2501 |
. . . . . . . . . 10
 
 
  
          |
153 | | ax-1ne0 9608 |
. . . . . . . . . . 11
 |
154 | 153 | a1i 11 |
. . . . . . . . . 10
 
 
  
  |
155 | 152, 154 | eqnetrd 2691 |
. . . . . . . . 9
 
 
  
          |
156 | 142, 155 | div0d 10382 |
. . . . . . . 8
 
 
  
            |
157 | 138, 156 | eqtrd 2485 |
. . . . . . 7
 
 
  
                |
158 | 27 | rpgt0d 11344 |
. . . . . . . 8
   |
159 | 158 | adantr 467 |
. . . . . . 7
 
 
  
  |
160 | 157, 159 | eqbrtrd 4423 |
. . . . . 6
 
 
  
                |
161 | 26 | adantr 467 |
. . . . . . 7
 
           |
162 | 27 | adantr 467 |
. . . . . . 7
 
    
  |
163 | 39 | adantr 467 |
. . . . . . . . . . 11
 
    
 
    |
164 | | neqne 37374 |
. . . . . . . . . . . 12
           |
165 | 164 | adantl 468 |
. . . . . . . . . . 11
 
           |
166 | 161, 163,
165 | ne0gt0d 9772 |
. . . . . . . . . 10
 
    
 
    |
167 | 161, 166 | elrpd 11338 |
. . . . . . . . 9
 
           |
168 | 167, 162 | rpdivcld 11358 |
. . . . . . . 8
 
             |
169 | | 1rp 11306 |
. . . . . . . . 9
 |
170 | 169 | a1i 11 |
. . . . . . . 8
 
       |
171 | 168, 170 | rpaddcld 11356 |
. . . . . . 7
 
               |
172 | 124 | adantr 467 |
. . . . . . 7
 
          
          |
173 | 161, 162,
171, 172 | ltdiv23d 11403 |
. . . . . 6
 
                     |
174 | 160, 173 | pm2.61dan 800 |
. . . . 5
                 |
175 | 136, 174 | syl5eqbr 4436 |
. . . 4
                                   |
176 | 90, 127, 28, 135, 175 | lelttrd 9793 |
. . 3
                           |
177 | 87, 90, 28, 123, 176 | lelttrd 9793 |
. 2
          
              |
178 | 85, 177 | eqbrtrd 4423 |
1
           
                 |