Step | Hyp | Ref
| Expression |
1 | | fourierdlem25.i |
. . 3
    ..^         |
2 | | ssrab2 3514 |
. . . 4
  ..^       ..^  |
3 | | ltso 9714 |
. . . . . 6
 |
4 | 3 | a1i 11 |
. . . . 5
   |
5 | | fzofi 12187 |
. . . . . . 7
 ..^  |
6 | | ssfi 7792 |
. . . . . . 7
   ..^   ..^       ..^    ..^     
  |
7 | 5, 2, 6 | mp2an 678 |
. . . . . 6
  ..^       |
8 | 7 | a1i 11 |
. . . . 5
   ..^    
   |
9 | | 0zd 10949 |
. . . . . . . 8
   |
10 | | fourierdlem25.m |
. . . . . . . . 9
   |
11 | 10 | nnzd 11039 |
. . . . . . . 8
   |
12 | 10 | nngt0d 10653 |
. . . . . . . 8
   |
13 | | fzolb 11926 |
. . . . . . . 8
  ..^     |
14 | 9, 11, 12, 13 | syl3anbrc 1192 |
. . . . . . 7
  ..^   |
15 | | fourierdlem25.qf |
. . . . . . . . 9
           |
16 | | elfzofz 11935 |
. . . . . . . . . 10
  ..^
      |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
       |
18 | 15, 17 | ffvelrnd 6023 |
. . . . . . . 8
       |
19 | 10 | nnnn0d 10925 |
. . . . . . . . . . . . 13
   |
20 | | nn0uz 11193 |
. . . . . . . . . . . . 13
     |
21 | 19, 20 | syl6eleq 2539 |
. . . . . . . . . . . 12
       |
22 | | eluzfz2 11807 |
. . . . . . . . . . . 12
    
      |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
       |
24 | 15, 23 | ffvelrnd 6023 |
. . . . . . . . . 10
       |
25 | 18, 24 | iccssred 37602 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)     
  |
26 | | fourierdlem25.cel |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)        |
27 | 25, 26 | sseldd 3433 |
. . . . . . . 8
   |
28 | 18 | rexrd 9690 |
. . . . . . . . 9
       |
29 | 24 | rexrd 9690 |
. . . . . . . . 9
       |
30 | | iccgelb 11691 |
. . . . . . . . 9
                ![[,] [,]](_icc.gif)             |
31 | 28, 29, 26, 30 | syl3anc 1268 |
. . . . . . . 8
    
  |
32 | | fourierdlem25.cnel |
. . . . . . . . . 10
   |
33 | | simpr 463 |
. . . . . . . . . . 11
 
    
      |
34 | | ffn 5728 |
. . . . . . . . . . . . . 14
               |
35 | 15, 34 | syl 17 |
. . . . . . . . . . . . 13
       |
36 | 35 | adantr 467 |
. . . . . . . . . . . 12
 
    
      |
37 | 17 | adantr 467 |
. . . . . . . . . . . 12
 
    
      |
38 | | fnfvelrn 6019 |
. . . . . . . . . . . 12
     
           |
39 | 36, 37, 38 | syl2anc 667 |
. . . . . . . . . . 11
 
    
      |
40 | 33, 39 | eqeltrd 2529 |
. . . . . . . . . 10
 
    
  |
41 | 32, 40 | mtand 665 |
. . . . . . . . 9
       |
42 | 41 | neqned 2631 |
. . . . . . . 8
       |
43 | 18, 27, 31, 42 | leneltd 9789 |
. . . . . . 7
    
  |
44 | | fveq2 5865 |
. . . . . . . . 9
           |
45 | 44 | breq1d 4412 |
. . . . . . . 8
     
       |
46 | 45 | elrab 3196 |
. . . . . . 7
   ..^        ..^        |
47 | 14, 43, 46 | sylanbrc 670 |
. . . . . 6
   ..^        |
48 | | ne0i 3737 |
. . . . . 6
   ..^        ..^        |
49 | 47, 48 | syl 17 |
. . . . 5
   ..^    
   |
50 | | fzossfz 11938 |
. . . . . . . 8
 ..^      |
51 | | fzssz 11801 |
. . . . . . . . 9
     |
52 | | zssre 10944 |
. . . . . . . . 9
 |
53 | 51, 52 | sstri 3441 |
. . . . . . . 8
     |
54 | 50, 53 | sstri 3441 |
. . . . . . 7
 ..^  |
55 | 2, 54 | sstri 3441 |
. . . . . 6
  ..^       |
56 | 55 | a1i 11 |
. . . . 5
   ..^    
   |
57 | | fisupcl 7985 |
. . . . 5
    ..^    
   ..^        ..^            ..^    
     ..^    
   |
58 | 4, 8, 49, 56, 57 | syl13anc 1270 |
. . . 4
     ..^          ..^        |
59 | 2, 58 | sseldi 3430 |
. . 3
     ..^         ..^   |
60 | 1, 59 | syl5eqel 2533 |
. 2
  ..^   |
61 | 50, 60 | sseldi 3430 |
. . . . 5
       |
62 | 15, 61 | ffvelrnd 6023 |
. . . 4
       |
63 | 62 | rexrd 9690 |
. . 3
       |
64 | | fzofzp1 12008 |
. . . . . 6
  ..^
        |
65 | 60, 64 | syl 17 |
. . . . 5
         |
66 | 15, 65 | ffvelrnd 6023 |
. . . 4
         |
67 | 66 | rexrd 9690 |
. . 3
         |
68 | 1, 58 | syl5eqel 2533 |
. . . . 5
   ..^        |
69 | | fveq2 5865 |
. . . . . . 7
           |
70 | 69 | breq1d 4412 |
. . . . . 6
     
       |
71 | 70 | elrab 3196 |
. . . . 5
   ..^        ..^        |
72 | 68, 71 | sylib 200 |
. . . 4
   ..^        |
73 | 72 | simprd 465 |
. . 3
    
  |
74 | 54, 60 | sseldi 3430 |
. . . . . . . . 9
   |
75 | | ltp1 10443 |
. . . . . . . . . 10
     |
76 | | id 22 |
. . . . . . . . . . 11
   |
77 | | peano2re 9806 |
. . . . . . . . . . 11
     |
78 | 76, 77 | ltnled 9782 |
. . . . . . . . . 10
 
 
     |
79 | 75, 78 | mpbid 214 |
. . . . . . . . 9
 

  |
80 | 74, 79 | syl 17 |
. . . . . . . 8
     |
81 | 50, 51 | sstri 3441 |
. . . . . . . . . . . 12
 ..^  |
82 | 2, 81 | sstri 3441 |
. . . . . . . . . . 11
  ..^       |
83 | 82 | a1i 11 |
. . . . . . . . . 10
 
      
  ..^        |
84 | | elrabi 3193 |
. . . . . . . . . . . . . . 15
   ..^       ..^   |
85 | | elfzo0le 11959 |
. . . . . . . . . . . . . . 15
  ..^
  |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . 14
   ..^        |
87 | 86 | adantl 468 |
. . . . . . . . . . . . 13
 
  ..^         |
88 | 87 | ralrimiva 2802 |
. . . . . . . . . . . 12
    ..^         |
89 | | breq2 4406 |
. . . . . . . . . . . . . 14
 
   |
90 | 89 | ralbidv 2827 |
. . . . . . . . . . . . 13
  
  ..^          ..^          |
91 | 90 | rspcev 3150 |
. . . . . . . . . . . 12
     ..^            ..^    
 
  |
92 | 11, 88, 91 | syl2anc 667 |
. . . . . . . . . . 11
     ..^         |
93 | 92 | adantr 467 |
. . . . . . . . . 10
 
      
    ..^    
 
  |
94 | | elfzuz 11796 |
. . . . . . . . . . . . . 14
               |
95 | 65, 94 | syl 17 |
. . . . . . . . . . . . 13
         |
96 | 95 | adantr 467 |
. . . . . . . . . . . 12
 
      
        |
97 | 11 | adantr 467 |
. . . . . . . . . . . 12
 
      
  |
98 | 53, 65 | sseldi 3430 |
. . . . . . . . . . . . . 14
     |
99 | 98 | adantr 467 |
. . . . . . . . . . . . 13
 
      
    |
100 | 97 | zred 11040 |
. . . . . . . . . . . . 13
 
      
  |
101 | | elfzle2 11803 |
. . . . . . . . . . . . . . 15
           |
102 | 65, 101 | syl 17 |
. . . . . . . . . . . . . 14
  
  |
103 | 102 | adantr 467 |
. . . . . . . . . . . . 13
 
      
    |
104 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
      
        |
105 | 66 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
      
        |
106 | 27 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
      
  |
107 | 105, 106 | ltnled 9782 |
. . . . . . . . . . . . . . . 16
 
      
      
         |
108 | 104, 107 | mpbid 214 |
. . . . . . . . . . . . . . 15
 
      
        |
109 | | iccleub 11690 |
. . . . . . . . . . . . . . . . . . 19
                ![[,] [,]](_icc.gif)             |
110 | 28, 29, 26, 109 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18

      |
111 | 110 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

        |
112 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
          
    |
113 | 112 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 

         
    |
114 | 111, 113 | breqtrd 4427 |
. . . . . . . . . . . . . . . 16
 

          |
115 | 114 | adantlr 721 |
. . . . . . . . . . . . . . 15
         
           |
116 | 108, 115 | mtand 665 |
. . . . . . . . . . . . . 14
 
      
    |
117 | 116 | neqned 2631 |
. . . . . . . . . . . . 13
 
      

   |
118 | 99, 100, 103, 117 | leneltd 9789 |
. . . . . . . . . . . 12
 
      
    |
119 | | elfzo2 11923 |
. . . . . . . . . . . 12
    ..^       
     |
120 | 96, 97, 118, 119 | syl3anbrc 1192 |
. . . . . . . . . . 11
 
      
   ..^   |
121 | | fveq2 5865 |
. . . . . . . . . . . . 13
          
    |
122 | 121 | breq1d 4412 |
. . . . . . . . . . . 12
       
         |
123 | 122 | elrab 3196 |
. . . . . . . . . . 11
     ..^          ..^          |
124 | 120, 104,
123 | sylanbrc 670 |
. . . . . . . . . 10
 
      
    ..^    
   |
125 | | suprzub 11255 |
. . . . . . . . . 10
    ..^    
     ..^    
 

   ..^        
    ..^    
     |
126 | 83, 93, 124, 125 | syl3anc 1268 |
. . . . . . . . 9
 
      
      ..^      
   |
127 | 126, 1 | syl6breqr 4443 |
. . . . . . . 8
 
      
    |
128 | 80, 127 | mtand 665 |
. . . . . . 7
    
    |
129 | | eqcom 2458 |
. . . . . . . . . . 11
      
        |
130 | 129 | biimpi 198 |
. . . . . . . . . 10
          
    |
131 | 130 | adantl 468 |
. . . . . . . . 9
 
      
        |
132 | 35 | adantr 467 |
. . . . . . . . . 10
 
      
      |
133 | 65 | adantr 467 |
. . . . . . . . . 10
 
      
        |
134 | | fnfvelrn 6019 |
. . . . . . . . . 10
      
         
    |
135 | 132, 133,
134 | syl2anc 667 |
. . . . . . . . 9
 
      
        |
136 | 131, 135 | eqeltrd 2529 |
. . . . . . . 8
 
      
  |
137 | 32, 136 | mtand 665 |
. . . . . . 7
    
    |
138 | 128, 137 | jca 535 |
. . . . . 6
       
         |
139 | | pm4.56 498 |
. . . . . 6
     
     
  
                |
140 | 138, 139 | sylib 200 |
. . . . 5
                 |
141 | 66, 27 | leloed 9778 |
. . . . 5
     
                   |
142 | 140, 141 | mtbird 303 |
. . . 4
    
    |
143 | 27, 66 | ltnled 9782 |
. . . 4
             
   |
144 | 142, 143 | mpbird 236 |
. . 3
         |
145 | 63, 67, 27, 73, 144 | eliood 37595 |
. 2
           
     |
146 | | fveq2 5865 |
. . . . 5
           |
147 | | oveq1 6297 |
. . . . . 6
       |
148 | 147 | fveq2d 5869 |
. . . . 5
          
    |
149 | 146, 148 | oveq12d 6308 |
. . . 4
                               |
150 | 149 | eleq2d 2514 |
. . 3
 
             
                 |
151 | 150 | rspcev 3150 |
. 2
   ..^                  ..^                  |
152 | 60, 145, 151 | syl2anc 667 |
1
   ..^                  |