Step | Hyp | Ref
| Expression |
1 | | fourierdlem25.i |
. . 3
    ..^         |
2 | | ssrab2 3500 |
. . . 4
  ..^       ..^  |
3 | | ltso 9732 |
. . . . . 6
 |
4 | 3 | a1i 11 |
. . . . 5
   |
5 | | fzofi 12225 |
. . . . . . 7
 ..^  |
6 | | ssfi 7810 |
. . . . . . 7
   ..^   ..^       ..^    ..^     
  |
7 | 5, 2, 6 | mp2an 686 |
. . . . . 6
  ..^       |
8 | 7 | a1i 11 |
. . . . 5
   ..^    
   |
9 | | 0zd 10973 |
. . . . . . . 8
   |
10 | | fourierdlem25.m |
. . . . . . . . 9
   |
11 | 10 | nnzd 11062 |
. . . . . . . 8
   |
12 | 10 | nngt0d 10675 |
. . . . . . . 8
   |
13 | | fzolb 11953 |
. . . . . . . 8
  ..^     |
14 | 9, 11, 12, 13 | syl3anbrc 1214 |
. . . . . . 7
  ..^   |
15 | | fourierdlem25.qf |
. . . . . . . . 9
           |
16 | | elfzofz 11962 |
. . . . . . . . . 10
  ..^
      |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
       |
18 | 15, 17 | ffvelrnd 6038 |
. . . . . . . 8
       |
19 | 10 | nnnn0d 10949 |
. . . . . . . . . . . . 13
   |
20 | | nn0uz 11217 |
. . . . . . . . . . . . 13
     |
21 | 19, 20 | syl6eleq 2559 |
. . . . . . . . . . . 12
       |
22 | | eluzfz2 11833 |
. . . . . . . . . . . 12
    
      |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
       |
24 | 15, 23 | ffvelrnd 6038 |
. . . . . . . . . 10
       |
25 | 18, 24 | iccssred 37698 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)     
  |
26 | | fourierdlem25.cel |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)        |
27 | 25, 26 | sseldd 3419 |
. . . . . . . 8
   |
28 | 18 | rexrd 9708 |
. . . . . . . . 9
       |
29 | 24 | rexrd 9708 |
. . . . . . . . 9
       |
30 | | iccgelb 11716 |
. . . . . . . . 9
                ![[,] [,]](_icc.gif)             |
31 | 28, 29, 26, 30 | syl3anc 1292 |
. . . . . . . 8
    
  |
32 | | fourierdlem25.cnel |
. . . . . . . . . 10
   |
33 | | simpr 468 |
. . . . . . . . . . 11
 
    
      |
34 | | ffn 5739 |
. . . . . . . . . . . . . 14
               |
35 | 15, 34 | syl 17 |
. . . . . . . . . . . . 13
       |
36 | 35 | adantr 472 |
. . . . . . . . . . . 12
 
    
      |
37 | 17 | adantr 472 |
. . . . . . . . . . . 12
 
    
      |
38 | | fnfvelrn 6034 |
. . . . . . . . . . . 12
     
           |
39 | 36, 37, 38 | syl2anc 673 |
. . . . . . . . . . 11
 
    
      |
40 | 33, 39 | eqeltrd 2549 |
. . . . . . . . . 10
 
    
  |
41 | 32, 40 | mtand 671 |
. . . . . . . . 9
       |
42 | 41 | neqned 2650 |
. . . . . . . 8
       |
43 | 18, 27, 31, 42 | leneltd 9806 |
. . . . . . 7
    
  |
44 | | fveq2 5879 |
. . . . . . . . 9
           |
45 | 44 | breq1d 4405 |
. . . . . . . 8
     
       |
46 | 45 | elrab 3184 |
. . . . . . 7
   ..^        ..^        |
47 | 14, 43, 46 | sylanbrc 677 |
. . . . . 6
   ..^        |
48 | | ne0i 3728 |
. . . . . 6
   ..^        ..^        |
49 | 47, 48 | syl 17 |
. . . . 5
   ..^    
   |
50 | | fzossfz 11965 |
. . . . . . . 8
 ..^      |
51 | | fzssz 11827 |
. . . . . . . . 9
     |
52 | | zssre 10968 |
. . . . . . . . 9
 |
53 | 51, 52 | sstri 3427 |
. . . . . . . 8
     |
54 | 50, 53 | sstri 3427 |
. . . . . . 7
 ..^  |
55 | 2, 54 | sstri 3427 |
. . . . . 6
  ..^       |
56 | 55 | a1i 11 |
. . . . 5
   ..^    
   |
57 | | fisupcl 8003 |
. . . . 5
    ..^    
   ..^        ..^            ..^    
     ..^    
   |
58 | 4, 8, 49, 56, 57 | syl13anc 1294 |
. . . 4
     ..^          ..^        |
59 | 2, 58 | sseldi 3416 |
. . 3
     ..^         ..^   |
60 | 1, 59 | syl5eqel 2553 |
. 2
  ..^   |
61 | 50, 60 | sseldi 3416 |
. . . . 5
       |
62 | 15, 61 | ffvelrnd 6038 |
. . . 4
       |
63 | 62 | rexrd 9708 |
. . 3
       |
64 | | fzofzp1 12037 |
. . . . . 6
  ..^
        |
65 | 60, 64 | syl 17 |
. . . . 5
         |
66 | 15, 65 | ffvelrnd 6038 |
. . . 4
         |
67 | 66 | rexrd 9708 |
. . 3
         |
68 | 1, 58 | syl5eqel 2553 |
. . . . 5
   ..^        |
69 | | fveq2 5879 |
. . . . . . 7
           |
70 | 69 | breq1d 4405 |
. . . . . 6
     
       |
71 | 70 | elrab 3184 |
. . . . 5
   ..^        ..^        |
72 | 68, 71 | sylib 201 |
. . . 4
   ..^        |
73 | 72 | simprd 470 |
. . 3
    
  |
74 | 54, 60 | sseldi 3416 |
. . . . . . . . 9
   |
75 | | ltp1 10465 |
. . . . . . . . . 10
     |
76 | | id 22 |
. . . . . . . . . . 11
   |
77 | | peano2re 9824 |
. . . . . . . . . . 11
     |
78 | 76, 77 | ltnled 9799 |
. . . . . . . . . 10
 
 
     |
79 | 75, 78 | mpbid 215 |
. . . . . . . . 9
 

  |
80 | 74, 79 | syl 17 |
. . . . . . . 8
     |
81 | 50, 51 | sstri 3427 |
. . . . . . . . . . . 12
 ..^  |
82 | 2, 81 | sstri 3427 |
. . . . . . . . . . 11
  ..^       |
83 | 82 | a1i 11 |
. . . . . . . . . 10
 
      
  ..^        |
84 | | elrabi 3181 |
. . . . . . . . . . . . . . 15
   ..^       ..^   |
85 | | elfzo0le 11987 |
. . . . . . . . . . . . . . 15
  ..^
  |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . 14
   ..^        |
87 | 86 | adantl 473 |
. . . . . . . . . . . . 13
 
  ..^         |
88 | 87 | ralrimiva 2809 |
. . . . . . . . . . . 12
    ..^         |
89 | | breq2 4399 |
. . . . . . . . . . . . . 14
 
   |
90 | 89 | ralbidv 2829 |
. . . . . . . . . . . . 13
  
  ..^          ..^          |
91 | 90 | rspcev 3136 |
. . . . . . . . . . . 12
     ..^            ..^    
 
  |
92 | 11, 88, 91 | syl2anc 673 |
. . . . . . . . . . 11
     ..^         |
93 | 92 | adantr 472 |
. . . . . . . . . 10
 
      
    ..^    
 
  |
94 | | elfzuz 11822 |
. . . . . . . . . . . . . 14
               |
95 | 65, 94 | syl 17 |
. . . . . . . . . . . . 13
         |
96 | 95 | adantr 472 |
. . . . . . . . . . . 12
 
      
        |
97 | 11 | adantr 472 |
. . . . . . . . . . . 12
 
      
  |
98 | 53, 65 | sseldi 3416 |
. . . . . . . . . . . . . 14
     |
99 | 98 | adantr 472 |
. . . . . . . . . . . . 13
 
      
    |
100 | 97 | zred 11063 |
. . . . . . . . . . . . 13
 
      
  |
101 | | elfzle2 11829 |
. . . . . . . . . . . . . . 15
           |
102 | 65, 101 | syl 17 |
. . . . . . . . . . . . . 14
  
  |
103 | 102 | adantr 472 |
. . . . . . . . . . . . 13
 
      
    |
104 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 
      
        |
105 | 66 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
      
        |
106 | 27 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
      
  |
107 | 105, 106 | ltnled 9799 |
. . . . . . . . . . . . . . . 16
 
      
      
         |
108 | 104, 107 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
      
        |
109 | | iccleub 11715 |
. . . . . . . . . . . . . . . . . . 19
                ![[,] [,]](_icc.gif)             |
110 | 28, 29, 26, 109 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18

      |
111 | 110 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 

        |
112 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
          
    |
113 | 112 | adantl 473 |
. . . . . . . . . . . . . . . . 17
 

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

          |
115 | 114 | adantlr 729 |
. . . . . . . . . . . . . . 15
         
           |
116 | 108, 115 | mtand 671 |
. . . . . . . . . . . . . 14
 
      
    |
117 | 116 | neqned 2650 |
. . . . . . . . . . . . 13
 
      

   |
118 | 99, 100, 103, 117 | leneltd 9806 |
. . . . . . . . . . . 12
 
      
    |
119 | | elfzo2 11950 |
. . . . . . . . . . . 12
    ..^       
     |
120 | 96, 97, 118, 119 | syl3anbrc 1214 |
. . . . . . . . . . 11
 
      
   ..^   |
121 | | fveq2 5879 |
. . . . . . . . . . . . 13
          
    |
122 | 121 | breq1d 4405 |
. . . . . . . . . . . 12
       
         |
123 | 122 | elrab 3184 |
. . . . . . . . . . 11
     ..^          ..^          |
124 | 120, 104,
123 | sylanbrc 677 |
. . . . . . . . . 10
 
      
    ..^    
   |
125 | | suprzub 11278 |
. . . . . . . . . 10
    ..^    
     ..^    
 

   ..^        
    ..^    
     |
126 | 83, 93, 124, 125 | syl3anc 1292 |
. . . . . . . . 9
 
      
      ..^      
   |
127 | 126, 1 | syl6breqr 4436 |
. . . . . . . 8
 
      
    |
128 | 80, 127 | mtand 671 |
. . . . . . 7
    
    |
129 | | eqcom 2478 |
. . . . . . . . . . 11
      
        |
130 | 129 | biimpi 199 |
. . . . . . . . . 10
          
    |
131 | 130 | adantl 473 |
. . . . . . . . 9
 
      
        |
132 | 35 | adantr 472 |
. . . . . . . . . 10
 
      
      |
133 | 65 | adantr 472 |
. . . . . . . . . 10
 
      
        |
134 | | fnfvelrn 6034 |
. . . . . . . . . 10
      
         
    |
135 | 132, 133,
134 | syl2anc 673 |
. . . . . . . . 9
 
      
        |
136 | 131, 135 | eqeltrd 2549 |
. . . . . . . 8
 
      
  |
137 | 32, 136 | mtand 671 |
. . . . . . 7
    
    |
138 | 128, 137 | jca 541 |
. . . . . 6
       
         |
139 | | pm4.56 503 |
. . . . . 6
     
     
  
                |
140 | 138, 139 | sylib 201 |
. . . . 5
                 |
141 | 66, 27 | leloed 9795 |
. . . . 5
     
                   |
142 | 140, 141 | mtbird 308 |
. . . 4
    
    |
143 | 27, 66 | ltnled 9799 |
. . . 4
             
   |
144 | 142, 143 | mpbird 240 |
. . 3
         |
145 | 63, 67, 27, 73, 144 | eliood 37691 |
. 2
           
     |
146 | | fveq2 5879 |
. . . . 5
           |
147 | | oveq1 6315 |
. . . . . 6
       |
148 | 147 | fveq2d 5883 |
. . . . 5
          
    |
149 | 146, 148 | oveq12d 6326 |
. . . 4
                               |
150 | 149 | eleq2d 2534 |
. . 3
 
             
                 |
151 | 150 | rspcev 3136 |
. 2
   ..^                  ..^                  |
152 | 60, 145, 151 | syl2anc 673 |
1
   ..^                  |