Step | Hyp | Ref
| Expression |
1 | | fourierdlem49.a |
. . . . . 6
   |
2 | | fourierdlem49.b |
. . . . . 6
   |
3 | | fourierdlem49.altb |
. . . . . 6
   |
4 | | fourierdlem49.t |
. . . . . 6
   |
5 | | fourierdlem49.e |
. . . . . . 7
 
       |
6 | | ovex 6318 |
. . . . . . . . . 10
           |
7 | | fourierdlem49.z |
. . . . . . . . . . 11
             |
8 | 7 | fvmpt2 5957 |
. . . . . . . . . 10
                             |
9 | 6, 8 | mpan2 677 |
. . . . . . . . 9
                 |
10 | 9 | oveq2d 6306 |
. . . . . . . 8
                     |
11 | 10 | mpteq2ia 4485 |
. . . . . . 7
                       |
12 | 5, 11 | eqtri 2473 |
. . . . . 6
 
             |
13 | 1, 2, 3, 4, 12 | fourierdlem4 37973 |
. . . . 5
       ![(,] (,]](_ioc.gif)    |
14 | | fourierdlem49.x |
. . . . 5
   |
15 | 13, 14 | ffvelrnd 6023 |
. . . 4
       ![(,] (,]](_ioc.gif)    |
16 | | simpr 463 |
. . . . . . 7
         ![(,] (,]](_ioc.gif)              |
17 | | fourierdlem49.q |
. . . . . . . . . . . . 13
       |
18 | | fourierdlem49.m |
. . . . . . . . . . . . . 14
   |
19 | | fourierdlem49.p |
. . . . . . . . . . . . . . 15
 
                 
 ..^                |
20 | 19 | fourierdlem2 37971 |
. . . . . . . . . . . . . 14
 
   
                  
 ..^                 |
21 | 18, 20 | syl 17 |
. . . . . . . . . . . . 13
                        
 ..^                 |
22 | 17, 21 | mpbid 214 |
. . . . . . . . . . . 12
                   
 ..^                |
23 | 22 | simpld 461 |
. . . . . . . . . . 11
         |
24 | | elmapi 7493 |
. . . . . . . . . . 11
                 |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
           |
26 | | ffn 5728 |
. . . . . . . . . 10
               |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
       |
28 | 27 | ad2antrr 732 |
. . . . . . . 8
         ![(,] (,]](_ioc.gif)       
      |
29 | | fvelrnb 5912 |
. . . . . . . 8
                           |
30 | 28, 29 | syl 17 |
. . . . . . 7
         ![(,] (,]](_ioc.gif)             
                |
31 | 16, 30 | mpbid 214 |
. . . . . 6
         ![(,] (,]](_ioc.gif)        
               |
32 | | 1zzd 10968 |
. . . . . . . . . . . . . . 15
          ![(,] (,]](_ioc.gif)  
             
  |
33 | | elfzelz 11800 |
. . . . . . . . . . . . . . . 16
       |
34 | 33 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
          ![(,] (,]](_ioc.gif)  
             
  |
35 | | 1e0p1 11079 |
. . . . . . . . . . . . . . . . 17
   |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
          ![(,] (,]](_ioc.gif)  
             
    |
37 | 34 | zred 11040 |
. . . . . . . . . . . . . . . . . 18
          ![(,] (,]](_ioc.gif)  
             
  |
38 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . 19
       |
39 | 38 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
          ![(,] (,]](_ioc.gif)  
             
  |
40 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
41 | 40 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
42 | 41 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
           |
43 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
44 | 43 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
           |
45 | 22 | simprld 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
46 | 45 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
47 | 46 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
       |
48 | 42, 44, 47 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . . . . 22
           
       |
49 | 48 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . . 21
          ![(,] (,]](_ioc.gif)           
       |
50 | 49 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . 20
           ![(,] (,]](_ioc.gif)                        |
51 | 1 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
      ![(,] (,]](_ioc.gif)  
  |
52 | 1 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
53 | 52 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
      ![(,] (,]](_ioc.gif)  
  |
54 | 2 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
55 | 54 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
      ![(,] (,]](_ioc.gif)  
  |
56 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
      ![(,] (,]](_ioc.gif)  
      ![(,] (,]](_ioc.gif)    |
57 | | iocgtlb 37599 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        ![(,] (,]](_ioc.gif)         |
58 | 53, 55, 56, 57 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
      ![(,] (,]](_ioc.gif)  
      |
59 | 51, 58 | gtned 9770 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      ![(,] (,]](_ioc.gif)  
      |
60 | 59 | neneqd 2629 |
. . . . . . . . . . . . . . . . . . . . 21
 
      ![(,] (,]](_ioc.gif)  
      |
61 | 60 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . 20
           ![(,] (,]](_ioc.gif)                        |
62 | 50, 61 | pm2.65da 580 |
. . . . . . . . . . . . . . . . . . 19
          ![(,] (,]](_ioc.gif)  
             
  |
63 | 62 | neqned 2631 |
. . . . . . . . . . . . . . . . . 18
          ![(,] (,]](_ioc.gif)  
             
  |
64 | 37, 39, 63 | ne0gt0d 9772 |
. . . . . . . . . . . . . . . . 17
          ![(,] (,]](_ioc.gif)  
             
  |
65 | | 0zd 10949 |
. . . . . . . . . . . . . . . . . 18
          ![(,] (,]](_ioc.gif)  
             
  |
66 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . 18
 
       |
67 | 65, 34, 66 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
          ![(,] (,]](_ioc.gif)  
             

     |
68 | 64, 67 | mpbid 214 |
. . . . . . . . . . . . . . . 16
          ![(,] (,]](_ioc.gif)  
             
    |
69 | 36, 68 | eqbrtrd 4423 |
. . . . . . . . . . . . . . 15
          ![(,] (,]](_ioc.gif)  
             
  |
70 | | eluz2 11165 |
. . . . . . . . . . . . . . 15
         |
71 | 32, 34, 69, 70 | syl3anbrc 1192 |
. . . . . . . . . . . . . 14
          ![(,] (,]](_ioc.gif)  
             
      |
72 | | nnuz 11194 |
. . . . . . . . . . . . . 14
     |
73 | 71, 72 | syl6eleqr 2540 |
. . . . . . . . . . . . 13
          ![(,] (,]](_ioc.gif)  
             
  |
74 | | nnm1nn0 10911 |
. . . . . . . . . . . . 13
     |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
    |
76 | | nn0uz 11193 |
. . . . . . . . . . . . 13
     |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
      |
78 | 75, 77 | eleqtrd 2531 |
. . . . . . . . . . 11
          ![(,] (,]](_ioc.gif)  
             
        |
79 | 18 | nnzd 11039 |
. . . . . . . . . . . 12
   |
80 | 79 | ad3antrrr 736 |
. . . . . . . . . . 11
          ![(,] (,]](_ioc.gif)  
             
  |
81 | | peano2zm 10980 |
. . . . . . . . . . . . . . 15
     |
82 | 33, 81 | syl 17 |
. . . . . . . . . . . . . 14
         |
83 | 82 | zred 11040 |
. . . . . . . . . . . . 13
         |
84 | 33 | zred 11040 |
. . . . . . . . . . . . 13
       |
85 | | elfzel2 11798 |
. . . . . . . . . . . . . 14
       |
86 | 85 | zred 11040 |
. . . . . . . . . . . . 13
       |
87 | 84 | ltm1d 10539 |
. . . . . . . . . . . . 13
         |
88 | | elfzle2 11803 |
. . . . . . . . . . . . 13
       |
89 | 83, 84, 86, 87, 88 | ltletrd 9795 |
. . . . . . . . . . . 12
         |
90 | 89 | ad2antlr 733 |
. . . . . . . . . . 11
          ![(,] (,]](_ioc.gif)  
             
    |
91 | | elfzo2 11923 |
. . . . . . . . . . 11
    ..^       
     |
92 | 78, 80, 90, 91 | syl3anbrc 1192 |
. . . . . . . . . 10
          ![(,] (,]](_ioc.gif)  
             
   ..^   |
93 | 25 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
          ![(,] (,]](_ioc.gif)  
             
          |
94 | 34, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
          ![(,] (,]](_ioc.gif)  
             
    |
95 | 65, 80, 94 | 3jca 1188 |
. . . . . . . . . . . . . . . 16
          ![(,] (,]](_ioc.gif)  
             
      |
96 | 75 | nn0ge0d 10928 |
. . . . . . . . . . . . . . . 16
          ![(,] (,]](_ioc.gif)  
             
    |
97 | 83, 86, 89 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
         |
98 | 97 | ad2antlr 733 |
. . . . . . . . . . . . . . . 16
          ![(,] (,]](_ioc.gif)  
             
    |
99 | 95, 96, 98 | jca32 538 |
. . . . . . . . . . . . . . 15
          ![(,] (,]](_ioc.gif)  
             
 
            |
100 | | elfz2 11791 |
. . . . . . . . . . . . . . 15
      
 
            |
101 | 99, 100 | sylibr 216 |
. . . . . . . . . . . . . 14
          ![(,] (,]](_ioc.gif)  
             
        |
102 | 93, 101 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
          ![(,] (,]](_ioc.gif)  
             
        |
103 | 102 | rexrd 9690 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
        |
104 | 25 | ffvelrnda 6022 |
. . . . . . . . . . . . . . 15
 
           |
105 | 104 | rexrd 9690 |
. . . . . . . . . . . . . 14
 
           |
106 | 105 | adantlr 721 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif)              |
107 | 106 | adantr 467 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
      |
108 | | iocssre 11714 |
. . . . . . . . . . . . . . . 16
     ![(,] (,]](_ioc.gif)    |
109 | 52, 2, 108 | syl2anc 667 |
. . . . . . . . . . . . . . 15
   ![(,] (,]](_ioc.gif) 
  |
110 | 109 | sselda 3432 |
. . . . . . . . . . . . . 14
 
      ![(,] (,]](_ioc.gif)  
      |
111 | 110 | rexrd 9690 |
. . . . . . . . . . . . 13
 
      ![(,] (,]](_ioc.gif)  
      |
112 | 111 | ad2antrr 732 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
      |
113 | | simplll 768 |
. . . . . . . . . . . . . . 15
          ![(,] (,]](_ioc.gif)  
             
  |
114 | | ovex 6318 |
. . . . . . . . . . . . . . . 16
   |
115 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . 18
     ..^
   ..^    |
116 | 115 | anbi2d 710 |
. . . . . . . . . . . . . . . . 17
    
 ..^      ..^     |
117 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
               |
118 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . 19
           |
119 | 118 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                   |
120 | 117, 119 | breq12d 4415 |
. . . . . . . . . . . . . . . . 17
       
     
                 |
121 | 116, 120 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
     
 ..^     
      
     ..^                    |
122 | 22 | simprrd 767 |
. . . . . . . . . . . . . . . . 17
   ..^              |
123 | 122 | r19.21bi 2757 |
. . . . . . . . . . . . . . . 16
 
 ..^              |
124 | 114, 121,
123 | vtocl 3100 |
. . . . . . . . . . . . . . 15
 
   ..^ 
                |
125 | 113, 92, 124 | syl2anc 667 |
. . . . . . . . . . . . . 14
          ![(,] (,]](_ioc.gif)  
             
                |
126 | 33 | zcnd 11041 |
. . . . . . . . . . . . . . . . . . 19
       |
127 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . . 19
       |
128 | 126, 127 | npcand 9990 |
. . . . . . . . . . . . . . . . . 18
           |
129 | 128 | eqcomd 2457 |
. . . . . . . . . . . . . . . . 17
           |
130 | 129 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                   |
131 | 130 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
                   |
132 | 131 | ad2antlr 733 |
. . . . . . . . . . . . . 14
          ![(,] (,]](_ioc.gif)  
             
              |
133 | 125, 132 | breqtrd 4427 |
. . . . . . . . . . . . 13
          ![(,] (,]](_ioc.gif)  
             
            |
134 | | simpr 463 |
. . . . . . . . . . . . 13
          ![(,] (,]](_ioc.gif)  
             
          |
135 | 133, 134 | breqtrd 4427 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
            |
136 | 109, 15 | sseldd 3433 |
. . . . . . . . . . . . . . . 16
       |
137 | 136 | leidd 10180 |
. . . . . . . . . . . . . . 15
    
      |
138 | 137 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                    
      |
139 | 41 | adantl 468 |
. . . . . . . . . . . . . 14
                           |
140 | 138, 139 | breqtrd 4427 |
. . . . . . . . . . . . 13
                    
      |
141 | 140 | adantllr 725 |
. . . . . . . . . . . 12
          ![(,] (,]](_ioc.gif)  
             
          |
142 | 103, 107,
112, 135, 141 | eliocd 37605 |
. . . . . . . . . . 11
          ![(,] (,]](_ioc.gif)  
             
            ![(,] (,]](_ioc.gif)        |
143 | 130 | oveq2d 6306 |
. . . . . . . . . . . 12
             ![(,] (,]](_ioc.gif)              ![(,] (,]](_ioc.gif)            |
144 | 143 | ad2antlr 733 |
. . . . . . . . . . 11
          ![(,] (,]](_ioc.gif)  
             
        ![(,] (,]](_ioc.gif)              ![(,] (,]](_ioc.gif)            |
145 | 142, 144 | eleqtrd 2531 |
. . . . . . . . . 10
          ![(,] (,]](_ioc.gif)  
             
            ![(,] (,]](_ioc.gif)            |
146 | 117, 119 | oveq12d 6308 |
. . . . . . . . . . . 12
         ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)            |
147 | 146 | eleq2d 2514 |
. . . . . . . . . . 11
              ![(,] (,]](_ioc.gif)       
            ![(,] (,]](_ioc.gif)             |
148 | 147 | rspcev 3150 |
. . . . . . . . . 10
     ..^             ![(,] (,]](_ioc.gif)             ..^            ![(,] (,]](_ioc.gif)          |
149 | 92, 145, 148 | syl2anc 667 |
. . . . . . . . 9
          ![(,] (,]](_ioc.gif)  
             
  ..^            ![(,] (,]](_ioc.gif)          |
150 | 149 | ex 436 |
. . . . . . . 8
         ![(,] (,]](_ioc.gif)                 
 ..^            ![(,] (,]](_ioc.gif)           |
151 | 150 | adantlr 721 |
. . . . . . 7
          ![(,] (,]](_ioc.gif)            
           ..^            ![(,] (,]](_ioc.gif)           |
152 | 151 | rexlimdva 2879 |
. . . . . 6
         ![(,] (,]](_ioc.gif)                         ..^            ![(,] (,]](_ioc.gif)           |
153 | 31, 152 | mpd 15 |
. . . . 5
         ![(,] (,]](_ioc.gif)        
 ..^            ![(,] (,]](_ioc.gif)          |
154 | 18 | ad2antrr 732 |
. . . . . . 7
         ![(,] (,]](_ioc.gif)          |
155 | 25 | ad2antrr 732 |
. . . . . . 7
         ![(,] (,]](_ioc.gif)                  |
156 | | iocssicc 11722 |
. . . . . . . . . 10
  ![(,] (,]](_ioc.gif)    ![[,] [,]](_icc.gif)   |
157 | 46 | eqcomd 2457 |
. . . . . . . . . . 11
       |
158 | 45 | simprd 465 |
. . . . . . . . . . . 12
       |
159 | 158 | eqcomd 2457 |
. . . . . . . . . . 11
       |
160 | 157, 159 | oveq12d 6308 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
161 | 156, 160 | syl5sseq 3480 |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif) 
      ![[,] [,]](_icc.gif)        |
162 | 161 | sselda 3432 |
. . . . . . . 8
 
      ![(,] (,]](_ioc.gif)  
          ![[,] [,]](_icc.gif)        |
163 | 162 | adantr 467 |
. . . . . . 7
         ![(,] (,]](_ioc.gif)                  ![[,] [,]](_icc.gif)        |
164 | | simpr 463 |
. . . . . . 7
         ![(,] (,]](_ioc.gif)       
      |
165 | | fveq2 5865 |
. . . . . . . . . 10
           |
166 | 165 | breq1d 4412 |
. . . . . . . . 9
     
   
           |
167 | 166 | cbvrabv 3044 |
. . . . . . . 8
  ..^            ..^           |
168 | 167 | supeq1i 7961 |
. . . . . . 7
    ..^    
      
    ..^             |
169 | 154, 155,
163, 164, 168 | fourierdlem25 37994 |
. . . . . 6
         ![(,] (,]](_ioc.gif)          ..^                      |
170 | | ioossioc 37588 |
. . . . . . . . 9
                    ![(,] (,]](_ioc.gif)         |
171 | 170 | sseli 3428 |
. . . . . . . 8
                             ![(,] (,]](_ioc.gif)          |
172 | 171 | a1i 11 |
. . . . . . 7
          ![(,] (,]](_ioc.gif)       
 ..^                    
          ![(,] (,]](_ioc.gif)           |
173 | 172 | reximdva 2862 |
. . . . . 6
         ![(,] (,]](_ioc.gif)           ..^                    
 ..^            ![(,] (,]](_ioc.gif)           |
174 | 169, 173 | mpd 15 |
. . . . 5
         ![(,] (,]](_ioc.gif)          ..^            ![(,] (,]](_ioc.gif)          |
175 | 153, 174 | pm2.61dan 800 |
. . . 4
 
      ![(,] (,]](_ioc.gif)  
  ..^            ![(,] (,]](_ioc.gif)          |
176 | 15, 175 | mpdan 674 |
. . 3
   ..^            ![(,] (,]](_ioc.gif)          |
177 | | fourierdlem49.f |
. . . . . . . . . . 11
       |
178 | | frel 5732 |
. . . . . . . . . . 11
       |
179 | 177, 178 | syl 17 |
. . . . . . . . . 10
   |
180 | | resindm 5149 |
. . . . . . . . . . 11

           
          |
181 | 180 | eqcomd 2457 |
. . . . . . . . . 10

         
            |
182 | 179, 181 | syl 17 |
. . . . . . . . 9
                       |
183 | | fdm 5733 |
. . . . . . . . . . . 12
       |
184 | 177, 183 | syl 17 |
. . . . . . . . . . 11
   |
185 | 184 | ineq2d 3634 |
. . . . . . . . . 10
                     |
186 | 185 | reseq2d 5105 |
. . . . . . . . 9
         
               |
187 | 182, 186 | eqtrd 2485 |
. . . . . . . 8
                       |
188 | 187 | 3ad2ant1 1029 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)                               |
189 | 188 | oveq1d 6305 |
. . . . . 6
 
 ..^           ![(,] (,]](_ioc.gif)                   lim                  lim        |
190 | | ax-resscn 9596 |
. . . . . . . . . . 11
 |
191 | 190 | a1i 11 |
. . . . . . . . . 10

  |
192 | 177, 191 | fssd 5738 |
. . . . . . . . 9
       |
193 | 192 | 3ad2ant1 1029 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)               |
194 | | inss2 3653 |
. . . . . . . . 9
          |
195 | 194 | a1i 11 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)                    |
196 | 193, 195 | fssresd 5750 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)                                   |
197 | | mnfxr 11414 |
. . . . . . . . . 10
 |
198 | 197 | a1i 11 |
. . . . . . . . . . 11
 
 ..^ 
  |
199 | 25 | adantr 467 |
. . . . . . . . . . . . 13
 
 ..^            |
200 | | elfzofz 11935 |
. . . . . . . . . . . . . 14
  ..^
      |
201 | 200 | adantl 468 |
. . . . . . . . . . . . 13
 
 ..^        |
202 | 199, 201 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 
 ..^        |
203 | 202 | rexrd 9690 |
. . . . . . . . . . 11
 
 ..^        |
204 | 202 | mnfltd 11426 |
. . . . . . . . . . 11
 
 ..^ 
      |
205 | 198, 203,
204 | xrltled 37484 |
. . . . . . . . . 10
 
 ..^ 
      |
206 | | iooss1 11671 |
. . . . . . . . . 10
                           |
207 | 197, 205,
206 | sylancr 669 |
. . . . . . . . 9
 
 ..^                       |
208 | 207 | 3adant3 1028 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)                    
         |
209 | | fzofzp1 12008 |
. . . . . . . . . . . . . 14
  ..^
        |
210 | 209 | adantl 468 |
. . . . . . . . . . . . 13
 
 ..^          |
211 | 199, 210 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 
 ..^          |
212 | 211 | 3adant3 1028 |
. . . . . . . . . . 11
 
 ..^           ![(,] (,]](_ioc.gif)                 |
213 | 212 | rexrd 9690 |
. . . . . . . . . 10
 
 ..^           ![(,] (,]](_ioc.gif)                 |
214 | 202 | 3adant3 1028 |
. . . . . . . . . . . 12
 
 ..^           ![(,] (,]](_ioc.gif)               |
215 | 214 | rexrd 9690 |
. . . . . . . . . . 11
 
 ..^           ![(,] (,]](_ioc.gif)               |
216 | | simp3 1010 |
. . . . . . . . . . 11
 
 ..^           ![(,] (,]](_ioc.gif)                   ![(,] (,]](_ioc.gif)          |
217 | | iocleub 37600 |
. . . . . . . . . . 11
           
          ![(,] (,]](_ioc.gif)                     |
218 | 215, 213,
216, 217 | syl3anc 1268 |
. . . . . . . . . 10
 
 ..^           ![(,] (,]](_ioc.gif)            
        |
219 | | iooss2 11672 |
. . . . . . . . . 10
                                               |
220 | 213, 218,
219 | syl2anc 667 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)                    
                |
221 | | fourierdlem49.cn |
. . . . . . . . . . . . 13
 
 ..^                                      |
222 | | cncff 21925 |
. . . . . . . . . . . . 13
 
                                                                     |
223 | | fdm 5733 |
. . . . . . . . . . . . 13
 
                                 
                               |
224 | 221, 222,
223 | 3syl 18 |
. . . . . . . . . . . 12
 
 ..^ 
                                |
225 | | ssdmres 5126 |
. . . . . . . . . . . 12
              
                                |
226 | 224, 225 | sylibr 216 |
. . . . . . . . . . 11
 
 ..^                  |
227 | 184 | adantr 467 |
. . . . . . . . . . 11
 
 ..^ 
  |
228 | 226, 227 | sseqtrd 3468 |
. . . . . . . . . 10
 
 ..^                  |
229 | 228 | 3adant3 1028 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)                      
  |
230 | 220, 229 | sstrd 3442 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)                    
  |
231 | 208, 230 | ssind 3656 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)                    
           |
232 | | fourierdlem49.d |
. . . . . . . . . 10

  |
233 | 232, 191 | sstrd 3442 |
. . . . . . . . 9

  |
234 | 233 | 3ad2ant1 1029 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)           |
235 | 194, 234 | syl5ss 3443 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)                    |
236 | | eqid 2451 |
. . . . . . 7
  ℂfld   ℂfld |
237 | | eqid 2451 |
. . . . . . 7
   ℂfld ↾t                      ℂfld
↾t                    |
238 | 136 | 3ad2ant1 1029 |
. . . . . . . . . 10
 
 ..^           ![(,] (,]](_ioc.gif)               |
239 | 238 | rexrd 9690 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)               |
240 | | iocgtlb 37599 |
. . . . . . . . . 10
           
          ![(,] (,]](_ioc.gif)                   |
241 | 215, 213,
216, 240 | syl3anc 1268 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)            
      |
242 | 238 | leidd 10180 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)            
      |
243 | 215, 239,
239, 241, 242 | eliocd 37605 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)                   ![(,] (,]](_ioc.gif)        |
244 | | snunioo2 37606 |
. . . . . . . . . . 11
                                             ![(,] (,]](_ioc.gif)        |
245 | 215, 239,
241, 244 | syl3anc 1268 |
. . . . . . . . . 10
 
 ..^           ![(,] (,]](_ioc.gif)                                   ![(,] (,]](_ioc.gif)        |
246 | 245 | fveq2d 5869 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)                ℂfld
↾t                                                  ℂfld
↾t                            ![(,] (,]](_ioc.gif)         |
247 | 236 | cnfldtop 21804 |
. . . . . . . . . . 11
  ℂfld  |
248 | | ovex 6318 |
. . . . . . . . . . . . 13
        |
249 | 248 | inex1 4544 |
. . . . . . . . . . . 12
          |
250 | | snex 4641 |
. . . . . . . . . . . 12
       |
251 | 249, 250 | unex 6589 |
. . . . . . . . . . 11
        
         |
252 | | resttop 20176 |
. . . . . . . . . . 11
    ℂfld
                     ℂfld ↾t                     |
253 | 247, 251,
252 | mp2an 678 |
. . . . . . . . . 10
   ℂfld ↾t                    |
254 | | retop 21782 |
. . . . . . . . . . . . 13
     |
255 | 254 | a1i 11 |
. . . . . . . . . . . 12
 
 ..^           ![(,] (,]](_ioc.gif)               |
256 | 251 | a1i 11 |
. . . . . . . . . . . 12
 
 ..^           ![(,] (,]](_ioc.gif)                            |
257 | | iooretop 21786 |
. . . . . . . . . . . . 13
            |
258 | 257 | a1i 11 |
. . . . . . . . . . . 12
 
 ..^           ![(,] (,]](_ioc.gif)               
      |
259 | | elrestr 15327 |
. . . . . . . . . . . 12
              
             
     
      
                        ↾t                     |
260 | 255, 256,
258, 259 | syl3anc 1268 |
. . . . . . . . . . 11
 
 ..^           ![(,] (,]](_ioc.gif)                
                       ↾t                     |
261 | | simpr 463 |
. . . . . . . . . . . . . . . 16
    ..^           ![(,] (,]](_ioc.gif)                    |
262 | | pnfxr 11412 |
. . . . . . . . . . . . . . . . . . . 20
 |
263 | 262 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^           ![(,] (,]](_ioc.gif)           |
264 | 238 | ltpnfd 11423 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^           ![(,] (,]](_ioc.gif)            
  |
265 | 215, 263,
238, 241, 264 | eliood 37595 |
. . . . . . . . . . . . . . . . . 18
 
 ..^           ![(,] (,]](_ioc.gif)                      |
266 | | snidg 3994 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
267 | | elun2 3602 |
. . . . . . . . . . . . . . . . . . . . 21
                                  |
268 | 266, 267 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                            |
269 | 136, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
             
          |
270 | 269 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . 18
 
 ..^           ![(,] (,]](_ioc.gif)                     
          |
271 | 265, 270 | elind 3618 |
. . . . . . . . . . . . . . . . 17
 
 ..^           ![(,] (,]](_ioc.gif)                   
                     |
272 | 271 | adantr 467 |
. . . . . . . . . . . . . . . 16
    ..^           ![(,] (,]](_ioc.gif)                         
                    |
273 | 261, 272 | eqeltrd 2529 |
. . . . . . . . . . . . . . 15
    ..^           ![(,] (,]](_ioc.gif)                     
                    |
274 | 273 | adantlr 721 |
. . . . . . . . . . . . . 14
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)           
      
                     |
275 | 215 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)             |
276 | 262 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)         |
277 | 203 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    ..^        ![(,] (,]](_ioc.gif)             |
278 | 136 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^        |
279 | 278 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    ..^        ![(,] (,]](_ioc.gif)             |
280 | | iocssre 11714 |
. . . . . . . . . . . . . . . . . . . 20
                 ![(,] (,]](_ioc.gif)        |
281 | 277, 279,
280 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
    ..^        ![(,] (,]](_ioc.gif)             ![(,] (,]](_ioc.gif)        |
282 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
    ..^        ![(,] (,]](_ioc.gif)             ![(,] (,]](_ioc.gif)        |
283 | 281, 282 | sseldd 3433 |
. . . . . . . . . . . . . . . . . 18
    ..^        ![(,] (,]](_ioc.gif)         |
284 | 283 | 3adantl3 1166 |
. . . . . . . . . . . . . . . . 17
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)         |
285 | 279 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . 19
    ..^        ![(,] (,]](_ioc.gif)             |
286 | | iocgtlb 37599 |
. . . . . . . . . . . . . . . . . . 19
                ![(,] (,]](_ioc.gif)             |
287 | 277, 285,
282, 286 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18
    ..^        ![(,] (,]](_ioc.gif)             |
288 | 287 | 3adantl3 1166 |
. . . . . . . . . . . . . . . . 17
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)             |
289 | 284 | ltpnfd 11423 |
. . . . . . . . . . . . . . . . 17
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)         |
290 | 275, 276,
284, 288, 289 | eliood 37595 |
. . . . . . . . . . . . . . . 16
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)                |
291 | 290 | adantr 467 |
. . . . . . . . . . . . . . 15
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
         |
292 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
  |
293 | 285 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
      |
294 | 283 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
  |
295 | 294 | mnfltd 11426 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
  |
296 | 136 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
      |
297 | | iocleub 37600 |
. . . . . . . . . . . . . . . . . . . . . 22
                ![(,] (,]](_ioc.gif)             |
298 | 277, 285,
282, 297 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^        ![(,] (,]](_ioc.gif)             |
299 | 298 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
      |
300 | | neqne 37374 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
301 | 300 | necomd 2679 |
. . . . . . . . . . . . . . . . . . . . 21
           |
302 | 301 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
      |
303 | 294, 296,
299, 302 | leneltd 9789 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
      |
304 | 292, 293,
294, 295, 303 | eliood 37595 |
. . . . . . . . . . . . . . . . . 18
   
 ..^ 
      ![(,] (,]](_ioc.gif)      
    
         |
305 | 304 | 3adantll3 37365 |
. . . . . . . . . . . . . . . . 17
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
         |
306 | 229 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
                  
  |
307 | 275 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
           |
308 | 213 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
             |
309 | 284 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
  |
310 | 288 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
        
  |
311 | 238 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
           |
312 | 212 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
             |
313 | 303 | 3adantll3 37365 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
           |
314 | 218 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
        
        |
315 | 309, 311,
312, 313, 314 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
             |
316 | 307, 308,
309, 310, 315 | eliood 37595 |
. . . . . . . . . . . . . . . . . 18
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
                |
317 | 306, 316 | sseldd 3433 |
. . . . . . . . . . . . . . . . 17
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
  |
318 | 305, 317 | elind 3618 |
. . . . . . . . . . . . . . . 16
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
           |
319 | | elun1 3601 |
. . . . . . . . . . . . . . . 16
         
                   |
320 | 318, 319 | syl 17 |
. . . . . . . . . . . . . . 15
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
                   |
321 | 291, 320 | elind 3618 |
. . . . . . . . . . . . . 14
   
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      
    
      
                     |
322 | 274, 321 | pm2.61dan 800 |
. . . . . . . . . . . . 13
    ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)              
                    |
323 | 215 | adantr 467 |
. . . . . . . . . . . . . 14
    ..^           ![(,] (,]](_ioc.gif)                
                         |
324 | 239 | adantr 467 |
. . . . . . . . . . . . . 14
    ..^           ![(,] (,]](_ioc.gif)                
                         |
325 | | elinel1 3619 |
. . . . . . . . . . . . . . . 16
                          
         |
326 | | elioore 11666 |
. . . . . . . . . . . . . . . . 17
       
  |
327 | 326 | rexrd 9690 |
. . . . . . . . . . . . . . . 16
       
  |
328 | 325, 327 | syl 17 |
. . . . . . . . . . . . . . 15
                          
  |
329 | 328 | adantl 468 |
. . . . . . . . . . . . . 14
    ..^           ![(,] (,]](_ioc.gif)                
                  
  |
330 | 203 | adantr 467 |
. . . . . . . . . . . . . . . 16
    ..^         
                         |
331 | 262 | a1i 11 |
. . . . . . . . . . . . . . . 16
    ..^         
                     |
332 | 325 | adantl 468 |
. . . . . . . . . . . . . . . 16
    ..^         
                  
         |
333 | | ioogtlb 37592 |
. . . . . . . . . . . . . . . 16
                    |
334 | 330, 331,
332, 333 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
    ..^         
                      
  |
335 | 334 | 3adantl3 1166 |
. . . . . . . . . . . . . 14
    ..^           ![(,] (,]](_ioc.gif)                
                      
  |
336 | | elinel2 3620 |
. . . . . . . . . . . . . . . 16
                          
                   |
337 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . 21
             |
338 | 337 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
      
      |
339 | 137 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
          
      |
340 | 338, 339 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . . 19
 
             |
341 | 340 | adantlr 721 |
. . . . . . . . . . . . . . . . . 18
                    
             |
342 | | simpll 760 |
. . . . . . . . . . . . . . . . . . 19
                    
         |
343 | | elunnel2 37360 |
. . . . . . . . . . . . . . . . . . . 20
          
                      
   |
344 | 343 | adantll 720 |
. . . . . . . . . . . . . . . . . . 19
                    
                  |
345 | | elinel1 3619 |
. . . . . . . . . . . . . . . . . . . 20
         
         |
346 | | elioore 11666 |
. . . . . . . . . . . . . . . . . . . . . 22
       
  |
347 | 346 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
       
  |
348 | 136 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
       
      |
349 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       
  |
350 | 348 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       
      |
351 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       
         |
352 | | iooltub 37610 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
353 | 349, 350,
351, 352 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
 
       
      |
354 | 347, 348,
353 | ltled 9783 |
. . . . . . . . . . . . . . . . . . . 20
 
       
      |
355 | 345, 354 | sylan2 477 |
. . . . . . . . . . . . . . . . . . 19
 
         
      |
356 | 342, 344,
355 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                    
             |
357 | 341, 356 | pm2.61dan 800 |
. . . . . . . . . . . . . . . . 17
 
                        |
358 | 357 | adantlr 721 |
. . . . . . . . . . . . . . . 16
    ..^                          |
359 | 336, 358 | sylan2 477 |
. . . . . . . . . . . . . . 15
    ..^         
                         |
360 | 359 | 3adantl3 1166 |
. . . . . . . . . . . . . 14
    ..^           ![(,] (,]](_ioc.gif)                
                         |
361 | 323, 324,
329, 335, 360 | eliocd 37605 |
. . . . . . . . . . . . 13
    ..^           ![(,] (,]](_ioc.gif)                
                  
      ![(,] (,]](_ioc.gif)        |
362 | 322, 361 | impbida 843 |
. . . . . . . . . . . 12
 
 ..^           ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)            
                      |
363 | 362 | eqrdv 2449 |
. . . . . . . . . . 11
 
 ..^           ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)      |