Step | Hyp | Ref
| Expression |
1 | | fourierdlem52.tf |
. . . . 5
   |
2 | | fourierdlem52.t |
. . . . . 6

  ![[,] [,]](_icc.gif)    |
3 | | fourierdlem52.a |
. . . . . . 7
   |
4 | | fourierdlem52.b |
. . . . . . 7
   |
5 | 3, 4 | iccssred 37602 |
. . . . . 6
   ![[,] [,]](_icc.gif) 
  |
6 | 2, 5 | sstrd 3442 |
. . . . 5

  |
7 | | fourierdlem52.s |
. . . . 5
            |
8 | | fourierdlem52.n |
. . . . 5
       |
9 | 1, 6, 7, 8 | fourierdlem36 38006 |
. . . 4

         |
10 | | isof1o 6216 |
. . . 4
                  |
11 | | f1of 5814 |
. . . 4
        
          |
12 | 9, 10, 11 | 3syl 18 |
. . 3
           |
13 | 12, 2 | fssd 5738 |
. 2
           ![[,] [,]](_icc.gif)    |
14 | | f1ofo 5821 |
. . . . . 6
        
          |
15 | 9, 10, 14 | 3syl 18 |
. . . . 5
           |
16 | | fourierdlem52.at |
. . . . 5
   |
17 | | foelrn 6041 |
. . . . 5
          
            |
18 | 15, 16, 17 | syl2anc 667 |
. . . 4
             |
19 | | elfzle1 11802 |
. . . . . . . . 9
       |
20 | 19 | adantl 468 |
. . . . . . . 8
 
       |
21 | 9 | adantr 467 |
. . . . . . . . 9
 
              |
22 | | ressxr 9684 |
. . . . . . . . . . . 12
 |
23 | 6, 22 | syl6ss 3444 |
. . . . . . . . . . 11

  |
24 | 23 | adantr 467 |
. . . . . . . . . 10
 
       |
25 | | fzssz 11801 |
. . . . . . . . . . 11
     |
26 | | zssre 10944 |
. . . . . . . . . . . 12
 |
27 | 26, 22 | sstri 3441 |
. . . . . . . . . . 11
 |
28 | 25, 27 | sstri 3441 |
. . . . . . . . . 10
     |
29 | 24, 28 | jctil 540 |
. . . . . . . . 9
 
         
   |
30 | | hashcl 12538 |
. . . . . . . . . . . . . . . 16
       |
31 | 1, 30 | syl 17 |
. . . . . . . . . . . . . . 15
       |
32 | | ne0i 3737 |
. . . . . . . . . . . . . . . . 17
   |
33 | 16, 32 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
34 | | hashge1 12568 |
. . . . . . . . . . . . . . . 16
         |
35 | 1, 33, 34 | syl2anc 667 |
. . . . . . . . . . . . . . 15

      |
36 | | elnnnn0c 10915 |
. . . . . . . . . . . . . . 15
         
       |
37 | 31, 35, 36 | sylanbrc 670 |
. . . . . . . . . . . . . 14
       |
38 | | nnm1nn0 10911 |
. . . . . . . . . . . . . 14
    
        |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
         |
40 | 8, 39 | syl5eqel 2533 |
. . . . . . . . . . . 12
   |
41 | | nn0uz 11193 |
. . . . . . . . . . . 12
     |
42 | 40, 41 | syl6eleq 2539 |
. . . . . . . . . . 11
       |
43 | | eluzfz1 11806 |
. . . . . . . . . . 11
    
      |
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
       |
45 | 44 | anim1i 572 |
. . . . . . . . 9
 
         
       |
46 | | leisorel 12623 |
. . . . . . . . 9
 
                        
           |
47 | 21, 29, 45, 46 | syl3anc 1268 |
. . . . . . . 8
 
     
           |
48 | 20, 47 | mpbid 214 |
. . . . . . 7
 
               |
49 | 48 | 3adant3 1028 |
. . . . . 6
 
   
    
          |
50 | | eqcom 2458 |
. . . . . . . 8
    
      |
51 | 50 | biimpi 198 |
. . . . . . 7
           |
52 | 51 | 3ad2ant3 1031 |
. . . . . 6
 
   
    
      |
53 | 49, 52 | breqtrd 4427 |
. . . . 5
 
   
    
      |
54 | 53 | rexlimdv3a 2881 |
. . . 4
                   |
55 | 18, 54 | mpd 15 |
. . 3
    
  |
56 | 3 | rexrd 9690 |
. . . 4
   |
57 | 4 | rexrd 9690 |
. . . 4
   |
58 | 13, 44 | ffvelrnd 6023 |
. . . 4
       ![[,] [,]](_icc.gif)    |
59 | | iccgelb 11691 |
. . . 4
        ![[,] [,]](_icc.gif)         |
60 | 56, 57, 58, 59 | syl3anc 1268 |
. . 3

      |
61 | 5, 58 | sseldd 3433 |
. . . 4
       |
62 | 61, 3 | letri3d 9777 |
. . 3
          
        |
63 | 55, 60, 62 | mpbir2and 933 |
. 2
       |
64 | | eluzfz2 11807 |
. . . . . 6
    
      |
65 | 42, 64 | syl 17 |
. . . . 5
       |
66 | 13, 65 | ffvelrnd 6023 |
. . . 4
       ![[,] [,]](_icc.gif)    |
67 | | iccleub 11690 |
. . . 4
        ![[,] [,]](_icc.gif)         |
68 | 56, 57, 66, 67 | syl3anc 1268 |
. . 3
    
  |
69 | | fourierdlem52.bt |
. . . . 5
   |
70 | | foelrn 6041 |
. . . . 5
          
            |
71 | 15, 69, 70 | syl2anc 667 |
. . . 4
             |
72 | | simp3 1010 |
. . . . . 6
 
   
    
      |
73 | | elfzle2 11803 |
. . . . . . . 8
       |
74 | 73 | 3ad2ant2 1030 |
. . . . . . 7
 
   
    
  |
75 | 9 | 3ad2ant1 1029 |
. . . . . . . 8
 
   
    
         |
76 | 29 | 3adant3 1028 |
. . . . . . . 8
 
   
    
        |
77 | | simp2 1009 |
. . . . . . . 8
 
   
    
      |
78 | 65 | 3ad2ant1 1029 |
. . . . . . . 8
 
   
    
      |
79 | | leisorel 12623 |
. . . . . . . 8
 
                        
           |
80 | 75, 76, 77, 78, 79 | syl112anc 1272 |
. . . . . . 7
 
   
    
            |
81 | 74, 80 | mpbid 214 |
. . . . . 6
 
   
    
          |
82 | 72, 81 | eqbrtrd 4423 |
. . . . 5
 
   
    
      |
83 | 82 | rexlimdv3a 2881 |
. . . 4
                   |
84 | 71, 83 | mpd 15 |
. . 3

      |
85 | 5, 66 | sseldd 3433 |
. . . 4
       |
86 | 85, 4 | letri3d 9777 |
. . 3
          
        |
87 | 68, 84, 86 | mpbir2and 933 |
. 2
       |
88 | 13, 63, 87 | jca31 537 |
1
             ![[,] [,]](_icc.gif)              |