Step | Hyp | Ref
| Expression |
1 | | ioossre 11696 |
. . . . . . . 8
          
    |
2 | 1 | a1i 11 |
. . . . . . 7
              
  |
3 | 2 | sselda 3432 |
. . . . . 6
 
                 |
4 | | iftrue 3887 |
. . . . . . . . . . 11
                |
5 | 4 | adantl 468 |
. . . . . . . . . 10
 
                |
6 | | fourierdlem97.f |
. . . . . . . . . . . . . 14
       |
7 | | ssid 3451 |
. . . . . . . . . . . . . 14
 |
8 | | dvfre 22905 |
. . . . . . . . . . . . . 14
                 |
9 | 6, 7, 8 | sylancl 668 |
. . . . . . . . . . . . 13
           |
10 | | fourierdlem97.g |
. . . . . . . . . . . . . 14
   |
11 | 10 | feq1i 5720 |
. . . . . . . . . . . . 13
                 |
12 | 9, 11 | sylibr 216 |
. . . . . . . . . . . 12
         |
13 | 12 | adantr 467 |
. . . . . . . . . . 11
 
         |
14 | | id 22 |
. . . . . . . . . . . . 13
   |
15 | 10 | dmeqi 5036 |
. . . . . . . . . . . . 13
   |
16 | 14, 15 | syl6eleq 2539 |
. . . . . . . . . . . 12
     |
17 | 16 | adantl 468 |
. . . . . . . . . . 11
 
     |
18 | 13, 17 | ffvelrnd 6023 |
. . . . . . . . . 10
 
       |
19 | 5, 18 | eqeltrd 2529 |
. . . . . . . . 9
 
            |
20 | 19 | adantlr 721 |
. . . . . . . 8
                |
21 | | iffalse 3890 |
. . . . . . . . . 10
            |
22 | | 0red 9644 |
. . . . . . . . . 10
   |
23 | 21, 22 | eqeltrd 2529 |
. . . . . . . . 9
            |
24 | 23 | adantl 468 |
. . . . . . . 8
   
            |
25 | 20, 24 | pm2.61dan 800 |
. . . . . . 7
 

           |
26 | 3, 25 | syldan 473 |
. . . . . 6
 
                          |
27 | | fourierdlem97.h |
. . . . . . 7
            |
28 | 27 | fvmpt2 5957 |
. . . . . 6
                           |
29 | 3, 26, 28 | syl2anc 667 |
. . . . 5
 
                              |
30 | | fourierdlem97.t |
. . . . . . . . . 10
   |
31 | | fourierdlem97.p |
. . . . . . . . . 10
 
                 
 ..^                |
32 | | fourierdlem97.m |
. . . . . . . . . 10
   |
33 | | fourierdlem97.q |
. . . . . . . . . 10
       |
34 | | fourierdlem97.c |
. . . . . . . . . 10
   |
35 | | fourierdlem97.d |
. . . . . . . . . . 11
      |
36 | | elioore 11666 |
. . . . . . . . . . 11
   
  |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
   |
38 | 34 | rexrd 9690 |
. . . . . . . . . . 11
   |
39 | | pnfxr 11412 |
. . . . . . . . . . . 12
 |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
   |
41 | | ioogtlb 37592 |
. . . . . . . . . . 11
        |
42 | 38, 40, 35, 41 | syl3anc 1268 |
. . . . . . . . . 10
   |
43 | | oveq1 6297 |
. . . . . . . . . . . . . 14
      
    |
44 | 43 | eleq1d 2513 |
. . . . . . . . . . . . 13
             |
45 | 44 | rexbidv 2901 |
. . . . . . . . . . . 12
  
            |
46 | 45 | cbvrabv 3044 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)    
    |
47 | 46 | uneq2i 3585 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)    
     |
48 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . 19
       |
49 | 48 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
           |
50 | 49 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
             |
51 | 50 | cbvrexv 3020 |
. . . . . . . . . . . . . . . 16
     
       |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)   
            |
53 | 52 | rabbiia 3033 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)         |
54 | 53 | uneq2i 3585 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)          |
55 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . 19
       |
56 | 55 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
           |
57 | 56 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
             |
58 | 57 | cbvrexv 3020 |
. . . . . . . . . . . . . . . 16
     
       |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)   
            |
60 | 59 | rabbiia 3033 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)         |
61 | 60 | uneq2i 3585 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)          |
62 | 54, 61 | eqtri 2473 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)          |
63 | 62 | fveq2i 5868 |
. . . . . . . . . . 11
      
   ![[,] [,]](_icc.gif)  
            
    ![[,] [,]](_icc.gif)           |
64 | 63 | oveq1i 6300 |
. . . . . . . . . 10
      
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)            |
65 | | fourierdlem97.v |
. . . . . . . . . 10
                  ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
         |
66 | | fourierdlem97.j |
. . . . . . . . . 10
  ..^           ![[,] [,]](_icc.gif)              |
67 | | oveq1 6297 |
. . . . . . . . . . . . . 14
       |
68 | 67 | oveq2d 6306 |
. . . . . . . . . . . . 13
                   |
69 | 68 | breq1d 4412 |
. . . . . . . . . . . 12
         
   
               |
70 | 69 | cbvrabv 3044 |
. . . . . . . . . . 11
              
              |
71 | 70 | supeq1i 7961 |
. . . . . . . . . 10
                
   
             
  |
72 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
73 | 72 | oveq1d 6305 |
. . . . . . . . . . . . 13
                                                       |
74 | 73 | breq1d 4412 |
. . . . . . . . . . . 12
                         
                      
      
         |
75 | 74 | cbvrabv 3044 |
. . . . . . . . . . 11
  ..^                       
  
       ..^                        
        |
76 | 75 | supeq1i 7961 |
. . . . . . . . . 10
    ..^                        
             ..^                        
          |
77 | 30, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76 | fourierdlem64 38034 |
. . . . . . . . 9
       ..^                        
          ..^                      ..^                
                         |
78 | 77 | simprd 465 |
. . . . . . . 8
   ..^                                         |
79 | | simpl1 1011 |
. . . . . . . . . . . . . . 15
     ..^                                      
          
      |
80 | | simpl2l 1061 |
. . . . . . . . . . . . . . 15
     ..^                                      
          
     ..^   |
81 | | fourierdlem97.qcn |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^                                      |
82 | | cncff 21925 |
. . . . . . . . . . . . . . . . . . . . 21
 
                                                                     |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^                                      |
84 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
85 | 12, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
86 | 85 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^ 
  |
87 | | ffvresb 6054 |
. . . . . . . . . . . . . . . . . . . . 21

                                  
                
        |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^                                                              |
89 | 83, 88 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                          |
90 | 89 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . 18
    ..^                         |
91 | 90 | simpld 461 |
. . . . . . . . . . . . . . . . 17
    ..^                   |
92 | 91 | ralrimiva 2802 |
. . . . . . . . . . . . . . . 16
 
 ..^                    |
93 | | dfss3 3422 |
. . . . . . . . . . . . . . . 16
              
                  |
94 | 92, 93 | sylibr 216 |
. . . . . . . . . . . . . . 15
 
 ..^                  |
95 | 79, 80, 94 | syl2anc 667 |
. . . . . . . . . . . . . 14
     ..^                                      
          
                 
  |
96 | | simpl2 1012 |
. . . . . . . . . . . . . . . 16
     ..^                                      
          
      ..^
   |
97 | 79, 96 | jca 535 |
. . . . . . . . . . . . . . 15
     ..^                                      
          
    
  ..^     |
98 | | simpl3 1013 |
. . . . . . . . . . . . . . . 16
     ..^                                      
          
                 
                        |
99 | | simpr 463 |
. . . . . . . . . . . . . . . 16
     ..^                                      
          
              
     |
100 | 98, 99 | sseldd 3433 |
. . . . . . . . . . . . . . 15
     ..^                                      
          
                            |
101 | 31 | fourierdlem2 37971 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   
                  
 ..^                 |
102 | 32, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                        
 ..^                 |
103 | 33, 102 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
 ..^                |
104 | 103 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
105 | | elmapi 7493 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
           |
107 | 106 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^            |
108 | | elfzofz 11935 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
      |
109 | 108 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^        |
110 | 107, 109 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^        |
111 | 110 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
112 | 111 | adantrr 723 |
. . . . . . . . . . . . . . . . 17
 
  ..^         |
113 | 112 | adantr 467 |
. . . . . . . . . . . . . . . 16
     ..^  
                             |
114 | | fzofzp1 12008 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
        |
115 | 114 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^          |
116 | 107, 115 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^          |
117 | 116 | adantrr 723 |
. . . . . . . . . . . . . . . . . 18
 
  ..^           |
118 | 117 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     ..^  
                               |
119 | 118 | rexrd 9690 |
. . . . . . . . . . . . . . . 16
     ..^  
                               |
120 | | elioore 11666 |
. . . . . . . . . . . . . . . . . 18
                         |
121 | 120 | adantl 468 |
. . . . . . . . . . . . . . . . 17
     ..^  
                         |
122 | | zre 10941 |
. . . . . . . . . . . . . . . . . . . 20
   |
123 | 122 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   ..^    |
124 | 123 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
     ..^  
                         |
125 | | fourierdlem97.a |
. . . . . . . . . . . . . . . . . . . . 21
   |
126 | | fourierdlem97.b |
. . . . . . . . . . . . . . . . . . . . 21
   |
127 | 125, 126 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . 20
     |
128 | 30, 127 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . 19
   |
129 | 128 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
     ..^  
                         |
130 | 124, 129 | remulcld 9671 |
. . . . . . . . . . . . . . . . 17
     ..^  
                           |
131 | 121, 130 | resubcld 10047 |
. . . . . . . . . . . . . . . 16
     ..^  
                             |
132 | 110 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ..^         |
133 | 122 | ad2antll 735 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  ..^     |
134 | 128 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  ..^     |
135 | 133, 134 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ..^       |
136 | 132, 135 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . 20
 
  ..^             |
137 | 136 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . 19
 
  ..^             |
138 | 137 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     ..^  
                                 |
139 | 117, 135 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . 20
 
  ..^               |
140 | 139 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . 19
 
  ..^               |
141 | 140 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     ..^  
                                   |
142 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
     ..^  
                                               |
143 | | ioogtlb 37592 |
. . . . . . . . . . . . . . . . . 18
                   
                                 |
144 | 138, 141,
142, 143 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
     ..^  
                                 |
145 | 132 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     ..^  
                             |
146 | 145, 130,
121 | ltaddsubd 10213 |
. . . . . . . . . . . . . . . . 17
     ..^  
                                           |
147 | 144, 146 | mpbid 214 |
. . . . . . . . . . . . . . . 16
     ..^  
                                 |
148 | | iooltub 37610 |
. . . . . . . . . . . . . . . . . 18
                   
                                   |
149 | 138, 141,
142, 148 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
     ..^  
                                   |
150 | 121, 130,
118 | ltsubaddd 10209 |
. . . . . . . . . . . . . . . . 17
     ..^  
                                               |
151 | 149, 150 | mpbird 236 |
. . . . . . . . . . . . . . . 16
     ..^  
                                   |
152 | 113, 119,
131, 147, 151 | eliood 37595 |
. . . . . . . . . . . . . . 15
     ..^  
                                           |
153 | 97, 100, 152 | syl2anc 667 |
. . . . . . . . . . . . . 14
     ..^                                      
          
                        |
154 | 95, 153 | sseldd 3433 |
. . . . . . . . . . . . 13
     ..^                                      
          
          |
155 | | elioore 11666 |
. . . . . . . . . . . . . . . 16
           
     |
156 | | recn 9629 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
157 | 156 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
       |
158 | | zcn 10942 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
159 | 158 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
160 | 128 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
161 | 160 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
162 | 159, 161 | mulcld 9663 |
. . . . . . . . . . . . . . . . . . . . 21
         |
163 | 157, 162 | npcand 9990 |
. . . . . . . . . . . . . . . . . . . 20
               |
164 | 163 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . 19
               |
165 | 164 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   

     
          |
166 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . 21
     |
167 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
168 | 167 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . . . 22
       

            |
169 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
170 | 169 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
171 | 169 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           |
172 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
173 | 171, 172 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 
                       |
174 | 170, 173 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . 22
                                
                        |
175 | 168, 174 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . 21
          
                           
                                  |
176 | | ax-resscn 9596 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
178 | 6, 177 | fssd 5738 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
179 | 178 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 

      |
180 | 122 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
181 | 128 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
182 | 180, 181 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
183 | 178 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
184 | 128 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
185 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
186 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
187 | | fourierdlem97.fper |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

            |
188 | 187 | adant423 37367 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

     
        |
189 | 183, 184,
185, 186, 188 | fperiodmul 37522 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
190 | 179, 182,
189, 10 | fperdvper 37790 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
191 | 166, 175,
190 | vtocl 3100 |
. . . . . . . . . . . . . . . . . . . 20
                 
                       |
192 | 191 | simpld 461 |
. . . . . . . . . . . . . . . . . . 19
                   |
193 | 192 | adantlr 721 |
. . . . . . . . . . . . . . . . . 18
   

     
          |
194 | 165, 193 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . 17
   

     
  |
195 | 194 | ex 436 |
. . . . . . . . . . . . . . . 16
             |
196 | 155, 195 | sylan2 477 |
. . . . . . . . . . . . . . 15
                           |
197 | 196 | adantlrl 726 |
. . . . . . . . . . . . . 14
     ..^  
          
            |
198 | 197 | 3adantl3 1166 |
. . . . . . . . . . . . 13
     ..^                                      
          
            |
199 | 154, 198 | mpd 15 |
. . . . . . . . . . . 12
     ..^                                      
          
      |
200 | 199 | ralrimiva 2802 |
. . . . . . . . . . 11
 
  ..^            
                         
                  |
201 | | dfss3 3422 |
. . . . . . . . . . 11
              
                  |
202 | 200, 201 | sylibr 216 |
. . . . . . . . . 10
 
  ..^            
                         
          
     |
203 | 202 | 3exp 1207 |
. . . . . . . . 9
    ..^             
                        
          
       |
204 | 203 | rexlimdvv 2885 |
. . . . . . . 8
    ..^                
                                   
   |
205 | 78, 204 | mpd 15 |
. . . . . . 7
              
  |
206 | 205 | sselda 3432 |
. . . . . 6
 
                 |
207 | 206 | iftrued 3889 |
. . . . 5
 
                              |
208 | 29, 207 | eqtr2d 2486 |
. . . 4
 
                         |
209 | 208 | mpteq2dva 4489 |
. . 3
                                
          |
210 | 15 | a1i 11 |
. . . . . 6
 
   |
211 | 210 | feq2d 5715 |
. . . . 5
               |
212 | 12, 211 | mpbird 236 |
. . . 4
       |
213 | 212, 205 | feqresmpt 5919 |
. . 3
                            
          |
214 | 25, 27 | fmptd 6046 |
. . . 4
       |
215 | 214, 2 | feqresmpt 5919 |
. . 3
                            
          |
216 | 209, 213,
215 | 3eqtr4d 2495 |
. 2
                                   |
217 | 214, 177 | fssd 5738 |
. . 3
       |
218 | 27 | a1i 11 |
. . . . . 6
    
             |
219 | | eleq1 2517 |
. . . . . . . . 9
         |
220 | | fveq2 5865 |
. . . . . . . . 9
          
    |
221 | 219, 220 | ifbieq1d 3904 |
. . . . . . . 8
                    
      |
222 | 178, 128,
187, 10 | fperdvper 37790 |
. . . . . . . . . 10
 
                 |
223 | 222 | simpld 461 |
. . . . . . . . 9
 
     |
224 | 223 | iftrued 3889 |
. . . . . . . 8
 
         
            |
225 | 221, 224 | sylan9eqr 2507 |
. . . . . . 7
   
                    |
226 | 225 | adantllr 725 |
. . . . . 6
   

                     |
227 | | simpr 463 |
. . . . . . . 8
 

  |
228 | 128 | adantr 467 |
. . . . . . . 8
 

  |
229 | 227, 228 | readdcld 9670 |
. . . . . . 7
 

    |
230 | 229 | adantr 467 |
. . . . . 6
         |
231 | 212 | ad2antrr 732 |
. . . . . . 7
           |
232 | 223 | adantlr 721 |
. . . . . . 7
         |
233 | 231, 232 | ffvelrnd 6023 |
. . . . . 6
             |
234 | 218, 226,
230, 233 | fvmptd 5954 |
. . . . 5
                   |
235 | 222 | simprd 465 |
. . . . . 6
 
             |
236 | 235 | adantlr 721 |
. . . . 5
                 |
237 | | eleq1 2517 |
. . . . . . . . 9
     |
238 | | fveq2 5865 |
. . . . . . . . 9
           |
239 | 237, 238 | ifbieq1d 3904 |
. . . . . . . 8
                     |
240 | 239 | adantl 468 |
. . . . . . 7
   

                      |
241 | | simplr 762 |
. . . . . . 7
    
  |
242 | | simpr 463 |
. . . . . . . . . 10
 
   |
243 | 242 | iftrued 3889 |
. . . . . . . . 9
 
  
             |
244 | 212 | ffvelrnda 6022 |
. . . . . . . . 9
 
       |
245 | 243, 244 | eqeltrd 2529 |
. . . . . . . 8
 
  
         |
246 | 245 | adantlr 721 |
. . . . . . 7
                |
247 | 218, 240,
241, 246 | fvmptd 5954 |
. . . . . 6
                    |
248 | | simpr 463 |
. . . . . . 7
    
  |
249 | 248 | iftrued 3889 |
. . . . . 6
                    |
250 | 247, 249 | eqtr2d 2486 |
. . . . 5
               |
251 | 234, 236,
250 | 3eqtrd 2489 |
. . . 4
                 |
252 | 229 | recnd 9669 |
. . . . . . . . . . 11
 

    |
253 | 228 | recnd 9669 |
. . . . . . . . . . 11
 

  |
254 | 252, 253 | negsubd 9992 |
. . . . . . . . . 10
 

           |
255 | 227 | recnd 9669 |
. . . . . . . . . . 11
 

  |
256 | 255, 253 | pncand 9987 |
. . . . . . . . . 10
 

      |
257 | 254, 256 | eqtr2d 2486 |
. . . . . . . . 9
 

       |
258 | 257 | adantr 467 |
. . . . . . . 8
              |
259 | | simpr 463 |
. . . . . . . . . 10
           |
260 | | simpll 760 |
. . . . . . . . . . 11
         |
261 | 260, 259 | jca 535 |
. . . . . . . . . 10
        
    |
262 | | eleq1 2517 |
. . . . . . . . . . . . 13
         |
263 | 262 | anbi2d 710 |
. . . . . . . . . . . 12
    

       |
264 | | oveq1 6297 |
. . . . . . . . . . . . . 14
             |
265 | 264 | eleq1d 2513 |
. . . . . . . . . . . . 13
               |
266 | 264 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                     |
267 | | fveq2 5865 |
. . . . . . . . . . . . . 14
          
    |
268 | 266, 267 | eqeq12d 2466 |
. . . . . . . . . . . . 13
                                 |
269 | 265, 268 | anbi12d 717 |
. . . . . . . . . . . 12
       
           
                         |
270 | 263, 269 | imbi12d 322 |
. . . . . . . . . . 11
     
    
               
 
                          |
271 | 128 | renegcld 10046 |
. . . . . . . . . . . 12
    |
272 | 160 | mulm1d 10070 |
. . . . . . . . . . . . . . . . 17
       |
273 | 272 | eqcomd 2457 |
. . . . . . . . . . . . . . . 16
       |
274 | 273 | adantr 467 |
. . . . . . . . . . . . . . 15
 

      |
275 | 274 | oveq2d 6306 |
. . . . . . . . . . . . . 14
 

          |
276 | 275 | fveq2d 5869 |
. . . . . . . . . . . . 13
 

                  |
277 | 178 | adantr 467 |
. . . . . . . . . . . . . 14
 

      |
278 | 128 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
279 | | 1zzd 10968 |
. . . . . . . . . . . . . . 15
 

  |
280 | 279 | znegcld 11042 |
. . . . . . . . . . . . . 14
 

   |
281 | | simpr 463 |
. . . . . . . . . . . . . 14
 

  |
282 | 187 | adantlr 721 |
. . . . . . . . . . . . . 14
                 |
283 | 277, 278,
280, 281, 282 | fperiodmul 37522 |
. . . . . . . . . . . . 13
 

               |
284 | 276, 283 | eqtrd 2485 |
. . . . . . . . . . . 12
 

             |
285 | 178, 271,
284, 10 | fperdvper 37790 |
. . . . . . . . . . 11
 
                   |
286 | 270, 285 | vtoclg 3107 |
. . . . . . . . . 10
     
 
                         |
287 | 259, 261,
286 | sylc 62 |
. . . . . . . . 9
            
            
     |
288 | 287 | simpld 461 |
. . . . . . . 8
              |
289 | 258, 288 | eqeltrd 2529 |
. . . . . . 7
         |
290 | 289 | stoic1a 1655 |
. . . . . 6
   

    |
291 | 290 | iffalsed 3892 |
. . . . 5
   
                |
292 | 27 | a1i 11 |
. . . . . 6
   
              |
293 | 221 | adantl 468 |
. . . . . 6
   
                      
      |
294 | 229 | adantr 467 |
. . . . . 6
   
     |
295 | | 0red 9644 |
. . . . . . 7
   
   |
296 | 291, 295 | eqeltrd 2529 |
. . . . . 6
   
                |
297 | 292, 293,
294, 296 | fvmptd 5954 |
. . . . 5
   
    
          
      |
298 | | simpr 463 |
. . . . . . . 8
   

  |
299 | 298 | iffalsed 3892 |
. . . . . . 7
   
            |
300 | 239, 299 | sylan9eqr 2507 |
. . . . . 6
   
              |
301 | | simplr 762 |
. . . . . 6
   
   |
302 | 292, 300,
301, 295 | fvmptd 5954 |
. . . . 5
   
       |
303 | 291, 297,
302 | 3eqtr4d 2495 |
. . . 4
   
    
        |
304 | 251, 303 | pm2.61dan 800 |
. . 3
 

            |
305 | | elioore 11666 |
. . . . . . . . . 10
                 |
306 | 305 | adantl 468 |
. . . . . . . . 9
 
                 |
307 | 305, 25 | sylan2 477 |
. . . . . . . . 9
 
                          |
308 | 306, 307,
28 | syl2anc 667 |
. . . . . . . 8
 
                              |
309 | 308 | adantlr 721 |
. . . . . . 7
    ..^                                |
310 | 91 | iftrued 3889 |
. . . . . . 7
    ..^                                |
311 | 309, 310 | eqtrd 2485 |
. . . . . 6
    ..^                           |
312 | 311 | mpteq2dva 4489 |
. . . . 5
 
 ..^                                            |
313 | 214 | adantr 467 |
. . . . . 6
 
 ..^        |
314 | | ioossre 11696 |
. . . . . . 7
               |
315 | 314 | a1i 11 |
. . . . . 6
 
 ..^                  |
316 | 313, 315 | feqresmpt 5919 |
. . . . 5
 
 ..^                                        |
317 | 212 | adantr 467 |
. . . . . 6
 
 ..^        |
318 | 317, 94 | feqresmpt 5919 |
. . . . 5
 
 ..^                                        |
319 | 312, 316,
318 | 3eqtr4d 2495 |
. . . 4
 
 ..^                  
                 |
320 | 319, 81 | eqeltrd 2529 |
. . 3
 
 ..^                                      |
321 | | eqid 2451 |
. . 3
                   
 ..^                                  
 ..^                |
322 | | oveq1 6297 |
. . . . . . . 8
           |
323 | 322 | eleq1d 2513 |
. . . . . . 7
             |
324 | 323 | rexbidv 2901 |
. . . . . 6
  
            |
325 | 324 | cbvrabv 3044 |
. . . . 5
   ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)         |
326 | 325 | uneq2i 3585 |
. . . 4
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)          |
327 | 326 | eqcomi 2460 |
. . 3
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)          |
328 | 54 | fveq2i 5868 |
. . . 4
      
   ![[,] [,]](_icc.gif)  
            
    ![[,] [,]](_icc.gif)           |
329 | 328 | oveq1i 6300 |
. . 3
      
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)            |
330 | | isoeq5 6214 |
. . . . . 6
    
   ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)         
               ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
      
           
   ![[,] [,]](_icc.gif)  
             
   ![[,] [,]](_icc.gif)             |
331 | 61, 330 | ax-mp 5 |
. . . . 5
                ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
      
           
   ![[,] [,]](_icc.gif)  
             
   ![[,] [,]](_icc.gif)            |
332 | 331 | iotabii 5568 |
. . . 4
              
   ![[,] [,]](_icc.gif)  
             
   ![[,] [,]](_icc.gif)             
               ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
         |
333 | | isoeq1 6210 |
. . . . 5
 
               ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
      
           
   ![[,] [,]](_icc.gif)  
             
   ![[,] [,]](_icc.gif)             |
334 | 333 | cbviotav 5552 |
. . . 4
              
   ![[,] [,]](_icc.gif)  
             
   ![[,] [,]](_icc.gif)             
               ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
         |
335 | 332, 334,
65 | 3eqtr4ri 2484 |
. . 3
                  ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)  
         |
336 | | id 22 |
. . . . 5
   |
337 | | oveq2 6298 |
. . . . . . . 8
 
     |
338 | 337 | oveq1d 6305 |
. . . . . . 7
           |
339 | 338 | fveq2d 5869 |
. . . . . 6
                   |
340 | 339 | oveq1d 6305 |
. . . . 5
                       |
341 | 336, 340 | oveq12d 6308 |
. . . 4
                           |
342 | 341 | cbvmptv 4495 |
. . 3
                             |
343 | | eqeq1 2455 |
. . . . 5
 
   |
344 | | id 22 |
. . . . 5
   |
345 | 343, 344 | ifbieq2d 3906 |
. . . 4
  
          |
346 | 345 | cbvmptv 4495 |
. . 3
   ![(,] (,]](_ioc.gif)     
     ![(,] (,]](_ioc.gif)     
   |
347 | | eqid 2451 |
. . 3
                           
                                     |
348 | | eqid 2451 |
. . 3
      ![(,] (,]](_ioc.gif)     
    |