Step | Hyp | Ref
| Expression |
1 | | fourierdlem42OLD.x |
. . . . 5
   |
2 | | fourierdlem42OLD.y |
. . . . 5
   |
3 | | fourierdlem42OLD.j |
. . . . . 6
     |
4 | | fourierdlem42OLD.k |
. . . . . 6

↾t   ![[,] [,]](_icc.gif)    |
5 | 3, 4 | icccmp 21892 |
. . . . 5
 
   |
6 | 1, 2, 5 | syl2anc 671 |
. . . 4
   |
7 | 6 | adantr 471 |
. . 3
 
   |
8 | | fourierdlem42OLD.h |
. . . . . 6
   ![[,] [,]](_icc.gif)         |
9 | | ssrab2 3526 |
. . . . . . 7
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)   |
10 | 9 | a1i 11 |
. . . . . 6
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
11 | 8, 10 | syl5eqss 3488 |
. . . . 5

  ![[,] [,]](_icc.gif)    |
12 | | retop 21831 |
. . . . . . . 8
     |
13 | 3, 12 | eqeltri 2536 |
. . . . . . 7
 |
14 | 1, 2 | iccssred 37640 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
  |
15 | | uniretop 21832 |
. . . . . . . . 9
      |
16 | 3 | unieqi 4221 |
. . . . . . . . 9
       |
17 | 15, 16 | eqtr4i 2487 |
. . . . . . . 8
  |
18 | 17 | restuni 20227 |
. . . . . . 7
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ↾t   ![[,] [,]](_icc.gif)     |
19 | 13, 14, 18 | sylancr 674 |
. . . . . 6
   ![[,] [,]](_icc.gif)    ↾t   ![[,] [,]](_icc.gif)     |
20 | 4 | unieqi 4221 |
. . . . . . 7
   ↾t   ![[,] [,]](_icc.gif)    |
21 | 20 | eqcomi 2471 |
. . . . . 6
  ↾t   ![[,] [,]](_icc.gif)     |
22 | 19, 21 | syl6eq 2512 |
. . . . 5
   ![[,] [,]](_icc.gif)     |
23 | 11, 22 | sseqtrd 3480 |
. . . 4

   |
24 | 23 | adantr 471 |
. . 3
 
    |
25 | | simpr 467 |
. . 3
 

  |
26 | | eqid 2462 |
. . . 4
   |
27 | 26 | bwth 20474 |
. . 3
  
   
          |
28 | 7, 24, 25, 27 | syl3anc 1276 |
. 2
 
              |
29 | 11, 14 | sstrd 3454 |
. . . . . . . . . 10

  |
30 | 29 | ad2antrr 737 |
. . . . . . . . 9
    
           |
31 | | ne0i 3749 |
. . . . . . . . . 10
        
          |
32 | 31 | adantl 472 |
. . . . . . . . 9
    
                   |
33 | | fourierdlem42OLD.e |
. . . . . . . . . . 11
   
 |
34 | | fourierdlem42OLD.r |
. . . . . . . . . . . . 13
   |
35 | | absf 13449 |
. . . . . . . . . . . . . . . . . 18
     |
36 | | ffn 5751 |
. . . . . . . . . . . . . . . . . 18
       |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
38 | | subf 9903 |
. . . . . . . . . . . . . . . . . 18
      |
39 | | ffn 5751 |
. . . . . . . . . . . . . . . . . 18
     
   |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17

  |
41 | | frn 5758 |
. . . . . . . . . . . . . . . . . 18
       |
42 | 38, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
43 | | fnco 5706 |
. . . . . . . . . . . . . . . . 17
   
      |
44 | 37, 40, 42, 43 | mp3an 1373 |
. . . . . . . . . . . . . . . 16


  |
45 | | fourierdlem42OLD.d |
. . . . . . . . . . . . . . . . 17
  |
46 | 45 | fneq1i 5692 |
. . . . . . . . . . . . . . . 16
  

    |
47 | 44, 46 | mpbir 214 |
. . . . . . . . . . . . . . 15

  |
48 | | fourierdlem42OLD.i |
. . . . . . . . . . . . . . . 16
    |
49 | | fourierdlem42OLD.a |
. . . . . . . . . . . . . . . . . . 19

  ![[,] [,]](_icc.gif)    |
50 | | fourierdlem42OLD.b |
. . . . . . . . . . . . . . . . . . . . 21
   |
51 | | fourierdlem42OLD.c |
. . . . . . . . . . . . . . . . . . . . 21
   |
52 | 50, 51 | iccssred 37640 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif) 
  |
53 | | ax-resscn 9622 |
. . . . . . . . . . . . . . . . . . . 20
 |
54 | 52, 53 | syl6ss 3456 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif) 
  |
55 | 49, 54 | sstrd 3454 |
. . . . . . . . . . . . . . . . . 18

  |
56 | | xpss12 4959 |
. . . . . . . . . . . . . . . . . 18
 
   
   |
57 | 55, 55, 56 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
  
    |
58 | 57 | ssdifssd 3583 |
. . . . . . . . . . . . . . . 16
        |
59 | 48, 58 | syl5eqss 3488 |
. . . . . . . . . . . . . . 15

    |
60 | | fnssres 5711 |
. . . . . . . . . . . . . . 15
           |
61 | 47, 59, 60 | sylancr 674 |
. . . . . . . . . . . . . 14
     |
62 | | fvres 5902 |
. . . . . . . . . . . . . . . . . . 19
             |
63 | 62 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
 
             |
64 | 45 | fveq1i 5889 |
. . . . . . . . . . . . . . . . . . 19
          |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
      
     |
66 | | ffun 5754 |
. . . . . . . . . . . . . . . . . . . 20
      |
67 | 38, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 |
68 | 59 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
69 | 38 | fdmi 5757 |
. . . . . . . . . . . . . . . . . . . 20
   |
70 | 68, 69 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . . 19
 
  |
71 | | fvco 5964 |
. . . . . . . . . . . . . . . . . . 19
         
     |
72 | 67, 70, 71 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
 
  
           |
73 | 63, 65, 72 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . 17
 
               |
74 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
        |
75 | 74, 68 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . . . 18
 
     |
76 | 75 | abscld 13547 |
. . . . . . . . . . . . . . . . 17
 
         |
77 | 73, 76 | eqeltrd 2540 |
. . . . . . . . . . . . . . . 16
 
         |
78 | | elxp2 4871 |
. . . . . . . . . . . . . . . . . . . 20
  
       |
79 | 68, 78 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
 
        |
80 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
81 | 80 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . . . 22
    

             |
82 | | df-ov 6318 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
83 | | simp1l 1038 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

      |
84 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
         |
85 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
      |
86 | 84, 85 | eqeltrrd 2541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
87 | 86 | adantll 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
     |
88 | 87 | 3adant2 1033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

         |
89 | 55 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  

  |
90 | 48 | eleq2i 2532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
        |
91 | | eldif 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  |
92 | 90, 91 | sylbb 202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
     
     |
93 | 92 | simpld 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
       |
94 | | opelxp 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          |
95 | 93, 94 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
    |
96 | 95 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  


   |
97 | 96 | simpld 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  

  |
98 | 89, 97 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  

  |
99 | 96 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  

  |
100 | 89, 99 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  

  |
101 | 92 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
    |
102 | | df-br 4417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  
 |
103 | 101, 102 | sylnibr 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
  |
104 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
105 | 104 | ideq 5006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
106 | 103, 105 | sylnib 310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  |
107 | 106 | neqned 2642 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
  |
108 | 107 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  

  |
109 | 98, 100, 108 | subne0d 10021 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  

    |
110 | 83, 88, 109 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . 23
    

        |
111 | 82, 110 | syl5eqner 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
    

           |
112 | 81, 111 | eqnetrd 2703 |
. . . . . . . . . . . . . . . . . . . . 21
    

        |
113 | 112 | 3exp 1214 |
. . . . . . . . . . . . . . . . . . . 20
 
              |
114 | 113 | rexlimdvv 2897 |
. . . . . . . . . . . . . . . . . . 19
 
  
         |
115 | 79, 114 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
 
     |
116 | | absgt0 13436 |
. . . . . . . . . . . . . . . . . . 19
               |
117 | 75, 116 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
             |
118 | 115, 117 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
 
         |
119 | 73 | eqcomd 2468 |
. . . . . . . . . . . . . . . . 17
 
               |
120 | 118, 119 | breqtrd 4441 |
. . . . . . . . . . . . . . . 16
 
         |
121 | 77, 120 | elrpd 11367 |
. . . . . . . . . . . . . . 15
 
         |
122 | 121 | ralrimiva 2814 |
. . . . . . . . . . . . . 14
          |
123 | | fnfvrnss 6074 |
. . . . . . . . . . . . . 14
    
      
    |
124 | 61, 122, 123 | syl2anc 671 |
. . . . . . . . . . . . 13
     |
125 | 34, 124 | syl5eqss 3488 |
. . . . . . . . . . . 12

  |
126 | | ltso 9740 |
. . . . . . . . . . . . . . 15
 |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . 14
   |
128 | | cnvso 5394 |
. . . . . . . . . . . . . 14
  |
129 | 127, 128 | sylib 201 |
. . . . . . . . . . . . 13
   |
130 | | fourierdlem42OLD.af |
. . . . . . . . . . . . . . . . . . 19
   |
131 | | xpfi 7868 |
. . . . . . . . . . . . . . . . . . 19
 
     |
132 | 130, 130,
131 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
     |
133 | | diffi 7829 |
. . . . . . . . . . . . . . . . . 18
     
  |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
  |
135 | 48, 134 | syl5eqel 2544 |
. . . . . . . . . . . . . . . 16
   |
136 | | fnfi 7875 |
. . . . . . . . . . . . . . . 16
         |
137 | 61, 135, 136 | syl2anc 671 |
. . . . . . . . . . . . . . 15
     |
138 | | rnfi 7883 |
. . . . . . . . . . . . . . 15
 

    |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . 14
     |
140 | 34, 139 | syl5eqel 2544 |
. . . . . . . . . . . . 13
   |
141 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
     |
142 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
  |
143 | 142 | reseq1d 5123 |
. . . . . . . . . . . . . . . . . 18
    
   |
144 | 143 | fveq1d 5890 |
. . . . . . . . . . . . . . . . 17
                      |
145 | | fourierdlem42OLD.ba |
. . . . . . . . . . . . . . . . . . . . 21
   |
146 | | fourierdlem42OLD.ca |
. . . . . . . . . . . . . . . . . . . . 21
   |
147 | | opelxp 4883 |
. . . . . . . . . . . . . . . . . . . . 21
  
       |
148 | 145, 146,
147 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . . . 20
        |
149 | | fourierdlem42OLD.bc |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
150 | 50, 149 | ltned 9797 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
151 | 150 | neneqd 2640 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
152 | | ideqg 5005 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
153 | 146, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
154 | 151, 153 | mtbird 307 |
. . . . . . . . . . . . . . . . . . . . 21
   |
155 | | df-br 4417 |
. . . . . . . . . . . . . . . . . . . . 21

    |
156 | 154, 155 | sylnib 310 |
. . . . . . . . . . . . . . . . . . . 20
     |
157 | 148, 156 | eldifd 3427 |
. . . . . . . . . . . . . . . . . . 19
         |
158 | 157, 48 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . 18
      |
159 | | fvres 5902 |
. . . . . . . . . . . . . . . . . 18
  

  
        
        |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
                 |
161 | 50 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . 21
   |
162 | 51 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . 21
   |
163 | | opelxp 4883 |
. . . . . . . . . . . . . . . . . . . . 21
  
       |
164 | 161, 162,
163 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . . . 20
        |
165 | 164, 69 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . . 19
   
 |
166 | | fvco 5964 |
. . . . . . . . . . . . . . . . . . 19
    
                   |
167 | 67, 165, 166 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
                    |
168 | | df-ov 6318 |
. . . . . . . . . . . . . . . . . . . . 21
        |
169 | 168 | eqcomi 2471 |
. . . . . . . . . . . . . . . . . . . 20
        |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
          |
171 | 170 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
                  |
172 | 167, 171 | eqtrd 2496 |
. . . . . . . . . . . . . . . . 17
            
    |
173 | 144, 160,
172 | 3eqtrrd 2501 |
. . . . . . . . . . . . . . . 16
    
   
         |
174 | | fnfvelrn 6042 |
. . . . . . . . . . . . . . . . 17
       
             |
175 | 61, 158, 174 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
              |
176 | 173, 175 | eqeltrd 2540 |
. . . . . . . . . . . . . . 15
    
      |
177 | | ne0i 3749 |
. . . . . . . . . . . . . . 15
         
   |
178 | 176, 177 | syl 17 |
. . . . . . . . . . . . . 14
     |
179 | 141, 178 | eqnetrd 2703 |
. . . . . . . . . . . . 13
   |
180 | | resss 5147 |
. . . . . . . . . . . . . . . . 17
   |
181 | | rnss 5082 |
. . . . . . . . . . . . . . . . 17
 

    |
182 | 180, 181 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
   |
183 | 45 | rneqi 5080 |
. . . . . . . . . . . . . . . . 17
  |
184 | | rncoss 5114 |
. . . . . . . . . . . . . . . . . 18
  |
185 | | frn 5758 |
. . . . . . . . . . . . . . . . . . 19
       |
186 | 35, 185 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 |
187 | 184, 186 | sstri 3453 |
. . . . . . . . . . . . . . . . 17
  |
188 | 183, 187 | eqsstri 3474 |
. . . . . . . . . . . . . . . 16
 |
189 | 182, 188 | sstri 3453 |
. . . . . . . . . . . . . . 15
   |
190 | 34, 189 | eqsstri 3474 |
. . . . . . . . . . . . . 14
 |
191 | 190 | a1i 11 |
. . . . . . . . . . . . 13

  |
192 | | fisupcl 8011 |
. . . . . . . . . . . . 13
  
     
  |
193 | 129, 140,
179, 191, 192 | syl13anc 1278 |
. . . . . . . . . . . 12
    
  |
194 | 125, 193 | sseldd 3445 |
. . . . . . . . . . 11
    
  |
195 | 33, 194 | syl5eqel 2544 |
. . . . . . . . . 10
   |
196 | 195 | ad2antrr 737 |
. . . . . . . . 9
    
        
  |
197 | 3, 30, 32, 196 | lptre2pt 37758 |
. . . . . . . 8
    
         

          |
198 | | simpll 765 |
. . . . . . . . . . . . . 14
   
 
   |
199 | 29 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
 
   |
200 | 199 | adantrr 728 |
. . . . . . . . . . . . . . . 16
 

    |
201 | 200 | adantr 471 |
. . . . . . . . . . . . . . 15
   
 
   |
202 | 29 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
 
   |
203 | 202 | adantrl 727 |
. . . . . . . . . . . . . . . 16
 

    |
204 | 203 | adantr 471 |
. . . . . . . . . . . . . . 15
   
 
   |
205 | | simpr 467 |
. . . . . . . . . . . . . . 15
   
 
   |
206 | 201, 204,
205 | 3jca 1194 |
. . . . . . . . . . . . . 14
   
 
 
   |
207 | 8 | eleq2i 2532 |
. . . . . . . . . . . . . . . . . . 19

   ![[,] [,]](_icc.gif)   
      |
208 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
209 | 208 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
210 | 209 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . . 21
  

  
        |
211 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
212 | 211 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
213 | 212 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
214 | 213 | cbvrexv 3032 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
215 | 210, 214 | syl6bb 269 |
. . . . . . . . . . . . . . . . . . . 20
  

  
        |
216 | 215 | elrab 3208 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          |
217 | 207, 216 | sylbb 202 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)          |
218 | 217 | simprd 469 |
. . . . . . . . . . . . . . . . 17
        |
219 | 218 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
        |
220 | 8 | eleq2i 2532 |
. . . . . . . . . . . . . . . . . . 19

   ![[,] [,]](_icc.gif)   
      |
221 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
222 | 221 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
223 | 222 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . 20
  

  
        |
224 | 223 | elrab 3208 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          |
225 | 220, 224 | sylbb 202 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)          |
226 | 225 | simprd 469 |
. . . . . . . . . . . . . . . . 17
        |
227 | 226 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
        |
228 | | reeanv 2970 |
. . . . . . . . . . . . . . . 16
  
                        |
229 | 219, 227,
228 | sylanbrc 675 |
. . . . . . . . . . . . . . 15
 
               |
230 | 229 | ad2antlr 738 |
. . . . . . . . . . . . . 14
   
 
               |
231 | | simplll 773 |
. . . . . . . . . . . . . . . 16
                       |
232 | | simpl1 1017 |
. . . . . . . . . . . . . . . . . . 19
       |
233 | | simpl2 1018 |
. . . . . . . . . . . . . . . . . . 19
       |
234 | | simpr 467 |
. . . . . . . . . . . . . . . . . . 19
    
  |
235 | 232, 233,
234 | 3jca 1194 |
. . . . . . . . . . . . . . . . . 18
         |
236 | 235 | adantll 725 |
. . . . . . . . . . . . . . . . 17
   
       |
237 | 236 | adantlr 726 |
. . . . . . . . . . . . . . . 16
                         |
238 | | simplr 767 |
. . . . . . . . . . . . . . . 16
                     
             |
239 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
240 | | breq2 4420 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
241 | 239, 240 | 3anbi23d 1351 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
242 | 241 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . 19
  

 
       |
243 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
244 | 243 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
245 | 244 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . 20
                         |
246 | 245 | 2rexbidv 2920 |
. . . . . . . . . . . . . . . . . . 19
  
           
              |
247 | 242, 246 | anbi12d 722 |
. . . . . . . . . . . . . . . . . 18
                   
      
              |
248 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . 20
       |
249 | 248 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . 19
               |
250 | 249 | breq2d 4428 |
. . . . . . . . . . . . . . . . . 18
       
         |
251 | 247, 250 | imbi12d 326 |
. . . . . . . . . . . . . . . . 17
                           
  

   
          
          |
252 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
253 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
254 | 252, 253 | 3anbi13d 1350 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
255 | 254 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . 20
  

 
       |
256 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
257 | 256 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
258 | 257 | anbi1d 716 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
259 | 258 | 2rexbidv 2920 |
. . . . . . . . . . . . . . . . . . . 20
  
           
              |
260 | 255, 259 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . 19
                   
      
              |
261 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . 21
       |
262 | 261 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . 20
               |
263 | 262 | breq2d 4428 |
. . . . . . . . . . . . . . . . . . 19
       
         |
264 | 260, 263 | imbi12d 326 |
. . . . . . . . . . . . . . . . . 18
                           
  

   
          
          |
265 | | fourierdlem42OLD.15 |
. . . . . . . . . . . . . . . . . . 19
   
   
             |
266 | 265 | simprbi 470 |
. . . . . . . . . . . . . . . . . . . 20
               |
267 | 265 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     |
268 | 267 | simpld 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
    |
269 | 268 | simpld 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
270 | 269, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
271 | 270 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
272 | 269, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
273 | 272 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
274 | 269, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  ![[,] [,]](_icc.gif)    |
275 | 274 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             ![[,] [,]](_icc.gif)    |
276 | 275 | adantrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   ![[,] [,]](_icc.gif)    |
277 | 274 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             ![[,] [,]](_icc.gif)    |
278 | 277 | adantrr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   ![[,] [,]](_icc.gif)    |
279 | 271, 273,
276, 278 | iccsuble 37658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                       
   |
280 | | fourierdlem42OLD.t |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
281 | 279, 280 | syl6breqr 4457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                         |
282 | 281 | 3adant2 1033 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
            |
283 | 282 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                         |
284 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   |
285 | | zre 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
286 | 285 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
287 | 286 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   |
288 | | zre 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
289 | 288 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
290 | 289 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   |
291 | 287, 290 | ltnled 9808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
 
   |
292 | 284, 291 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   |
293 | 51, 50 | resubcld 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
294 | 280, 293 | syl5eqel 2544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
295 | 269, 294 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
296 | 295 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

  |
297 | 289 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
298 | 286 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
299 | 297, 298 | resubcld 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
300 | 295 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
  |
301 | 299, 300 | remulcld 9697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
302 | 301 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

      |
303 | 268 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
304 | 303 | simp2d 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
305 | 304 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
306 | 288 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
307 | 295 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
308 | 306, 307 | remulcld 9697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
309 | 308 | adantrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
310 | 305, 309 | readdcld 9696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
311 | 303 | simp1d 1026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
312 | 311 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
313 | 285 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
314 | 295 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
315 | 313, 314 | remulcld 9697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
316 | 315 | adantrr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
317 | 312, 316 | readdcld 9696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
318 | 310, 317 | resubcld 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 |
319 | 318 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

            |
320 | 295 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
321 | 320 | mulid2d 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
322 | 321 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

    |
323 | 322 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 

    |
324 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 

  |
325 | | zltlem1 11018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
       |
326 | 325 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 

      |
327 | 324, 326 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

    |
328 | 286 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
  |
329 | | peano2rem 9967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
330 | 297, 329 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
331 | 330 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
    |
332 | | 1re 9668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
333 | | resubcl 9964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
     |
334 | 332, 328,
333 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
    |
335 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
    |
336 | 328, 331,
334, 335 | leadd1dd 10255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
  
            |
337 | | zcn 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
338 | 337 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
339 | | 1cnd 9685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
340 | 338, 339 | pncan3d 10015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
       |
341 | 340 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
  
      |
342 | | zcn 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
343 | 342 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
344 | 343, 339,
338 | npncand 10036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
           |
345 | 344 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
  
          |
346 | 336, 341,
345 | 3brtr3d 4446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 
  
    |
347 | 327, 346 | syldan 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 

    |
348 | 332 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

  |
349 | 299 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

    |
350 | 50, 51 | posdifd 10228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       |
351 | 149, 350 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
352 | 351, 280 | syl6breqr 4457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   |
353 | 294, 352 | elrpd 11367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
354 | 269, 353 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
355 | 354 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

  |
356 | 348, 349,
355 | lemul1d 11410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 

  
         |
357 | 347, 356 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 

        |
358 | 323, 357 | eqbrtrd 4437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

      |
359 | 304, 311 | resubcld 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
360 | 303 | simp3d 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

  |
361 | 311, 304 | posdifd 10228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
362 | 360, 361 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

    |
363 | 359, 362 | elrpd 11367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
364 | 363 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
365 | 301, 364 | ltaddrp2d 11401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
          |
366 | 304 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
367 | 366 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
368 | 308 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
369 | 368 | adantrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
370 | 311 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
371 | 370 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
372 | 315 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
373 | 372 | adantrr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
374 | 367, 369,
371, 373 | addsub4d 10059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                           |
375 | 342 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
376 | 337 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
377 | 320 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
  |
378 | 375, 376,
377 | subdird 10103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
379 | 378 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 |
380 | 379 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                         |
381 | 374, 380 | eqtr2d 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                         |
382 | 365, 381 | breqtrd 4441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        
            |
383 | 382 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

                |
384 | 296, 302,
319, 358, 383 | lelttrd 9819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 

            |
385 | 296, 319 | ltnled 9808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 

          
             |
386 | 384, 385 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 

            |
387 | 292, 386 | syldan 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
          
  |
388 | 387 | 3adantl3 1172 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                      
  |
389 | 283, 388 | condan 808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
  |
390 | 190, 193 | sseldi 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
  |
391 | 33, 390 | syl5eqel 2544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
392 | 269, 391 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
393 | 392 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
  |
394 | 393 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                             |
395 | 295 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
  |
396 | 395 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                             |
397 | 286, 289 | resubcld 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     |
398 | 397 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
399 | 398, 300 | remulcld 9697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
400 | 399 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
      |
401 | 400 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                 |
402 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
403 | 145, 146 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   |
404 | 402, 403,
149 | 3jca 1194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  

   |
405 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
   |
406 | 405 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
  
      |
407 | | breq2 4420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   |
408 | 406, 407 | 3anbi23d 1351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  


 


    |
409 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
410 | 409 | breq2d 4428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   
     |
411 | 408, 410 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    


     


      |
412 | | simp2l 1040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 

    |
413 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
   |
414 | 413 | anbi1d 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
  
      |
415 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
416 | 414, 415 | 3anbi23d 1351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
  


 


    |
417 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       |
418 | 417 | breq2d 4428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   
     |
419 | 416, 418 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    


     


      |
420 | 190 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 

    |
421 | | 0re 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 |
422 | 34 | eleq2i 2532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47

    |
423 | 422 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
     |
424 | 423 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
     |
425 | 61 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 
     |
426 | | fvelrnb 5935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

  

         |
427 | 425, 426 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
   

         |
428 | 424, 427 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
 
        |
429 | 121 | rpge0d 11374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 
         |
430 | 429 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 
               |
431 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 
               |
432 | 430, 431 | breqtrd 4441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
         |
433 | 432 | 3exp 1214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
        
    |
434 | 433 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
        
    |
435 | 434 | rexlimdv 2889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
  
     
   |
436 | 428, 435 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
   |
437 | 436 | ralrimiva 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
  |
438 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
   |
439 | 438 | ralbidv 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
  

   |
440 | 439 | rspcev 3162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
    
   |
441 | 421, 437,
440 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     |
442 | 441 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 

      |
443 | | pm3.22 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
 
   |
444 | | opelxp 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
          |
445 | 443, 444 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 
        |
446 | 445 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

         |
447 | 49, 52 | sstrd 3454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51

  |
448 | 447 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 
   |
449 | 448 | adantrr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

    |
450 | 449 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

    |
451 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

    |
452 | 450, 451 | gtned 9796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

    |
453 | 452 | neneqd 2640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

 
  |
454 | | df-br 4417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47

  
 |
455 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 |
456 | 455 | ideq 5006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47

  |
457 | 454, 456 | bitr3i 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
      |
458 | 453, 457 | sylnibr 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

      |
459 | 446, 458 | eldifd 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

       
  |
460 | 459, 48 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

       |
461 | 450, 451 | ltned 9797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

    |
462 | 143 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

     
   |
463 | 462 | fveq1d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

          
  
         |
464 | 445 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

         |
465 | | necom 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53

  |
466 | 465 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
   |
467 | 466 | neneqd 2640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51

  |
468 | 467 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 

 
  |
469 | 468, 457 | sylnibr 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

      |
470 | 464, 469 | eldifd 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

       
  |
471 | 470, 48 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

       |
472 | | fvres 5902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
   
                    |
473 | 471, 472 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

    
      
 
        |
474 | | simp1 1014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 

    |
475 | 474, 471 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

         |
476 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
           |
477 | 476 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
       
       |
478 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
    
     |
479 | 477, 478 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
      

            |
480 | 479, 70 | vtoclg 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
   
 
  

  
  |
481 | 471, 475,
480 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

      |
482 | | fvco 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
    
          
        |
483 | 67, 481, 482 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

   
     
           |
484 | | df-ov 6318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
        |
485 | 484 | eqcomi 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
        |
486 | 485 | fveq2i 5891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
  
             |
487 | 483, 486 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

   
     
        |
488 | 463, 473,
487 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

          
        |
489 | 461, 488 | syld3an3 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

          
        |
490 | 447 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
   |
491 | 490 | adantrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

    |
492 | 491 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

    |
493 | 450, 492,
451 | ltled 9809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

    |
494 | 450, 492,
493 | abssubge0d 13542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

            |
495 | 489, 494 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

          
    |
496 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
           
         |
497 | 496 | eqeq1d 2464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
      
                    |
498 | 497 | rspcev 3162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    
        
  

          |
499 | 460, 495,
498 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 

  
          |
500 | 491, 449 | resubcld 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

      |
501 | | elex 3066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
       |
502 | 500, 501 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

      |
503 | 502 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

      |
504 | | simp1 1014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

    |
505 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
     
       |
506 | | eqeq2 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
         
           |
507 | 506 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
    
     

           |
508 | 505, 507 | bibi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
     
 
          
 
            |
509 | 508 | imbi2d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
    
  

       
    
 
             |
510 | 61, 426 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
  
 
         |
511 | 509, 510 | vtoclg 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
        

            |
512 | 503, 504,
511 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 

      

           |
513 | 499, 512 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 

        |
514 | 513, 34 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 

      |
515 | | infmrlbOLD 10625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 


  
  
     |
516 | 420, 442,
514, 515 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 

          |
517 | 33, 516 | syl5eqbr 4450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 

      |
518 | 419, 517 | vtoclg 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  


      |
519 | 412, 518 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 

      |
520 | 411, 519 | vtoclg 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  


 
    |
521 | 146, 404,
520 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

    |
522 | 521, 280 | syl6breqr 4457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
523 | 269, 522 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
524 | 523 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
  |
525 | 524 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                             |
526 | 366 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     |
527 | 526, 368 | pncan2d 10014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
             |
528 | 527 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                 |
529 | 342 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
530 | 320 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
531 | 421 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   |
532 | 531, 352 | gtned 9796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
533 | 269, 532 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
534 | 533 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
535 | 529, 530,
534 | divcan4d 10417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         |
536 | 528, 535 | eqtr2d 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
             |
537 | 536 | adantrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               |
538 | 537 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
 
                   |
539 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                       |
540 | 539 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             |