Step | Hyp | Ref
| Expression |
1 | | fourierdlem93.4 |
. . . . . . . 8
       |
2 | | fourierdlem93.3 |
. . . . . . . . 9
   |
3 | | fourierdlem93.1 |
. . . . . . . . . 10
 
                  
 ..^                |
4 | 3 | fourierdlem2 38083 |
. . . . . . . . 9
 
   
                   
 ..^                 |
5 | 2, 4 | syl 17 |
. . . . . . . 8
                         
 ..^                 |
6 | 1, 5 | mpbid 215 |
. . . . . . 7
                    
 ..^                |
7 | 6 | simprd 470 |
. . . . . 6
             
 ..^               |
8 | 7 | simplld 769 |
. . . . 5
        |
9 | 8 | eqcomd 2477 |
. . . 4
        |
10 | 7 | simplrd 771 |
. . . . 5
       |
11 | 10 | eqcomd 2477 |
. . . 4
       |
12 | 9, 11 | oveq12d 6326 |
. . 3
    ![[,] [,]](_icc.gif) 
      ![[,] [,]](_icc.gif)        |
13 | 12 | itgeq1d 37930 |
. 2
     ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)              |
14 | | 0zd 10973 |
. . 3
   |
15 | | nnuz 11218 |
. . . . 5
     |
16 | 2, 15 | syl6eleq 2559 |
. . . 4
       |
17 | | 1e0p1 11102 |
. . . . . 6
   |
18 | 17 | a1i 11 |
. . . . 5
     |
19 | 18 | fveq2d 5883 |
. . . 4
             |
20 | 16, 19 | eleqtrd 2551 |
. . 3
         |
21 | 3, 2, 1 | fourierdlem15 38096 |
. . . 4
            ![[,] [,]](_icc.gif)    |
22 | | pire 23492 |
. . . . . . 7
 |
23 | 22 | renegcli 9955 |
. . . . . 6
  |
24 | | iccssre 11741 |
. . . . . 6
       ![[,] [,]](_icc.gif)    |
25 | 23, 22, 24 | mp2an 686 |
. . . . 5
   ![[,] [,]](_icc.gif)   |
26 | 25 | a1i 11 |
. . . 4
    ![[,] [,]](_icc.gif) 
  |
27 | 21, 26 | fssd 5750 |
. . 3
           |
28 | 7 | simprd 470 |
. . . 4
   ..^              |
29 | 28 | r19.21bi 2776 |
. . 3
 
 ..^              |
30 | | fourierdlem93.6 |
. . . . 5
      ![[,] [,]](_icc.gif)      |
31 | 30 | adantr 472 |
. . . 4
 
      ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      |
32 | | simpr 468 |
. . . . 5
 
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
33 | 12 | eqcomd 2477 |
. . . . . 6
       ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    |
34 | 33 | adantr 472 |
. . . . 5
 
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    |
35 | 32, 34 | eleqtrd 2551 |
. . . 4
 
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
36 | 31, 35 | ffvelrnd 6038 |
. . 3
 
      ![[,] [,]](_icc.gif)             |
37 | 27 | adantr 472 |
. . . . 5
 
 ..^            |
38 | | elfzofz 11962 |
. . . . . 6
  ..^
      |
39 | 38 | adantl 473 |
. . . . 5
 
 ..^        |
40 | 37, 39 | ffvelrnd 6038 |
. . . 4
 
 ..^        |
41 | | fzofzp1 12037 |
. . . . . 6
  ..^
        |
42 | 41 | adantl 473 |
. . . . 5
 
 ..^          |
43 | 37, 42 | ffvelrnd 6038 |
. . . 4
 
 ..^          |
44 | 30 | feqmptd 5932 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)         |
45 | 44 | adantr 472 |
. . . . . . . . 9
 
 ..^      ![[,] [,]](_icc.gif)         |
46 | 45 | reseq1d 5110 |
. . . . . . . 8
 
 ..^                       ![[,] [,]](_icc.gif)                        |
47 | | ioossicc 11745 |
. . . . . . . . . . 11
                    ![[,] [,]](_icc.gif)         |
48 | 47 | a1i 11 |
. . . . . . . . . 10
 
 ..^                      ![[,] [,]](_icc.gif)          |
49 | 23 | rexri 9711 |
. . . . . . . . . . . . . 14
  |
50 | 49 | a1i 11 |
. . . . . . . . . . . . 13
    ..^        ![[,] [,]](_icc.gif)            |
51 | 22 | rexri 9711 |
. . . . . . . . . . . . . 14
 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
    ..^        ![[,] [,]](_icc.gif)           |
53 | 21 | ad2antrr 740 |
. . . . . . . . . . . . 13
    ..^        ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)    |
54 | | simplr 770 |
. . . . . . . . . . . . 13
    ..^        ![[,] [,]](_icc.gif)          ..^   |
55 | | simpr 468 |
. . . . . . . . . . . . 13
    ..^        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
56 | 50, 52, 53, 54, 55 | fourierdlem1 38082 |
. . . . . . . . . . . 12
    ..^        ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
57 | 56 | ralrimiva 2809 |
. . . . . . . . . . 11
 
 ..^         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
58 | | dfss3 3408 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
59 | 57, 58 | sylibr 217 |
. . . . . . . . . 10
 
 ..^        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
60 | 48, 59 | sstrd 3428 |
. . . . . . . . 9
 
 ..^                   ![[,] [,]](_icc.gif)    |
61 | 60 | resmptd 5162 |
. . . . . . . 8
 
 ..^       ![[,] [,]](_icc.gif)                                            |
62 | 46, 61 | eqtrd 2505 |
. . . . . . 7
 
 ..^                                        |
63 | 62 | eqcomd 2477 |
. . . . . 6
 
 ..^                                        |
64 | | fourierdlem93.7 |
. . . . . 6
 
 ..^                                      |
65 | 63, 64 | eqeltrd 2549 |
. . . . 5
 
 ..^                                          |
66 | | fourierdlem93.9 |
. . . . . 6
 
 ..^                   lim          |
67 | 62 | oveq1d 6323 |
. . . . . 6
 
 ..^                   lim                             lim          |
68 | 66, 67 | eleqtrd 2551 |
. . . . 5
 
 ..^                       lim          |
69 | | fourierdlem93.8 |
. . . . . 6
 
 ..^                   lim        |
70 | 62 | oveq1d 6323 |
. . . . . 6
 
 ..^                   lim                           lim        |
71 | 69, 70 | eleqtrd 2551 |
. . . . 5
 
 ..^                       lim        |
72 | 40, 43, 65, 68, 71 | iblcncfioo 37952 |
. . . 4
 
 ..^                         |
73 | 30 | ad2antrr 740 |
. . . . 5
    ..^        ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)      |
74 | 73, 56 | ffvelrnd 6038 |
. . . 4
    ..^        ![[,] [,]](_icc.gif)               |
75 | 40, 43, 72, 74 | ibliooicc 37945 |
. . 3
 
 ..^         ![[,] [,]](_icc.gif)                |
76 | 14, 20, 27, 29, 36, 75 | itgspltprt 37953 |
. 2
        ![[,] [,]](_icc.gif)              ..^         ![[,] [,]](_icc.gif)                |
77 | | fvres 5893 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)                  |
78 | 77 | eqcomd 2477 |
. . . . . . 7
       ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)              |
79 | 78 | adantl 473 |
. . . . . 6
    ..^        ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)              |
80 | 79 | itgeq2dv 22818 |
. . . . 5
 
 ..^         ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)               |
81 | | eqid 2471 |
. . . . . 6
       ![[,] [,]](_icc.gif)                                   ![[,] [,]](_icc.gif)        
                            ![[,] [,]](_icc.gif)                                   ![[,] [,]](_icc.gif)        
                      |
82 | 30 | adantr 472 |
. . . . . . 7
 
 ..^       ![[,] [,]](_icc.gif)      |
83 | 82, 59 | fssresd 5762 |
. . . . . 6
 
 ..^         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)            |
84 | 48 | resabs1d 5140 |
. . . . . . 7
 
 ..^          ![[,] [,]](_icc.gif)                                          |
85 | 84, 64 | eqeltrd 2549 |
. . . . . 6
 
 ..^          ![[,] [,]](_icc.gif)                                            |
86 | 84 | oveq1d 6323 |
. . . . . . . 8
 
 ..^    
      ![[,] [,]](_icc.gif)                        lim         
               lim          |
87 | 40, 43, 29, 83 | limcicciooub 37814 |
. . . . . . . 8
 
 ..^    
      ![[,] [,]](_icc.gif)                        lim         
      ![[,] [,]](_icc.gif)         lim          |
88 | 86, 87 | eqtr3d 2507 |
. . . . . . 7
 
 ..^                   lim         
      ![[,] [,]](_icc.gif)         lim          |
89 | 66, 88 | eleqtrd 2551 |
. . . . . 6
 
 ..^          ![[,] [,]](_icc.gif)         lim          |
90 | 84 | eqcomd 2477 |
. . . . . . . . 9
 
 ..^                          ![[,] [,]](_icc.gif)        
                 |
91 | 90 | oveq1d 6323 |
. . . . . . . 8
 
 ..^                   lim               ![[,] [,]](_icc.gif)        
               lim        |
92 | 40, 43, 29, 83 | limciccioolb 37798 |
. . . . . . . 8
 
 ..^    
      ![[,] [,]](_icc.gif)                        lim       
      ![[,] [,]](_icc.gif)         lim        |
93 | 91, 92 | eqtrd 2505 |
. . . . . . 7
 
 ..^                   lim       
      ![[,] [,]](_icc.gif)         lim        |
94 | 69, 93 | eleqtrd 2551 |
. . . . . 6
 
 ..^          ![[,] [,]](_icc.gif)         lim        |
95 | | fourierdlem93.5 |
. . . . . . 7
   |
96 | 95 | adantr 472 |
. . . . . 6
 
 ..^    |
97 | 81, 40, 43, 29, 83, 85, 89, 94, 96 | fourierdlem82 38164 |
. . . . 5
 
 ..^         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)           
     |
98 | 40 | adantr 472 |
. . . . . . . 8
    ..^          ![[,] [,]](_icc.gif)                 |
99 | 43 | adantr 472 |
. . . . . . . 8
    ..^          ![[,] [,]](_icc.gif)                   |
100 | 95 | ad2antrr 740 |
. . . . . . . . 9
    ..^          ![[,] [,]](_icc.gif)             |
101 | 98, 100 | resubcld 10068 |
. . . . . . . . . 10
    ..^          ![[,] [,]](_icc.gif)                   |
102 | 99, 100 | resubcld 10068 |
. . . . . . . . . 10
    ..^          ![[,] [,]](_icc.gif)                     |
103 | | simpr 468 |
. . . . . . . . . 10
    ..^          ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)            |
104 | | eliccre 37699 |
. . . . . . . . . 10
               
        ![[,] [,]](_icc.gif)             |
105 | 101, 102,
103, 104 | syl3anc 1292 |
. . . . . . . . 9
    ..^          ![[,] [,]](_icc.gif)             |
106 | 100, 105 | readdcld 9688 |
. . . . . . . 8
    ..^          ![[,] [,]](_icc.gif)           
   |
107 | | elicc2 11724 |
. . . . . . . . . . . 12
                          ![[,] [,]](_icc.gif)                
            |
108 | 101, 102,
107 | syl2anc 673 |
. . . . . . . . . . 11
    ..^          ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)         
      
            |
109 | 103, 108 | mpbid 215 |
. . . . . . . . . 10
    ..^          ![[,] [,]](_icc.gif)                 
           |
110 | 109 | simp2d 1043 |
. . . . . . . . 9
    ..^          ![[,] [,]](_icc.gif)                   |
111 | 98, 100, 105 | lesubadd2d 10233 |
. . . . . . . . 9
    ..^          ![[,] [,]](_icc.gif)                 
    
    |
112 | 110, 111 | mpbid 215 |
. . . . . . . 8
    ..^          ![[,] [,]](_icc.gif)                   |
113 | 109 | simp3d 1044 |
. . . . . . . . 9
    ..^          ![[,] [,]](_icc.gif)                     |
114 | 100, 105,
99 | leaddsub2d 10236 |
. . . . . . . . 9
    ..^          ![[,] [,]](_icc.gif)             
     
           |
115 | 113, 114 | mpbird 240 |
. . . . . . . 8
    ..^          ![[,] [,]](_icc.gif)           
         |
116 | 98, 99, 106, 112, 115 | eliccd 37697 |
. . . . . . 7
    ..^          ![[,] [,]](_icc.gif)           
       ![[,] [,]](_icc.gif)          |
117 | | fvres 5893 |
. . . . . . 7
         ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)                 
    |
118 | 116, 117 | syl 17 |
. . . . . 6
    ..^          ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)                 
    |
119 | 118 | itgeq2dv 22818 |
. . . . 5
 
 ..^           ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)              
     |
120 | 80, 97, 119 | 3eqtrd 2509 |
. . . 4
 
 ..^         ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)              
     |
121 | 120 | sumeq2dv 13846 |
. . 3
   ..^         ![[,] [,]](_icc.gif)                ..^           ![[,] [,]](_icc.gif)              
     |
122 | | oveq2 6316 |
. . . . . . 7
 
     |
123 | 122 | fveq2d 5883 |
. . . . . 6
          
    |
124 | 123 | cbvitgv 22813 |
. . . . 5
      ![[,] [,]](_icc.gif) 
      
         ![[,] [,]](_icc.gif)        
    |
125 | 124 | a1i 11 |
. . . 4
       ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif) 
      
     |
126 | | fourierdlem93.2 |
. . . . . . . . 9
             |
127 | 126 | a1i 11 |
. . . . . . . 8
               |
128 | | fveq2 5879 |
. . . . . . . . . 10
           |
129 | 128 | oveq1d 6323 |
. . . . . . . . 9
               |
130 | 129 | adantl 473 |
. . . . . . . 8
 
               |
131 | 2 | nnzd 11062 |
. . . . . . . . . 10
   |
132 | 14, 131, 14 | 3jca 1210 |
. . . . . . . . 9
 
   |
133 | | 0le0 10721 |
. . . . . . . . . . 11
 |
134 | 133 | a1i 11 |
. . . . . . . . . 10

  |
135 | | 0red 9662 |
. . . . . . . . . . 11
   |
136 | 2 | nnred 10646 |
. . . . . . . . . . 11
   |
137 | 2 | nngt0d 10675 |
. . . . . . . . . . 11
   |
138 | 135, 136,
137 | ltled 9800 |
. . . . . . . . . 10

  |
139 | 134, 138 | jca 541 |
. . . . . . . . 9
 
   |
140 | | elfz2 11817 |
. . . . . . . . 9
    
 
 
    |
141 | 132, 139,
140 | sylanbrc 677 |
. . . . . . . 8
       |
142 | 8, 23 | syl6eqel 2557 |
. . . . . . . . 9
       |
143 | 142, 95 | resubcld 10068 |
. . . . . . . 8
         |
144 | 127, 130,
141, 143 | fvmptd 5969 |
. . . . . . 7
             |
145 | 8 | oveq1d 6323 |
. . . . . . 7
            |
146 | 144, 145 | eqtr2d 2506 |
. . . . . 6
          |
147 | | fveq2 5879 |
. . . . . . . . . 10
           |
148 | 147 | oveq1d 6323 |
. . . . . . . . 9
               |
149 | 148 | adantl 473 |
. . . . . . . 8
 
               |
150 | 14, 131, 131 | 3jca 1210 |
. . . . . . . . 9
 
   |
151 | 136 | leidd 10201 |
. . . . . . . . . 10

  |
152 | 138, 151 | jca 541 |
. . . . . . . . 9
 
   |
153 | | elfz2 11817 |
. . . . . . . . 9
    
 
 
    |
154 | 150, 152,
153 | sylanbrc 677 |
. . . . . . . 8
       |
155 | 10, 22 | syl6eqel 2557 |
. . . . . . . . 9
       |
156 | 155, 95 | resubcld 10068 |
. . . . . . . 8
         |
157 | 127, 149,
154, 156 | fvmptd 5969 |
. . . . . . 7
             |
158 | 10 | oveq1d 6323 |
. . . . . . 7
           |
159 | 157, 158 | eqtr2d 2506 |
. . . . . 6
         |
160 | 146, 159 | oveq12d 6326 |
. . . . 5
      ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)        |
161 | 160 | itgeq1d 37930 |
. . . 4
       ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)          
     |
162 | 27 | fnvinran 37398 |
. . . . . . . 8
 
           |
163 | 95 | adantr 472 |
. . . . . . . 8
 
       |
164 | 162, 163 | resubcld 10068 |
. . . . . . 7
 
             |
165 | 164, 126 | fmptd 6061 |
. . . . . 6
           |
166 | 40, 43, 96, 29 | ltsub1dd 10246 |
. . . . . . 7
 
 ..^                  |
167 | 39, 164 | syldan 478 |
. . . . . . . 8
 
 ..^          |
168 | 126 | fvmpt2 5972 |
. . . . . . . 8
                         |
169 | 39, 167, 168 | syl2anc 673 |
. . . . . . 7
 
 ..^              |
170 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
171 | 170 | oveq1d 6323 |
. . . . . . . . . . 11
               |
172 | 171 | cbvmptv 4488 |
. . . . . . . . . 10
                         |
173 | 126, 172 | eqtri 2493 |
. . . . . . . . 9
             |
174 | 173 | a1i 11 |
. . . . . . . 8
 
 ..^                |
175 | | fveq2 5879 |
. . . . . . . . . 10
               |
176 | 175 | oveq1d 6323 |
. . . . . . . . 9
                   |
177 | 176 | adantl 473 |
. . . . . . . 8
    ..^                     |
178 | 43, 96 | resubcld 10068 |
. . . . . . . 8
 
 ..^            |
179 | 174, 177,
42, 178 | fvmptd 5969 |
. . . . . . 7
 
 ..^                  |
180 | 166, 169,
179 | 3brtr4d 4426 |
. . . . . 6
 
 ..^              |
181 | | frn 5747 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)   
  |
182 | 30, 181 | syl 17 |
. . . . . . . 8
   |
183 | 182 | adantr 472 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)         |
184 | | ffun 5742 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)      |
185 | 30, 184 | syl 17 |
. . . . . . . . 9
   |
186 | 185 | adantr 472 |
. . . . . . . 8
 
      ![[,] [,]](_icc.gif)         |
187 | 23 | a1i 11 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)          |
188 | 22 | a1i 11 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)         |
189 | 95 | adantr 472 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)         |
190 | 144, 143 | eqeltrd 2549 |
. . . . . . . . . . . . 13
       |
191 | 190 | adantr 472 |
. . . . . . . . . . . 12
 
      ![[,] [,]](_icc.gif)             |
192 | 157, 156 | eqeltrd 2549 |
. . . . . . . . . . . . 13
       |
193 | 192 | adantr 472 |
. . . . . . . . . . . 12
 
      ![[,] [,]](_icc.gif)             |
194 | | simpr 468 |
. . . . . . . . . . . 12
 
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
195 | | eliccre 37699 |
. . . . . . . . . . . 12
                ![[,] [,]](_icc.gif)         |
196 | 191, 193,
194, 195 | syl3anc 1292 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)         |
197 | 189, 196 | readdcld 9688 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)       
   |
198 | 128 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
           |
199 | 198 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
 
               |
200 | 127, 199,
141, 143 | fvmptd 5969 |
. . . . . . . . . . . . . 14
             |
201 | 200 | oveq2d 6324 |
. . . . . . . . . . . . 13
                 |
202 | 95 | recnd 9687 |
. . . . . . . . . . . . . 14
   |
203 | 142 | recnd 9687 |
. . . . . . . . . . . . . 14
       |
204 | 202, 203 | pncan3d 10008 |
. . . . . . . . . . . . 13
               |
205 | 201, 204,
8 | 3eqtrrd 2510 |
. . . . . . . . . . . 12
          |
206 | 205 | adantr 472 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)                |
207 | | elicc2 11724 |
. . . . . . . . . . . . . . 15
                  ![[,] [,]](_icc.gif)          
        |
208 | 191, 193,
207 | syl2anc 673 |
. . . . . . . . . . . . . 14
 
      ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
    
        |
209 | 194, 208 | mpbid 215 |
. . . . . . . . . . . . 13
 
      ![[,] [,]](_icc.gif)                   |
210 | 209 | simp2d 1043 |
. . . . . . . . . . . 12
 
      ![[,] [,]](_icc.gif)             |
211 | 191, 196,
189, 210 | leadd2dd 10249 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)       
         |
212 | 206, 211 | eqbrtrd 4416 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)            |
213 | 209 | simp3d 1044 |
. . . . . . . . . . . 12
 
      ![[,] [,]](_icc.gif)             |
214 | 196, 193,
189, 213 | leadd2dd 10249 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)       
         |
215 | 157 | oveq2d 6324 |
. . . . . . . . . . . . 13
                 |
216 | 155 | recnd 9687 |
. . . . . . . . . . . . . 14
       |
217 | 202, 216 | pncan3d 10008 |
. . . . . . . . . . . . 13
               |
218 | 215, 217,
10 | 3eqtrrd 2510 |
. . . . . . . . . . . 12
         |
219 | 218 | adantr 472 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)               |
220 | 214, 219 | breqtrrd 4422 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)       
   |
221 | 187, 188,
197, 212, 220 | eliccd 37697 |
. . . . . . . . 9
 
      ![[,] [,]](_icc.gif)       
    ![[,] [,]](_icc.gif)    |
222 | | fdm 5745 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
223 | 30, 222 | syl 17 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)    |
224 | 223 | eqcomd 2477 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif) 
  |
225 | 224 | adantr 472 |
. . . . . . . . 9
 
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
226 | 221, 225 | eleqtrd 2551 |
. . . . . . . 8
 
      ![[,] [,]](_icc.gif)       
   |
227 | | fvelrn 6030 |
. . . . . . . 8
  
     
    |
228 | 186, 226,
227 | syl2anc 673 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)               |
229 | 183, 228 | sseldd 3419 |
. . . . . 6
 
      ![[,] [,]](_icc.gif)               |
230 | 169, 167 | eqeltrd 2549 |
. . . . . . 7
 
 ..^        |
231 | 179, 178 | eqeltrd 2549 |
. . . . . . 7
 
 ..^          |
232 | 82, 60 | fssresd 5762 |
. . . . . . . . . . 11
 
 ..^                                      |
233 | 40 | rexrd 9708 |
. . . . . . . . . . . . . 14
 
 ..^        |
234 | 233 | adantr 472 |
. . . . . . . . . . . . 13
    ..^                       |
235 | 43 | rexrd 9708 |
. . . . . . . . . . . . . 14
 
 ..^          |
236 | 235 | adantr 472 |
. . . . . . . . . . . . 13
    ..^                         |
237 | 95 | ad2antrr 740 |
. . . . . . . . . . . . . 14
    ..^                   |
238 | | elioore 11691 |
. . . . . . . . . . . . . . 15
                 |
239 | 238 | adantl 473 |
. . . . . . . . . . . . . 14
    ..^                   |
240 | 237, 239 | readdcld 9688 |
. . . . . . . . . . . . 13
    ..^                 
   |
241 | 169 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
 
 ..^                  |
242 | 202 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
 ..^    |
243 | 40 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 
 ..^        |
244 | 242, 243 | pncan3d 10008 |
. . . . . . . . . . . . . . . 16
 
 ..^                |
245 | | eqidd 2472 |
. . . . . . . . . . . . . . . 16
 
 ..^            |
246 | 241, 244,
245 | 3eqtrrd 2510 |
. . . . . . . . . . . . . . 15
 
 ..^              |
247 | 246 | adantr 472 |
. . . . . . . . . . . . . 14
    ..^                             |
248 | 230 | adantr 472 |
. . . . . . . . . . . . . . 15
    ..^                       |
249 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
    ..^                                 |
250 | 248 | rexrd 9708 |
. . . . . . . . . . . . . . . . . 18
    ..^                       |
251 | 231 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^          |
252 | 251 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
    ..^                         |
253 | | elioo2 11702 |
. . . . . . . . . . . . . . . . . 18
                           
    
          |
254 | 250, 252,
253 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
    ..^                               
    
          |
255 | 249, 254 | mpbid 215 |
. . . . . . . . . . . . . . . 16
    ..^                               |
256 | 255 | simp2d 1043 |
. . . . . . . . . . . . . . 15
    ..^                       |
257 | 248, 239,
237, 256 | ltadd2dd 9811 |
. . . . . . . . . . . . . 14
    ..^                 
         |
258 | 247, 257 | eqbrtrd 4416 |
. . . . . . . . . . . . 13
    ..^                         |
259 | 231 | adantr 472 |
. . . . . . . . . . . . . . 15
    ..^                         |
260 | 255 | simp3d 1044 |
. . . . . . . . . . . . . . 15
    ..^                         |
261 | 239, 259,
237, 260 | ltadd2dd 9811 |
. . . . . . . . . . . . . 14
    ..^                 
           |
262 | 179 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
 
 ..^                      |
263 | 43 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 
 ..^          |
264 | 242, 263 | pncan3d 10008 |
. . . . . . . . . . . . . . . 16
 
 ..^                    |
265 | 262, 264 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
 
 ..^                  |
266 | 265 | adantr 472 |
. . . . . . . . . . . . . 14
    ..^                 
               |
267 | 261, 266 | breqtrd 4420 |
. . . . . . . . . . . . 13
    ..^                 
         |
268 | 234, 236,
240, 258, 267 | eliood 37691 |
. . . . . . . . . . . 12
    ..^                 
                 |
269 | | eqid 2471 |
. . . . . . . . . . . 12
                                     |
270 | 268, 269 | fmptd 6061 |
. . . . . . . . . . 11
 
 ..^                                                      |
271 | | fcompt 6075 |
. . . . . . . . . . 11
                                                                                                                                                                                       |
272 | 232, 270,
271 | syl2anc 673 |
. . . . . . . . . 10
 
 ..^                                                                                                  |
273 | | oveq2 6316 |
. . . . . . . . . . . . . . . 16
 
     |
274 | 273 | cbvmptv 4488 |
. . . . . . . . . . . . . . 15
                                     |
275 | 274 | fveq1i 5880 |
. . . . . . . . . . . . . 14
                                             |
276 | 275 | fveq2i 5882 |
. . . . . . . . . . . . 13
 
                                                                                   |
277 | 276 | mpteq2i 4479 |
. . . . . . . . . . . 12
                
                                                                                                    |
278 | 277 | a1i 11 |
. . . . . . . . . . 11
 
 ..^                                                                                                                        |
279 | | fveq2 5879 |
. . . . . . . . . . . . . 14
                                               |
280 | 279 | fveq2d 5883 |
. . . . . . . . . . . . 13
                                            
                                          |
281 | 280 | cbvmptv 4488 |
. . . . . . . . . . . 12
                
                                                                                                    |
282 | 281 | a1i 11 |
. . . . . . . . . . 11
 
 ..^                                                                                                                        |
283 | | eqidd 2472 |
. . . . . . . . . . . . . . 15
    ..^                                                       |
284 | | oveq2 6316 |
. . . . . . . . . . . . . . . 16
 
     |
285 | 284 | adantl 473 |
. . . . . . . . . . . . . . 15
   
 ..^ 
              
       |
286 | 283, 285,
249, 240 | fvmptd 5969 |
. . . . . . . . . . . . . 14
    ..^                                           |
287 | 286 | fveq2d 5883 |
. . . . . . . . . . . . 13
    ..^                                                            
                 
    |
288 | | fvres 5893 |
. . . . . . . . . . . . . 14
                                          
    |
289 | 268, 288 | syl 17 |
. . . . . . . . . . . . 13
    ..^                                          
    |
290 | 287, 289 | eqtrd 2505 |
. . . . . . . . . . . 12
    ..^                                                                   |
291 | 290 | mpteq2dva 4482 |
. . . . . . . . . . 11
 
 ..^                                                                              
     |
292 | 278, 282,
291 | 3eqtrd 2509 |
. . . . . . . . . 10
 
 ..^                                                                              
     |
293 | 272, 292 | eqtr2d 2506 |
. . . . . . . . 9
 
 ..^                    
                                         |
294 | | eqid 2471 |
. . . . . . . . . . 11
         |
295 | | ssid 3437 |
. . . . . . . . . . . . . . 15
 |
296 | 295 | a1i 11 |
. . . . . . . . . . . . . 14
   |
297 | | id 22 |
. . . . . . . . . . . . . 14
   |
298 | 296, 297,
296 | constcncfg 37845 |
. . . . . . . . . . . . 13
         |
299 | | cncfmptid 22022 |
. . . . . . . . . . . . . . 15
 
         |
300 | 295, 295,
299 | mp2an 686 |
. . . . . . . . . . . . . 14
       |
301 | 300 | a1i 11 |
. . . . . . . . . . . . 13
         |
302 | 298, 301 | addcncf 37847 |
. . . . . . . . . . . 12
           |
303 | 242, 302 | syl 17 |
. . . . . . . . . . 11
 
 ..^            |
304 | | ioosscn 37687 |
. . . . . . . . . . . 12
               |
305 | 304 | a1i 11 |
. . . . . . . . . . 11
 
 ..^                  |
306 | | ioosscn 37687 |
. . . . . . . . . . . 12
               |
307 | 306 | a1i 11 |
. . . . . . . . . . 11
 
 ..^                  |
308 | 294, 303,
305, 307, 268 | cncfmptssg 37844 |
. . . . . . . . . 10
 
 ..^                                                      |
309 | 308, 64 | cncfco 22017 |
. . . . . . . . 9
 
 ..^                                                          |
310 | 293, 309 | eqeltrd 2549 |
. . . . . . . 8
 
 ..^                    
                       |
311 | 233 | adantr 472 |
. . . . . . . . . . . . . . 15
    ..^                           |
312 | 235 | adantr 472 |
. . . . . . . . . . . . . . 15
    ..^                             |
313 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
    ..^                                         |
314 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
315 | 269 | elrnmpt 5087 |
. . . . . . . . . . . . . . . . . 18
                                         |
316 | 314, 315 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
                   
                   |
317 | 313, 316 | sylib 201 |
. . . . . . . . . . . . . . . 16
    ..^                                         |
318 | | nfv 1769 |
. . . . . . . . . . . . . . . . . 18
    ..^   |
319 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . 20
                     |
320 | 319 | nfrn 5083 |
. . . . . . . . . . . . . . . . . . 19
                     |
321 | 320 | nfcri 2606 |
. . . . . . . . . . . . . . . . . 18
                    |
322 | 318, 321 | nfan 2031 |
. . . . . . . . . . . . . . . . 17
   
 ..^ 
                    |
323 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
  |
324 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . 20
 
                     |
325 | 95 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
326 | 238 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
327 | 325, 326 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . 20
 
                 
   |
328 | 324, 327 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
329 | 328 | 3exp 1230 |
. . . . . . . . . . . . . . . . . 18
                  
    |
330 | 329 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
    ..^                                   
       |
331 | 322, 323,
330 | rexlimd 2866 |
. . . . . . . . . . . . . . . 16
    ..^                                           |
332 | 317, 331 | mpd 15 |
. . . . . . . . . . . . . . 15
    ..^                       |
333 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
     
 |
334 | 258 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                           |
335 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                       |
336 | 334, 335 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . . . 19
    ..^                         |
337 | 336 | 3exp 1230 |
. . . . . . . . . . . . . . . . . 18
 
 ..^                
           |
338 | 337 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    ..^                                   
           |
339 | 322, 333,
338 | rexlimd 2866 |
. . . . . . . . . . . . . . . 16
    ..^                                               |
340 | 317, 339 | mpd 15 |
. . . . . . . . . . . . . . 15
    ..^                           |
341 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
        |
342 | 267 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                   
         |
343 | 335, 342 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . 19
    ..^                           |
344 | 343 | 3exp 1230 |
. . . . . . . . . . . . . . . . . 18
 
 ..^                
             |
345 | 344 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    ..^                                   
             |
346 | 322, 341,
345 | rexlimd 2866 |
. . . . . . . . . . . . . . . 16
    ..^                                                 |
347 | 317, 346 | mpd 15 |
. . . . . . . . . . . . . . 15
    ..^                             |
348 | 311, 312,
332, 340, 347 | eliood 37691 |
. . . . . . . . . . . . . 14
    ..^                                     |
349 | 223 | ineq2d 3625 |
. . . . . . . . . . . . . . . . 17
                                   ![[,] [,]](_icc.gif)     |
350 | 349 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
 ..^                                    ![[,] [,]](_icc.gif)     |
351 | | dmres 5131 |
. . . . . . . . . . . . . . . . 17
                                 |
352 | 351 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
 ..^ 
                                  |
353 | | dfss 3405 |
. . . . . . . . . . . . . . . . 17
                  ![[,] [,]](_icc.gif) 
                                ![[,] [,]](_icc.gif)     |
354 | 60, 353 | sylib 201 |
. . . . . . . . . . . . . . . 16
 
 ..^                                  ![[,] [,]](_icc.gif)     |
355 | 350, 352,
354 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . 15
 
 ..^ 
                                |
356 | 355 | adantr 472 |
. . . . . . . . . . . . . 14
    ..^                    
                                |
357 | 348, 356 | eleqtrrd 2552 |
. . . . . . . . . . . . 13
    ..^                     
   |