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

↾t   ![[,] [,]](_icc.gif)    |
5 | 3, 4 | icccmp 21836 |
. . . . 5
 
   |
6 | 1, 2, 5 | syl2anc 666 |
. . . 4
   |
7 | 6 | adantr 467 |
. . 3
 
   |
8 | | fourierdlem42.h |
. . . . . 6
   ![[,] [,]](_icc.gif)         |
9 | | ssrab2 3513 |
. . . . . . 7
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)   |
10 | 9 | a1i 11 |
. . . . . 6
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
11 | 8, 10 | syl5eqss 3475 |
. . . . 5

  ![[,] [,]](_icc.gif)    |
12 | | retop 21775 |
. . . . . . . 8
     |
13 | 3, 12 | eqeltri 2524 |
. . . . . . 7
 |
14 | 1, 2 | iccssred 37596 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
  |
15 | | uniretop 21776 |
. . . . . . . . 9
      |
16 | 3 | unieqi 4206 |
. . . . . . . . 9
       |
17 | 15, 16 | eqtr4i 2475 |
. . . . . . . 8
  |
18 | 17 | restuni 20171 |
. . . . . . 7
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ↾t   ![[,] [,]](_icc.gif)     |
19 | 13, 14, 18 | sylancr 668 |
. . . . . 6
   ![[,] [,]](_icc.gif)    ↾t   ![[,] [,]](_icc.gif)     |
20 | 4 | unieqi 4206 |
. . . . . . 7
   ↾t   ![[,] [,]](_icc.gif)    |
21 | 20 | eqcomi 2459 |
. . . . . 6
  ↾t   ![[,] [,]](_icc.gif)     |
22 | 19, 21 | syl6eq 2500 |
. . . . 5
   ![[,] [,]](_icc.gif)     |
23 | 11, 22 | sseqtrd 3467 |
. . . 4

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

  |
26 | | eqid 2450 |
. . . 4
   |
27 | 26 | bwth 20418 |
. . 3
  
   
          |
28 | 7, 24, 25, 27 | syl3anc 1267 |
. 2
 
              |
29 | 11, 14 | sstrd 3441 |
. . . . . . . . . 10

  |
30 | 29 | ad2antrr 731 |
. . . . . . . . 9
    
           |
31 | | ne0i 3736 |
. . . . . . . . . 10
        
          |
32 | 31 | adantl 468 |
. . . . . . . . 9
    
                   |
33 | | fourierdlem42.e |
. . . . . . . . . . 11
inf    |
34 | | fourierdlem42.r |
. . . . . . . . . . . . 13
   |
35 | | absf 13393 |
. . . . . . . . . . . . . . . . . 18
     |
36 | | ffn 5726 |
. . . . . . . . . . . . . . . . . 18
       |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
38 | | subf 9874 |
. . . . . . . . . . . . . . . . . 18
      |
39 | | ffn 5726 |
. . . . . . . . . . . . . . . . . 18
     
   |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17

  |
41 | | frn 5733 |
. . . . . . . . . . . . . . . . . 18
       |
42 | 38, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
43 | | fnco 5682 |
. . . . . . . . . . . . . . . . 17
   
      |
44 | 37, 40, 42, 43 | mp3an 1363 |
. . . . . . . . . . . . . . . 16


  |
45 | | fourierdlem42.d |
. . . . . . . . . . . . . . . . 17
  |
46 | 45 | fneq1i 5668 |
. . . . . . . . . . . . . . . 16
  

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

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

  ![[,] [,]](_icc.gif)    |
50 | | fourierdlem42.b |
. . . . . . . . . . . . . . . . . . . . 21
   |
51 | | fourierdlem42.c |
. . . . . . . . . . . . . . . . . . . . 21
   |
52 | 50, 51 | iccssred 37596 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif) 
  |
53 | | ax-resscn 9593 |
. . . . . . . . . . . . . . . . . . . 20
 |
54 | 52, 53 | syl6ss 3443 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif) 
  |
55 | 49, 54 | sstrd 3441 |
. . . . . . . . . . . . . . . . . 18

  |
56 | | xpss12 4939 |
. . . . . . . . . . . . . . . . . 18
 
   
   |
57 | 55, 55, 56 | syl2anc 666 |
. . . . . . . . . . . . . . . . 17
  
    |
58 | 57 | ssdifssd 3570 |
. . . . . . . . . . . . . . . 16
        |
59 | 48, 58 | syl5eqss 3475 |
. . . . . . . . . . . . . . 15

    |
60 | | fnssres 5687 |
. . . . . . . . . . . . . . 15
           |
61 | 47, 59, 60 | sylancr 668 |
. . . . . . . . . . . . . 14
     |
62 | | fvres 5877 |
. . . . . . . . . . . . . . . . . . 19
             |
63 | 62 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
             |
64 | 45 | fveq1i 5864 |
. . . . . . . . . . . . . . . . . . 19
          |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
      
     |
66 | | ffun 5729 |
. . . . . . . . . . . . . . . . . . . 20
      |
67 | 38, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 |
68 | 59 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
69 | 38 | fdmi 5732 |
. . . . . . . . . . . . . . . . . . . 20
   |
70 | 68, 69 | syl6eleqr 2539 |
. . . . . . . . . . . . . . . . . . 19
 
  |
71 | | fvco 5939 |
. . . . . . . . . . . . . . . . . . 19
         
     |
72 | 67, 70, 71 | sylancr 668 |
. . . . . . . . . . . . . . . . . 18
 
  
           |
73 | 63, 65, 72 | 3eqtrd 2488 |
. . . . . . . . . . . . . . . . 17
 
               |
74 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
        |
75 | 74, 68 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . 18
 
     |
76 | 75 | abscld 13491 |
. . . . . . . . . . . . . . . . 17
 
         |
77 | 73, 76 | eqeltrd 2528 |
. . . . . . . . . . . . . . . 16
 
         |
78 | | elxp2 4851 |
. . . . . . . . . . . . . . . . . . . 20
  
       |
79 | 68, 78 | sylib 200 |
. . . . . . . . . . . . . . . . . . 19
 
        |
80 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
81 | 80 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . 22
    

             |
82 | | df-ov 6291 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
83 | | simp1l 1031 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

      |
84 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
         |
85 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
      |
86 | 84, 85 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
87 | 86 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
     |
88 | 87 | 3adant2 1026 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

         |
89 | 55 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  

  |
90 | 48 | eleq2i 2520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
        |
91 | | eldif 3413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  |
92 | 90, 91 | sylbb 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
     
     |
93 | 92 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
       |
94 | | opelxp 4863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          |
95 | 93, 94 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
    |
96 | 95 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  


   |
97 | 96 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  

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

  |
99 | 96 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  

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

  |
101 | 92 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
    |
102 | | df-br 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  
 |
103 | 101, 102 | sylnibr 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
  |
104 | | vex 3047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
105 | 104 | ideq 4986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
106 | 103, 105 | sylnib 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  |
107 | 106 | neqned 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
  |
108 | 107 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  

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

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

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

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

        |
113 | 112 | 3exp 1206 |
. . . . . . . . . . . . . . . . . . . 20
 
              |
114 | 113 | rexlimdvv 2884 |
. . . . . . . . . . . . . . . . . . 19
 
  
         |
115 | 79, 114 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
 
     |
116 | | absgt0 13380 |
. . . . . . . . . . . . . . . . . . 19
               |
117 | 75, 116 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
             |
118 | 115, 117 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
 
         |
119 | 73 | eqcomd 2456 |
. . . . . . . . . . . . . . . . 17
 
               |
120 | 118, 119 | breqtrd 4426 |
. . . . . . . . . . . . . . . 16
 
         |
121 | 77, 120 | elrpd 11335 |
. . . . . . . . . . . . . . 15
 
         |
122 | 121 | ralrimiva 2801 |
. . . . . . . . . . . . . 14
          |
123 | | fnfvrnss 6049 |
. . . . . . . . . . . . . 14
    
      
    |
124 | 61, 122, 123 | syl2anc 666 |
. . . . . . . . . . . . 13
     |
125 | 34, 124 | syl5eqss 3475 |
. . . . . . . . . . . 12

  |
126 | | ltso 9711 |
. . . . . . . . . . . . . 14
 |
127 | 126 | a1i 11 |
. . . . . . . . . . . . 13
   |
128 | | fourierdlem42.af |
. . . . . . . . . . . . . . . . . . 19
   |
129 | | xpfi 7839 |
. . . . . . . . . . . . . . . . . . 19
 
     |
130 | 128, 128,
129 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
     |
131 | | diffi 7800 |
. . . . . . . . . . . . . . . . . 18
     
  |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
  |
133 | 48, 132 | syl5eqel 2532 |
. . . . . . . . . . . . . . . 16
   |
134 | | fnfi 7846 |
. . . . . . . . . . . . . . . 16
         |
135 | 61, 133, 134 | syl2anc 666 |
. . . . . . . . . . . . . . 15
     |
136 | | rnfi 7854 |
. . . . . . . . . . . . . . 15
 

    |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . 14
     |
138 | 34, 137 | syl5eqel 2532 |
. . . . . . . . . . . . 13
   |
139 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
     |
140 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
  |
141 | 140 | reseq1d 5103 |
. . . . . . . . . . . . . . . . . 18
    
   |
142 | 141 | fveq1d 5865 |
. . . . . . . . . . . . . . . . 17
                      |
143 | | fourierdlem42.ba |
. . . . . . . . . . . . . . . . . . . . 21
   |
144 | | fourierdlem42.ca |
. . . . . . . . . . . . . . . . . . . . 21
   |
145 | | opelxp 4863 |
. . . . . . . . . . . . . . . . . . . . 21
  
       |
146 | 143, 144,
145 | sylanbrc 669 |
. . . . . . . . . . . . . . . . . . . 20
        |
147 | | fourierdlem42.bc |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
148 | 50, 147 | ltned 9768 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
149 | 148 | neneqd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
150 | | ideqg 4985 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
151 | 144, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
152 | 149, 151 | mtbird 303 |
. . . . . . . . . . . . . . . . . . . . 21
   |
153 | | df-br 4402 |
. . . . . . . . . . . . . . . . . . . . 21

    |
154 | 152, 153 | sylnib 306 |
. . . . . . . . . . . . . . . . . . . 20
     |
155 | 146, 154 | eldifd 3414 |
. . . . . . . . . . . . . . . . . . 19
         |
156 | 155, 48 | syl6eleqr 2539 |
. . . . . . . . . . . . . . . . . 18
      |
157 | | fvres 5877 |
. . . . . . . . . . . . . . . . . 18
  

  
        
        |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
                 |
159 | 50 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . 21
   |
160 | 51 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . 21
   |
161 | | opelxp 4863 |
. . . . . . . . . . . . . . . . . . . . 21
  
       |
162 | 159, 160,
161 | sylanbrc 669 |
. . . . . . . . . . . . . . . . . . . 20
        |
163 | 162, 69 | syl6eleqr 2539 |
. . . . . . . . . . . . . . . . . . 19
   
 |
164 | | fvco 5939 |
. . . . . . . . . . . . . . . . . . 19
    
                   |
165 | 67, 163, 164 | sylancr 668 |
. . . . . . . . . . . . . . . . . 18
                    |
166 | | df-ov 6291 |
. . . . . . . . . . . . . . . . . . . . 21
        |
167 | 166 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . . 20
        |
168 | 167 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
          |
169 | 168 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
                  |
170 | 165, 169 | eqtrd 2484 |
. . . . . . . . . . . . . . . . 17
            
    |
171 | 142, 158,
170 | 3eqtrrd 2489 |
. . . . . . . . . . . . . . . 16
    
   
         |
172 | | fnfvelrn 6017 |
. . . . . . . . . . . . . . . . 17
       
             |
173 | 61, 156, 172 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
              |
174 | 171, 173 | eqeltrd 2528 |
. . . . . . . . . . . . . . 15
    
      |
175 | | ne0i 3736 |
. . . . . . . . . . . . . . 15
         
   |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . 14
     |
177 | 139, 176 | eqnetrd 2690 |
. . . . . . . . . . . . 13
   |
178 | | resss 5127 |
. . . . . . . . . . . . . . . . 17
   |
179 | | rnss 5062 |
. . . . . . . . . . . . . . . . 17
 

    |
180 | 178, 179 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
   |
181 | 45 | rneqi 5060 |
. . . . . . . . . . . . . . . . 17
  |
182 | | rncoss 5094 |
. . . . . . . . . . . . . . . . . 18
  |
183 | | frn 5733 |
. . . . . . . . . . . . . . . . . . 19
       |
184 | 35, 183 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 |
185 | 182, 184 | sstri 3440 |
. . . . . . . . . . . . . . . . 17
  |
186 | 181, 185 | eqsstri 3461 |
. . . . . . . . . . . . . . . 16
 |
187 | 180, 186 | sstri 3440 |
. . . . . . . . . . . . . . 15
   |
188 | 34, 187 | eqsstri 3461 |
. . . . . . . . . . . . . 14
 |
189 | 188 | a1i 11 |
. . . . . . . . . . . . 13

  |
190 | | fiinfcl 8014 |
. . . . . . . . . . . . 13
 
  inf     |
191 | 127, 138,
177, 189, 190 | syl13anc 1269 |
. . . . . . . . . . . 12
 inf     |
192 | 125, 191 | sseldd 3432 |
. . . . . . . . . . 11
 inf     |
193 | 33, 192 | syl5eqel 2532 |
. . . . . . . . . 10
   |
194 | 193 | ad2antrr 731 |
. . . . . . . . 9
    
        
  |
195 | 3, 30, 32, 194 | lptre2pt 37714 |
. . . . . . . 8
    
         

          |
196 | | simpll 759 |
. . . . . . . . . . . . . 14
   
 
   |
197 | 29 | sselda 3431 |
. . . . . . . . . . . . . . . . 17
 
   |
198 | 197 | adantrr 722 |
. . . . . . . . . . . . . . . 16
 

    |
199 | 198 | adantr 467 |
. . . . . . . . . . . . . . 15
   
 
   |
200 | 29 | sselda 3431 |
. . . . . . . . . . . . . . . . 17
 
   |
201 | 200 | adantrl 721 |
. . . . . . . . . . . . . . . 16
 

    |
202 | 201 | adantr 467 |
. . . . . . . . . . . . . . 15
   
 
   |
203 | | simpr 463 |
. . . . . . . . . . . . . . 15
   
 
   |
204 | 199, 202,
203 | 3jca 1187 |
. . . . . . . . . . . . . 14
   
 
 
   |
205 | 8 | eleq2i 2520 |
. . . . . . . . . . . . . . . . . . 19

   ![[,] [,]](_icc.gif)   
      |
206 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
207 | 206 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
208 | 207 | rexbidv 2900 |
. . . . . . . . . . . . . . . . . . . . 21
  

  
        |
209 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
210 | 209 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
211 | 210 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
212 | 211 | cbvrexv 3019 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
213 | 208, 212 | syl6bb 265 |
. . . . . . . . . . . . . . . . . . . 20
  

  
        |
214 | 213 | elrab 3195 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          |
215 | 205, 214 | sylbb 201 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)          |
216 | 215 | simprd 465 |
. . . . . . . . . . . . . . . . 17
        |
217 | 216 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
        |
218 | 8 | eleq2i 2520 |
. . . . . . . . . . . . . . . . . . 19

   ![[,] [,]](_icc.gif)   
      |
219 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
220 | 219 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
221 | 220 | rexbidv 2900 |
. . . . . . . . . . . . . . . . . . . 20
  

  
        |
222 | 221 | elrab 3195 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          |
223 | 218, 222 | sylbb 201 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)          |
224 | 223 | simprd 465 |
. . . . . . . . . . . . . . . . 17
        |
225 | 224 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
        |
226 | | reeanv 2957 |
. . . . . . . . . . . . . . . 16
  
                        |
227 | 217, 225,
226 | sylanbrc 669 |
. . . . . . . . . . . . . . 15
 
               |
228 | 227 | ad2antlr 732 |
. . . . . . . . . . . . . 14
   
 
               |
229 | | simplll 767 |
. . . . . . . . . . . . . . . 16
                       |
230 | | simpl1 1010 |
. . . . . . . . . . . . . . . . . . 19
       |
231 | | simpl2 1011 |
. . . . . . . . . . . . . . . . . . 19
       |
232 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
    
  |
233 | 230, 231,
232 | 3jca 1187 |
. . . . . . . . . . . . . . . . . 18
         |
234 | 233 | adantll 719 |
. . . . . . . . . . . . . . . . 17
   
       |
235 | 234 | adantlr 720 |
. . . . . . . . . . . . . . . 16
                         |
236 | | simplr 761 |
. . . . . . . . . . . . . . . 16
                     
             |
237 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
238 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
239 | 237, 238 | 3anbi23d 1341 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
240 | 239 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . 19
  

 
       |
241 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
242 | 241 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
243 | 242 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . 20
                         |
244 | 243 | 2rexbidv 2907 |
. . . . . . . . . . . . . . . . . . 19
  
           
              |
245 | 240, 244 | anbi12d 716 |
. . . . . . . . . . . . . . . . . 18
                   
      
              |
246 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . 20
       |
247 | 246 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . 19
               |
248 | 247 | breq2d 4413 |
. . . . . . . . . . . . . . . . . 18
       
         |
249 | 245, 248 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
                           
  

   
          
          |
250 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
251 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
252 | 250, 251 | 3anbi13d 1340 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
253 | 252 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . 20
  

 
       |
254 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
255 | 254 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
256 | 255 | anbi1d 710 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
257 | 256 | 2rexbidv 2907 |
. . . . . . . . . . . . . . . . . . . 20
  
           
              |
258 | 253, 257 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . 19
                   
      
              |
259 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . 21
       |
260 | 259 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . 20
               |
261 | 260 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . 19
       
         |
262 | 258, 261 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
                           
  

   
          
          |
263 | | fourierdlem42.15 |
. . . . . . . . . . . . . . . . . . 19
   
   
             |
264 | 263 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . 20
               |
265 | 263 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     |
266 | 265 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
    |
267 | 266 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
268 | 267, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
269 | 268 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
270 | 267, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
271 | 270 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
272 | 267, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  ![[,] [,]](_icc.gif)    |
273 | 272 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             ![[,] [,]](_icc.gif)    |
274 | 273 | adantrl 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   ![[,] [,]](_icc.gif)    |
275 | 272 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             ![[,] [,]](_icc.gif)    |
276 | 275 | adantrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   ![[,] [,]](_icc.gif)    |
277 | 269, 271,
274, 276 | iccsuble 37614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                       
   |
278 | | fourierdlem42.t |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
279 | 277, 278 | syl6breqr 4442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                         |
280 | 279 | 3adant2 1026 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
            |
281 | 280 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                         |
282 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   |
283 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
284 | 283 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
285 | 284 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   |
286 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
287 | 286 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
288 | 287 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   |
289 | 285, 288 | ltnled 9779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
 
   |
290 | 282, 289 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   |
291 | 51, 50 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
292 | 278, 291 | syl5eqel 2532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
293 | 267, 292 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
294 | 293 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

  |
295 | 287 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
296 | 284 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
297 | 295, 296 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
298 | 293 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
  |
299 | 297, 298 | remulcld 9668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
300 | 299 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

      |
301 | 266 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
302 | 301 | simp2d 1020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
303 | 302 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
304 | 286 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
305 | 293 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
306 | 304, 305 | remulcld 9668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
307 | 306 | adantrl 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
308 | 303, 307 | readdcld 9667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
309 | 301 | simp1d 1019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
310 | 309 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
311 | 283 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
312 | 293 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
313 | 311, 312 | remulcld 9668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
314 | 313 | adantrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
315 | 310, 314 | readdcld 9667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
316 | 308, 315 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 |
317 | 316 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

            |
318 | 293 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
319 | 318 | mulid2d 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
320 | 319 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

    |
321 | 320 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 

    |
322 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 

  |
323 | | zltlem1 10986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
       |
324 | 323 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 

      |
325 | 322, 324 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

    |
326 | 284 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
  |
327 | | peano2rem 9938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
328 | 295, 327 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
329 | 328 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
    |
330 | | 1re 9639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
331 | | resubcl 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
     |
332 | 330, 326,
331 | sylancr 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
    |
333 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
  
    |
334 | 326, 329,
332, 333 | leadd1dd 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
  
            |
335 | | zcn 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
336 | 335 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
337 | | 1cnd 9656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
338 | 336, 337 | pncan3d 9986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
       |
339 | 338 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
  
      |
340 | | zcn 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
341 | 340 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
342 | 341, 337,
336 | npncand 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
           |
343 | 342 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
  
          |
344 | 334, 339,
343 | 3brtr3d 4431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 
  
    |
345 | 325, 344 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 

    |
346 | 330 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

  |
347 | 297 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

    |
348 | 50, 51 | posdifd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       |
349 | 147, 348 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
350 | 349, 278 | syl6breqr 4442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   |
351 | 292, 350 | elrpd 11335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
352 | 267, 351 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
353 | 352 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 

  |
354 | 346, 347,
353 | lemul1d 11378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 

  
         |
355 | 345, 354 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 

        |
356 | 321, 355 | eqbrtrd 4422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

      |
357 | 302, 309 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
358 | 301 | simp3d 1021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

  |
359 | 309, 302 | posdifd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
360 | 358, 359 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

    |
361 | 357, 360 | elrpd 11335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
362 | 361 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
363 | 299, 362 | ltaddrp2d 11369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
          |
364 | 302 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
365 | 364 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
366 | 306 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
367 | 366 | adantrl 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
368 | 309 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
369 | 368 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
370 | 313 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
371 | 370 | adantrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
372 | 365, 367,
369, 371 | addsub4d 10030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                           |
373 | 340 | ad2antll 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
374 | 335 | ad2antrl 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
375 | 318 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
  |
376 | 373, 374,
375 | subdird 10072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
377 | 376 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 |
378 | 377 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                         |
379 | 372, 378 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                         |
380 | 363, 379 | breqtrd 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        
            |
381 | 380 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 

                |
382 | 294, 300,
317, 356, 381 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 

            |
383 | 294, 317 | ltnled 9779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 

          
             |
384 | 382, 383 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 

            |
385 | 290, 384 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
          
  |
386 | 385 | 3adantl3 1165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                      
  |
387 | 281, 386 | condan 802 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
  |
388 | 188, 191 | sseldi 3429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 inf     |
389 | 33, 388 | syl5eqel 2532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
390 | 267, 389 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
391 | 390 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
  |
392 | 391 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                             |
393 | 293 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
  |
394 | 393 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                             |
395 | 284, 287 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     |
396 | 395 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
397 | 396, 298 | remulcld 9668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
398 | 397 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
      |
399 | 398 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                 |
400 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
401 | 143, 144 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   |
402 | 400, 401,
147 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  

   |
403 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
   |
404 | 403 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
  
      |
405 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   |
406 | 404, 405 | 3anbi23d 1341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  


 


    |
407 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
408 | 407 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   
     |
409 | 406, 408 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    


     


      |
410 | | simp2l 1033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 

    |
411 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
   |
412 | 411 | anbi1d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
  
      |
413 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
414 | 412, 413 | 3anbi23d 1341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
  


 


    |
415 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       |
416 | 415 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   
     |
417 | 414, 416 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    


     


      |
418 | 188 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 

    |
419 | | 0re 9640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 |
420 | 34 | eleq2i 2520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47

    |
421 | 420 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
     |
422 | 421 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
     |
423 | 61 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 
     |
424 | | fvelrnb 5910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

  

         |
425 | 423, 424 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
   

         |
426 | 422, 425 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
 
        |
427 | 121 | rpge0d 11342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 
         |
428 | 427 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 
               |
429 | | simp3 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 
               |
430 | 428, 429 | breqtrd 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
         |
431 | 430 | 3exp 1206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
        
    |
432 | 431 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 
        
    |
433 | 432 | rexlimdv 2876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
  
     
   |
434 | 426, 433 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
   |
435 | 434 | ralrimiva 2801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
  |
436 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
   |
437 | 436 | ralbidv 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
  

   |
438 | 437 | rspcev 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
    
   |
439 | 419, 435,
438 | sylancr 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     |
440 | 439 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 

      |
441 | | pm3.22 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
 
   |
442 | | opelxp 4863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
          |
443 | 441, 442 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 
        |
444 | 443 | 3ad2ant2 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

         |
445 | 49, 52 | sstrd 3441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51

  |
446 | 445 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 
   |
447 | 446 | adantrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

    |
448 | 447 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

    |
449 | | simp3 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

    |
450 | 448, 449 | gtned 9767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

    |
451 | 450 | neneqd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

 
  |
452 | | df-br 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47

  
 |
453 | | vex 3047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 |
454 | 453 | ideq 4986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47

  |
455 | 452, 454 | bitr3i 255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
      |
456 | 451, 455 | sylnibr 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

      |
457 | 444, 456 | eldifd 3414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

       
  |
458 | 457, 48 | syl6eleqr 2539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

       |
459 | 448, 449 | ltned 9768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

    |
460 | 141 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

     
   |
461 | 460 | fveq1d 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

          
  
         |
462 | 443 | 3ad2ant2 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

         |
463 | | necom 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53

  |
464 | 463 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
   |
465 | 464 | neneqd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51

  |
466 | 465 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 

 
  |
467 | 466, 455 | sylnibr 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

      |
468 | 462, 467 | eldifd 3414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

       
  |
469 | 468, 48 | syl6eleqr 2539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

       |
470 | | fvres 5877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
   
                    |
471 | 469, 470 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

    
      
 
        |
472 | | simp1 1007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 

    |
473 | 472, 469 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 

         |
474 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
           |
475 | 474 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
       
       |
476 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
    
     |
477 | 475, 476 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
      

            |
478 | 477, 70 | vtoclg 3106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
   
 
  

  
  |
479 | 469, 473,
478 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
 

      |
480 | | fvco 5939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
    
          
        |
481 | 67, 479, 480 | sylancr 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 

   
     
           |
482 | | df-ov 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
        |
483 | 482 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
        |
484 | 483 | fveq2i 5866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
  
             |
485 | 481, 484 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

   
     
        |
486 | 461, 471,
485 | 3eqtrd 2488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

          
        |
487 | 459, 486 | syld3an3 1312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

          
        |
488 | 445 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 
   |
489 | 488 | adantrl 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 

    |
490 | 489 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

    |
491 | 448, 490,
449 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

    |
492 | 448, 490,
491 | abssubge0d 13486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

            |
493 | 487, 492 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

          
    |
494 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
           
         |
495 | 494 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
      
                    |
496 | 495 | rspcev 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    
        
  

          |
497 | 458, 493,
496 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 

  
          |
498 | 489, 447 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
 

      |
499 | | elex 3053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
       |
500 | 498, 499 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 

      |
501 | 500 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

      |
502 | | simp1 1007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 

    |
503 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
     
       |
504 | | eqeq2 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
         
           |
505 | 504 | rexbidv 2900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
    
     

           |
506 | 503, 505 | bibi12d 323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
     
 
          
 
            |
507 | 506 | imbi2d 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
    
  

       
    
 
             |
508 | 61, 424 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
  
 
         |
509 | 507, 508 | vtoclg 3106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
        

            |
510 | 501, 502,
509 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 

      

           |
511 | 497, 510 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 

        |
512 | 511, 34 | syl6eleqr 2539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 

      |
513 | | infrelb 10593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 


  
inf       |
514 | 418, 440,
512, 513 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 

  inf       |
515 | 33, 514 | syl5eqbr 4435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 

      |
516 | 417, 515 | vtoclg 3106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  


      |
517 | 410, 516 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 

      |
518 | 409, 517 | vtoclg 3106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  


 
    |
519 | 144, 402,
518 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

    |
520 | 519, 278 | syl6breqr 4442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
521 | 267, 520 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
522 | 521 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
  |
523 | 522 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                             |
524 | 364 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     |
525 | 524, 366 | pncan2d 9985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
             |
526 | 525 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                 |
527 | 340 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
528 | 318 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
529 | 419 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   |
530 | 529, 350 | gtned 9767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
531 | 267, 530 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
532 | 531 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
533 | 527, 528,
532 | divcan4d 10386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         |
534 | 526, 533 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
             |
535 | 534 | adantrl 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               |
536 | 535 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
 
                   |
537 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                       |
538 | 537 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                           |
539 | 538 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
 
  |