Step | Hyp | Ref
| Expression |
1 | | fourierdlem50.u |
. . 3
   ..^                                |
2 | | fourierdlem50.m |
. . . . . . . 8
   |
3 | | fourierdlem50.a |
. . . . . . . 8
   |
4 | | fourierdlem50.b |
. . . . . . . 8
   |
5 | | fourierdlem50.altb |
. . . . . . . . 9
   |
6 | 3, 4, 5 | ltled 9780 |
. . . . . . . 8

  |
7 | | fourierdlem50.p |
. . . . . . . . . . . . 13
 
                        ..^                |
8 | | fourierdlem50.v |
. . . . . . . . . . . . 13
       |
9 | 7, 2, 8 | fourierdlem15 37978 |
. . . . . . . . . . . 12
              ![[,] [,]](_icc.gif)      |
10 | | pire 23406 |
. . . . . . . . . . . . . . . 16
 |
11 | 10 | renegcli 9932 |
. . . . . . . . . . . . . . 15
  |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
    |
13 | | fourierdlem50.xre |
. . . . . . . . . . . . . 14
   |
14 | 12, 13 | readdcld 9667 |
. . . . . . . . . . . . 13
      |
15 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
   |
16 | 15, 13 | readdcld 9667 |
. . . . . . . . . . . . 13
     |
17 | 14, 16 | iccssred 37596 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)   
  |
18 | 9, 17 | fssd 5736 |
. . . . . . . . . . 11
           |
19 | 18 | ffvelrnda 6020 |
. . . . . . . . . 10
 
           |
20 | 13 | adantr 467 |
. . . . . . . . . 10
 
       |
21 | 19, 20 | resubcld 10044 |
. . . . . . . . 9
 
             |
22 | | fourierdlem50.q |
. . . . . . . . 9
             |
23 | 21, 22 | fmptd 6044 |
. . . . . . . 8
           |
24 | 22 | a1i 11 |
. . . . . . . . . . 11
               |
25 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
26 | 25 | oveq1d 6303 |
. . . . . . . . . . . 12
               |
27 | 26 | adantl 468 |
. . . . . . . . . . 11
 
               |
28 | | nnssnn0 10869 |
. . . . . . . . . . . . . . 15
 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . 14

  |
30 | | nn0uz 11190 |
. . . . . . . . . . . . . 14
     |
31 | 29, 30 | syl6sseq 3477 |
. . . . . . . . . . . . 13

      |
32 | 31, 2 | sseldd 3432 |
. . . . . . . . . . . 12
       |
33 | | eluzfz1 11803 |
. . . . . . . . . . . 12
    
      |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
       |
35 | 18, 34 | ffvelrnd 6021 |
. . . . . . . . . . . 12
       |
36 | 35, 13 | resubcld 10044 |
. . . . . . . . . . 11
         |
37 | 24, 27, 34, 36 | fvmptd 5952 |
. . . . . . . . . 10
             |
38 | 7 | fourierdlem2 37965 |
. . . . . . . . . . . . . . . 16
 
   
                         ..^                 |
39 | 2, 38 | syl 17 |
. . . . . . . . . . . . . . 15
                               ..^                 |
40 | 8, 39 | mpbid 214 |
. . . . . . . . . . . . . 14
                          ..^                |
41 | 40 | simprd 465 |
. . . . . . . . . . . . 13
                   ..^               |
42 | 41 | simpld 461 |
. . . . . . . . . . . 12
        
         |
43 | 42 | simpld 461 |
. . . . . . . . . . 11
          |
44 | 43 | oveq1d 6303 |
. . . . . . . . . 10
              |
45 | 12 | recnd 9666 |
. . . . . . . . . . 11
    |
46 | 13 | recnd 9666 |
. . . . . . . . . . 11
   |
47 | 45, 46 | pncand 9984 |
. . . . . . . . . 10
         |
48 | 37, 44, 47 | 3eqtrd 2488 |
. . . . . . . . 9
        |
49 | 12 | rexrd 9687 |
. . . . . . . . . 10
    |
50 | 15 | rexrd 9687 |
. . . . . . . . . 10
   |
51 | | fourierdlem50.ab |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
52 | 3 | leidd 10177 |
. . . . . . . . . . . 12

  |
53 | 3, 4, 3, 52, 6 | eliccd 37595 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
54 | 51, 53 | sseldd 3432 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    |
55 | | iccgelb 11688 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)      |
56 | 49, 50, 54, 55 | syl3anc 1267 |
. . . . . . . . 9
    |
57 | 48, 56 | eqbrtrd 4422 |
. . . . . . . 8
    
  |
58 | 4 | leidd 10177 |
. . . . . . . . . . . 12

  |
59 | 3, 4, 4, 6, 58 | eliccd 37595 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
60 | 51, 59 | sseldd 3432 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    |
61 | | iccleub 11687 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     |
62 | 49, 50, 60, 61 | syl3anc 1267 |
. . . . . . . . 9

  |
63 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
64 | 63 | oveq1d 6303 |
. . . . . . . . . . . 12
               |
65 | 64 | adantl 468 |
. . . . . . . . . . 11
 
               |
66 | | eluzfz2 11804 |
. . . . . . . . . . . 12
    
      |
67 | 32, 66 | syl 17 |
. . . . . . . . . . 11
       |
68 | 18, 67 | ffvelrnd 6021 |
. . . . . . . . . . . 12
       |
69 | 68, 13 | resubcld 10044 |
. . . . . . . . . . 11
         |
70 | 24, 65, 67, 69 | fvmptd 5952 |
. . . . . . . . . 10
             |
71 | 42 | simprd 465 |
. . . . . . . . . . 11
         |
72 | 71 | oveq1d 6303 |
. . . . . . . . . 10
             |
73 | 15 | recnd 9666 |
. . . . . . . . . . 11
   |
74 | 73, 46 | pncand 9984 |
. . . . . . . . . 10
       |
75 | 70, 72, 74 | 3eqtrrd 2489 |
. . . . . . . . 9
       |
76 | 62, 75 | breqtrd 4426 |
. . . . . . . 8

      |
77 | | fourierdlem50.j |
. . . . . . . 8
  ..^   |
78 | | fourierdlem50.t |
. . . . . . . 8
   
        |
79 | | prfi 7843 |
. . . . . . . . . . . 12
    |
80 | 79 | a1i 11 |
. . . . . . . . . . 11
   
  |
81 | | fzfid 12183 |
. . . . . . . . . . . . 13
       |
82 | 22 | rnmptfi 37429 |
. . . . . . . . . . . . 13
       |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . 12
   |
84 | | infi 7792 |
. . . . . . . . . . . 12
         |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
         |
86 | | unfi 7835 |
. . . . . . . . . . 11
    
          
         |
87 | 80, 85, 86 | syl2anc 666 |
. . . . . . . . . 10
    
         |
88 | 78, 87 | syl5eqel 2532 |
. . . . . . . . 9
   |
89 | 3, 4 | jca 535 |
. . . . . . . . . . . 12
     |
90 | | prssg 4126 |
. . . . . . . . . . . . 13
 
   
      |
91 | 3, 4, 90 | syl2anc 666 |
. . . . . . . . . . . 12
   
      |
92 | 89, 91 | mpbid 214 |
. . . . . . . . . . 11
      |
93 | | inss2 3652 |
. . . . . . . . . . . . 13

          |
94 | | ioossre 11693 |
. . . . . . . . . . . . 13
     |
95 | 93, 94 | sstri 3440 |
. . . . . . . . . . . 12

      |
96 | 95 | a1i 11 |
. . . . . . . . . . 11
      
  |
97 | 92, 96 | unssd 3609 |
. . . . . . . . . 10
    
      
  |
98 | 78, 97 | syl5eqss 3475 |
. . . . . . . . 9

  |
99 | | fourierdlem50.s |
. . . . . . . . 9
            |
100 | | fourierdlem50.n |
. . . . . . . . 9
       |
101 | 88, 98, 99, 100 | fourierdlem36 38000 |
. . . . . . . 8

         |
102 | | eqid 2450 |
. . . . . . . 8
  
 ..^    
      
    ..^          
  |
103 | 2, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102 | fourierdlem20 37983 |
. . . . . . 7
   ..^                                |
104 | | fourierdlem50.ch |
. . . . . . . . . . . . 13
      ..^               
              
 ..^               
                 |
105 | 104 | biimpi 198 |
. . . . . . . . . . . . . . . . . 18
    
 ..^            
                   ..^            
                    |
106 | | simp-4l 775 |
. . . . . . . . . . . . . . . . . 18
      ..^               
              
 ..^               
                 |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
108 | | simplr 761 |
. . . . . . . . . . . . . . . . . 18
      ..^               
              
 ..^               
                ..^   |
109 | 105, 108 | syl 17 |
. . . . . . . . . . . . . . . . 17

 ..^   |
110 | 107, 109 | jca 535 |
. . . . . . . . . . . . . . . 16
   ..^    |
111 | | simp-4r 776 |
. . . . . . . . . . . . . . . . 17
      ..^               
              
 ..^               
                ..^   |
112 | 105, 111 | syl 17 |
. . . . . . . . . . . . . . . 16

 ..^   |
113 | | elfzofz 11932 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
      |
114 | 113 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^               
              
 ..^               
                     |
115 | 105, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20

      |
116 | 107, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
117 | 116, 115 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . 21
       |
118 | 107, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21

  |
119 | 117, 118 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . 20
         |
120 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
121 | 120 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . 21
               |
122 | 121, 22 | fvmptg 5944 |
. . . . . . . . . . . . . . . . . . . 20
                         |
123 | 115, 119,
122 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . 19
             |
124 | 123, 119 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . 18
       |
125 | 23 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^            |
126 | | fzofzp1 12005 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
        |
127 | 126 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^          |
128 | 125, 127 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^          |
129 | 107, 112,
128 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
         |
130 | | isof1o 6214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  |
131 | 101, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
132 | | f1of 5812 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
          |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
134 | | fzofzp1 12005 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
        |
135 | 77, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
136 | 133, 135 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . 21
    
    |
137 | 98, 136 | sseldd 3432 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
138 | 107, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
    |
139 | | elfzofz 11932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
      |
140 | 77, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
141 | 133, 140 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
142 | 98, 141 | sseldd 3432 |
. . . . . . . . . . . . . . . . . . . . 21
       |
143 | 107, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
       |
144 | 105 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . 22
              
                |
145 | 124 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
146 | 23 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 ..^            |
147 | | fzofzp1 12005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
        |
148 | 147 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 ..^          |
149 | 146, 148 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 ..^          |
150 | 149 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 ..^          |
151 | 110, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
152 | 143 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
153 | 138 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
    |
154 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ..^
  |
155 | 154 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
  |
156 | 155 | ltp1d 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^
    |
157 | 77, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
158 | | isoeq5 6212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
       
                     |
159 | 78, 158 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
                    |
160 | 101, 159 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

                    |
161 | | isorel 6215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                  
    
      
                |
162 | 160, 140,
135, 161 | syl12anc 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    
         |
163 | 157, 162 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
        |
164 | 107, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
        |
165 | 145, 151,
152, 153, 164 | ioossioobi 37612 |
. . . . . . . . . . . . . . . . . . . . . 22
            
                             
 
          |
166 | 144, 165 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21
             
 
         |
167 | 166 | simpld 461 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
168 | 124, 143,
138, 167, 164 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . 19
    
        |
169 | | elfzofz 11932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^
      |
170 | 169 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^            
                        |
171 | 170 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      ..^               
              
 ..^               
                     |
172 | 105, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23

      |
173 | 107, 172,
21 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
174 | 22 | fvmpt2 5955 |
. . . . . . . . . . . . . . . . . . . . . . 23
                         |
175 | 172, 173,
174 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
176 | 175, 173 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . . . . 21
       |
177 | | simpllr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^               
              
 ..^               
                            
                |
178 | 105, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
              
                |
179 | 176, 129,
143, 138, 164, 178 | fourierdlem10 37973 |
. . . . . . . . . . . . . . . . . . . 20
             
 
         |
180 | 179 | simprd 465 |
. . . . . . . . . . . . . . . . . . 19
    
 
        |
181 | 124, 138,
129, 168, 180 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . 18
    
        |
182 | 124, 129,
118, 181 | ltadd2dd 9791 |
. . . . . . . . . . . . . . . . 17
                 |
183 | 123 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . 18
                 |
184 | 107, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19

  |
185 | 117 | recnd 9666 |
. . . . . . . . . . . . . . . . . . 19
       |
186 | 184, 185 | pncan3d 9986 |
. . . . . . . . . . . . . . . . . 18
               |
187 | 183, 186 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . 17
             |
188 | 112, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         |
189 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 ..^            |
190 | 189, 127 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 ..^          |
191 | 107, 112,
190 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
192 | 191, 118 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . 21
           |
193 | 188, 192 | jca 535 |
. . . . . . . . . . . . . . . . . . . 20
                   |
194 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
         |
195 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
196 | 195 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
197 | 196 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
           |
198 | 194, 197 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . . . . 22
                                   |
199 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
200 | 199, 196 | eqeq12d 2465 |
. . . . . . . . . . . . . . . . . . . . . 22
             
                 |
201 | 198, 200 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . 21
         
                                                     |
202 | 201, 122 | vtoclg 3106 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
203 | 188, 193,
202 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
                 |
204 | 203 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . 18
                     |
205 | 191 | recnd 9666 |
. . . . . . . . . . . . . . . . . . 19
         |
206 | 184, 205 | pncan3d 9986 |
. . . . . . . . . . . . . . . . . 18
                   |
207 | 204, 206 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . 17
                 |
208 | 182, 187,
207 | 3brtr4d 4432 |
. . . . . . . . . . . . . . . 16
    
        |
209 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . 20
   ..^
 ..^    |
210 | 209 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
 ..^ 
   ..^   ..^     |
211 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . 21
       |
212 | 211 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . 20
               |
213 | 212 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . 19
     
     
             |
214 | 210, 213 | anbi12d 716 |
. . . . . . . . . . . . . . . . . 18
      ..^ 
 ..^            
  
 ..^   ..^                |
215 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
216 | 215 | breq2d 4413 |
. . . . . . . . . . . . . . . . . 18
     
   
           |
217 | 214, 216 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
     
 ..^   ..^            
              ..^   ..^                         |
218 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^
 ..^    |
219 | 218 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . . 21
  
 ..^  
 ..^     |
220 | 219 | anbi1d 710 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
 ..^ 
   ..^   ..^     |
221 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
           |
222 | 221 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . . 20
     
     
             |
223 | 220, 222 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
 ..^            
  
 ..^   ..^                |
224 | 221 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . 19
     
   
           |
225 | 223, 224 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
     
 ..^   ..^            
              ..^   ..^                         |
226 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  |
227 | 226 | ad3antlr 736 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
 ..^            
  |
228 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  |
229 | 228 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
 ..^               |
230 | | simplr 761 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
 ..^            
               |
231 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 ..^            |
232 | | fzofzp1 12005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ..^
        |
233 | 232 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 ..^          |
234 | 231, 233 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 ..^          |
235 | 234 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^   ..^ 
        |
236 | 235 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
 ..^ 
           |
237 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 ..^            |
238 | | elfzofz 11932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
      |
239 | 238 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 ..^        |
240 | 237, 239 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 ..^        |
241 | 240 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
 ..^ 
         |
242 | 228 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ..^
  |
243 | | peano2re 9803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
    |
245 | 244 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 ..^ 
 ..^ 
       |
246 | 226 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
  |
247 | 246 | ad3antlr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 ..^ 
 ..^ 
     |
248 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 ..^ 
 ..^ 
  
    |
249 | 245, 247,
248 | nltled 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
 ..^ 
       |
250 | 228 | peano2zd 11040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  ..^
    |
251 | 250 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    ..^
 ..^   
     |
252 | 226 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    ..^
 ..^   
   |
253 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    ..^
 ..^   
  
  |
254 | | eluz2 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
255 | 251, 252,
253, 254 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    ..^
 ..^   
         |
256 | 255 | adantlll 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 ..^ 
 ..^   
         |
257 | | simplll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 ..^ 
 ..^ 
         |
258 | | 0zd 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    ..^
 ..^ 
         |
259 | | elfzoel2 11916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  ..^
  |
260 | 259 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    ..^
 ..^ 
         |
261 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
262 | 261 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    ..^
 ..^ 
         |
263 | 258, 260,
262 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    ..^
 ..^ 
           |
264 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^          |
265 | 261 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
266 | 265 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^          |
267 | 242 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^          |
268 | | elfzole1 11925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  ..^
  |
269 | 268 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^          |
270 | 267, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   ..^            |
271 | 267 | ltp1d 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   ..^            |
272 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           |
273 | 272 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   ..^            |
274 | 267, 270,
266, 271, 273 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^          |
275 | 264, 267,
266, 269, 274 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^          |
276 | 264, 266,
275 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^          |
277 | 276 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    ..^
 ..^ 
         |
278 | 265 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^          |
279 | 259 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  ..^
  |
280 | 279 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^          |
281 | 246 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^          |
282 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
283 | 282 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^          |
284 | | elfzolt2 11926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  ..^
  |
285 | 284 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^          |
286 | 278, 281,
280, 283, 285 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^          |
287 | 278, 280,
286 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^          |
288 | 287 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    ..^
 ..^ 
         |
289 | 263, 277,
288 | jca32 538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    ..^
 ..^ 
          
    |
290 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
 
 
    |
291 | 289, 290 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    ..^
 ..^ 
             |
292 | 291 | adantlll 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 ..^ 
 ..^ 
             |
293 | 257, 292,
19 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 ..^ 
 ..^ 
             |
294 | 293 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ..^ 
 ..^   

      
      |
295 | | simplll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 ..^ 
 ..^ 
           |
296 | | 0zd 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   ..^            |
297 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
298 | 297 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   ..^            |
299 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^            |
300 | 298 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^            |
301 | 242 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^            |
302 | 268 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^            |
303 | 301, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^              |
304 | 301 | ltp1d 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^              |
305 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
             |
306 | 305 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   ..^              |
307 | 301, 303,
300, 304, 306 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ..^            |
308 | 299, 301,
300, 302, 307 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^            |
309 | 299, 300,
308 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   ..^            |
310 | | eluz2 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
311 | 296, 298,
309, 310 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   ..^                |
312 | 311 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 ..^ 
 ..^ 
               |
313 | | elfzoel2 11916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  ..^
  |
314 | 313 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 ..^ 
 ..^ 
           |
315 | 297 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
316 | 315 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^            |
317 | | peano2rem 9938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
318 | 246, 317 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  ..^
    |
319 | 318 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^              |
320 | 279 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^            |
321 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             |
322 | 321 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^              |
323 | 246 | ltm1d 10536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  ..^
    |
324 | 318, 246,
279, 323, 284 | lttrd 9793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  ..^
    |
325 | 324 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   ..^              |
326 | 316, 319,
320, 322, 325 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   ..^            |
327 | 326 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    ..^             |
328 | 327 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 ..^ 
 ..^ 
           |
329 | | elfzo2 11920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  ..^     
   |
330 | 312, 314,
328, 329 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 ..^ 
 ..^ 
          ..^   |
331 | 169, 19 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
 ..^        |
332 | 41 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   ..^              |
333 | 332 | r19.21bi 2756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
 ..^              |
334 | 331, 190,
333 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
 ..^              |
335 | 295, 330,
334 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 ..^ 
 ..^ 
                     |
336 | 335 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ..^ 
 ..^   

        
            |
337 | 256, 294,
336 | monoord 12240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
 ..^   
      
      |
338 | 249, 337 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
 ..^ 
               |
339 | 236, 241,
338 | lensymd 9783 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 ..^ 
 ..^ 
  
            |
340 | 339 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
 ..^            
  
            |
341 | 230, 340 | condan 802 |
. . . . . . . . . . . . . . . . . . . . 21
   
 ..^ 
 ..^                 |
342 | | zleltp1 10984 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
343 | 227, 229,
342 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
   
 ..^ 
 ..^                   |
344 | 341, 343 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
 ..^               |
345 | | eluz2 11162 |
. . . . . . . . . . . . . . . . . . . 20
         |
346 | 227, 229,
344, 345 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
 ..^                   |
347 | 18 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . . . 21
   
 ..^ 
 ..^ 
               |
348 | | 0zd 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^
 ..^ 
       |
349 | 259 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^
 ..^ 
    
  |
350 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
351 | 350 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^
 ..^ 
       |
352 | 348, 349,
351 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^
 ..^ 
     
   |
353 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
354 | 246 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
355 | 350 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
356 | 355 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
357 | | elfzole1 11925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
  |
358 | 357 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
359 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
360 | 359 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
361 | 353, 354,
356, 358, 360 | letrd 9789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^        |
362 | 361 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^
 ..^ 
    
  |
363 | 355 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
364 | 313 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
  |
365 | 364 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
366 | 242 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   ..^        |
367 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
368 | 367 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   ..^        |
369 | | elfzolt2 11926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ..^
  |
370 | 369 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   ..^        |
371 | 363, 366,
365, 368, 370 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^        |
372 | 363, 365,
371 | ltled 9780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^        |
373 | 372 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^
 ..^ 
    
  |
374 | 352, 362,
373 | jca32 538 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ..^
 ..^ 
        
    |
375 | 374, 290 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^
 ..^ 
           |
376 | 375 | adantlll 723 |
. . . . . . . . . . . . . . . . . . . . 21
   
 ..^ 
 ..^ 
           |
377 | 347, 376 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
 ..^ 
           |
378 | 377 | adantlr 720 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
 ..^            
           |
379 | | simp-4l 775 |
. . . . . . . . . . . . . . . . . . . 20
      ..^ 
 ..^            
         |
380 | | 0zd 10946 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
381 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
382 | 381 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
383 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^          |
384 | 246 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^          |
385 | 382 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^          |
386 | 357 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^          |
387 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
388 | 387 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^          |
389 | 383, 384,
385, 386, 388 | letrd 9789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
390 | 380, 382,
389, 310 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^              |
391 | 390 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^               |
392 | 391 | adant423 37361 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^ 
 ..^            
             |
393 | 313 | ad3antlr 736 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^ 
 ..^            
      
  |
394 | 381 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
395 | 394 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
396 | 242 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
397 | 364 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
398 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
399 | 398 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^            |
400 | | zltlem1 10986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       |
401 | 381, 228,
400 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^        
     |
402 | 399, 401 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
403 | 369 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ..^          |
404 | 395, 396,
397, 402, 403 | lttrd 9793 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^          |
405 | 404 | adantll 719 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 ..^ 
 ..^ 
      
  |
406 | 405 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^ 
 ..^            
      
  |
407 | 392, 393,
406, 329 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . . 20
      ..^ 
 ..^            
        ..^   |
408 | 379, 407,
334 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
 ..^            
          
        |
409 | 346, 378,
408 | monoord 12240 |
. . . . . . . . . . . . . . . . . 18
   
 ..^ 
 ..^                
      |
410 | 225, 409 | chvarv 2106 |
. . . . . . . . . . . . . . . . 17
   
 ..^ 
 ..^                
      |
411 | 217, 410 | chvarv 2106 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
 ..^                
      |
412 | 110, 112,
208, 411 | syl21anc 1266 |
. . . . . . . . . . . . . . 15
    
      |
413 | 107, 112 | jca 535 |
. . . . . . . . . . . . . . . 16
   ..^    |
414 | 110, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
415 | 179 | simpld 461 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
416 | 176, 143,
138, 415, 164 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . . 19
    
        |
417 | 166 | simprd 465 |
. . . . . . . . . . . . . . . . . . 19
    
 
        |
418 | 176, 138,
414, 416, 417 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . 18
    
        |
419 | 176, 414,
118, 418 | ltadd2dd 9791 |
. . . . . . . . . . . . . . . . 17
                 |
420 | 175 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . 18
                 |
421 | 107, 172,
19 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . 20
       |
422 | 421 | recnd 9666 |
. . . . . . . . . . . . . . . . . . 19
       |
423 | 184, 422 | pncan3d 9986 |
. . . . . . . . . . . . . . . . . 18
               |
424 | 420, 423 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . 17
             |
425 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^                |
426 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
427 | 426 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
428 | 427 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                     |
429 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 ..^            |
430 | 429, 148 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^          |
431 | 13 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^    |
432 | 430, 431 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^            |
433 | 425, 428,
148, 432 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^                  |
434 | 107, 109,
433 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . 19
                 |
435 | 434 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . 18
                     |
436 | 110, 430 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         |
437 | 436 | recnd 9666 |
. . . . . . . . . . . . . . . . . . 19
         |
438 | 184, 437 | pncan3d 9986 |
. . . . . . . . . . . . . . . . . 18
                   |
439 | 435, 438 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . 17
                 |
440 | 419, 424,
439 | 3brtr4d 4432 |
. . . . . . . . . . . . . . . 16
    
        |
441 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . 20
   ..^
 ..^    |
442 | 441 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^ 
 ..^ 
   ..^   ..^     |
443 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . 21
       |
444 | 443 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . 20
               |
445 | 444 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . 19
     
     
             |
446 | 442, 445 | anbi12d 716 |
. . . . . . . . . . . . . . . . . 18
      ..^ 
 ..^            
  
 ..^   ..^                |
447 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
448 | 447 | breq2d 4413 |
. . . . . . . . . . . . . . . . . 18
     
   
           |
449 | 446, 448 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
     
 ..^   ..^            
              ..^   ..^                         |
450 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^
 ..^    |
451 | 450 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . . 21
  
 ..^  
 ..^     |
452 | 451 | anbi1d 710 |
. . . . . . . . . . . . . . . . . . . 20
   
 ..^ 
 ..^ 
   ..^   ..^     |
453 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
           |
454 | 453 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . . 20
     
     
             |
455 | 452, 454 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
 ..^            
  
 ..^   ..^                |
456 | 453 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . 19
     
   
           |
457 | 455, 456 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
     
 ..^   ..^            
              ..^   ..^                         |
458 | 457, 409 | chvarv 2106 |
. . . . . . . . . . . . . . . . 17
   
 ..^ 
 ..^                
      |
459 | 449, 458 | chvarv 2106 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
 ..^                
      |
460 | 413, 109,
440, 459 | syl21anc 1266 |
. . . . . . . . . . . . . . 15
    
      |
461 | 117, 421 | letri3d 9774 |
. . . . . . . . . . . . . . 15
                      
        |
462 | 412, 460,
461 | mpbir2and 932 |
. . . . . . . . . . . . . 14
           |
463 | 7, 2, 8 | fourierdlem34 37998 |
. . . . . . . . . . . . . . . 16
           |
464 | 107, 463 | syl 17 |
. . . . . . . . . . . . . . 15
           |
465 | | f1fveq 6161 |
. . . . . . . . . . . . . . 15
                             
   |
466 | 464, 115,
172, 465 | syl12anc 1265 |
. . . . . . . . . . . . . 14
             |
467 | 462, 466 | mpbid 214 |
. . . . . . . . . . . . 13

  |
468 | 104, 467 | sylbir 217 |
. . . . . . . . . . . 12
      ..^               
              
 ..^               
                 |
469 | 468 | ex 436 |
. . . . . . . . . . 11
   
 ..^               
              
 ..^             
                    |
470 | | simpl 459 |
. . . . . . . . . . . . . 14
               
                            
                |
471 | | fveq2 5863 |
. . . . . . . . . . . . . . . . 17
           |
472 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . 18
       |
473 | 472 | fveq2d 5867 |
. . . . . . . . . . . . . . . . 17
               |
474 | 471, 473 | oveq12d 6306 |
. . . . . . . . . . . . . . . 16
                               |
475 | 474 | eqcomd 2456 |
. . . . . . . . . . . . . . 15
                               |
476 | 475 | adantl 468 |
. . . . . . . . . . . . . 14
               
                                             |
477 | 470, 476 | sseqtrd 3467 |
. . . . . . . . . . . . 13
               
                            
                |
478 | 477 | ex 436 |
. . . . . . . . . . . 12
                                           
                 |
479 | 478 | ad2antlr 732 |
. . . . . . . . . . 11
   
 ..^               
              
 ..^             
                    |
480 | 469, 479 | impbid 194 |
. . . . . . . . . 10
   
 ..^               
              
 ..^             
                    |
481 | 480 | ralrimiva 2801 |
. . . . . . . . 9
    ..^ |