Proof of Theorem fourierdlem37
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3514 |
. . . 4
  ..^               ..^  |
2 | | ltso 9714 |
. . . . . 6
 |
3 | 2 | a1i 11 |
. . . . 5
 

  |
4 | | fzfi 12185 |
. . . . . . 7
     |
5 | | fzossfz 11938 |
. . . . . . . 8
 ..^      |
6 | 1, 5 | sstri 3441 |
. . . . . . 7
  ..^                   |
7 | | ssfi 7792 |
. . . . . . 7
        ..^                     ..^                |
8 | 4, 6, 7 | mp2an 678 |
. . . . . 6
  ..^               |
9 | 8 | a1i 11 |
. . . . 5
 

  ..^                |
10 | | 0zd 10949 |
. . . . . . . . 9
   |
11 | | fourierdlem37.m |
. . . . . . . . . 10
   |
12 | 11 | nnzd 11039 |
. . . . . . . . 9
   |
13 | 11 | nngt0d 10653 |
. . . . . . . . 9
   |
14 | | fzolb 11926 |
. . . . . . . . 9
  ..^     |
15 | 10, 12, 13, 14 | syl3anbrc 1192 |
. . . . . . . 8
  ..^   |
16 | 15 | adantr 467 |
. . . . . . 7
 

 ..^   |
17 | | fourierdlem37.q |
. . . . . . . . . . . . . . . 16
       |
18 | | fourierdlem37.p |
. . . . . . . . . . . . . . . . . 18
 
                 
 ..^                |
19 | 18 | fourierdlem2 37971 |
. . . . . . . . . . . . . . . . 17
 
   
                  
 ..^                 |
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
                        
 ..^                 |
21 | 17, 20 | mpbid 214 |
. . . . . . . . . . . . . . 15
                   
 ..^                |
22 | 21 | simprd 465 |
. . . . . . . . . . . . . 14
            
 ..^               |
23 | 22 | simplld 761 |
. . . . . . . . . . . . 13
       |
24 | 18, 11, 17 | fourierdlem11 37980 |
. . . . . . . . . . . . . 14
     |
25 | 24 | simp1d 1020 |
. . . . . . . . . . . . 13
   |
26 | 23, 25 | eqeltrd 2529 |
. . . . . . . . . . . 12
       |
27 | 26, 23 | eqled 9737 |
. . . . . . . . . . 11
    
  |
28 | 27 | ad2antrr 732 |
. . . . . . . . . 10
               |
29 | | iftrue 3887 |
. . . . . . . . . . . 12
                    |
30 | 29 | eqcomd 2457 |
. . . . . . . . . . 11
                    |
31 | 30 | adantl 468 |
. . . . . . . . . 10
                        |
32 | 28, 31 | breqtrd 4427 |
. . . . . . . . 9
                            |
33 | 26 | adantr 467 |
. . . . . . . . . . . 12
 

      |
34 | 25 | adantr 467 |
. . . . . . . . . . . . . . 15
 

  |
35 | 34 | rexrd 9690 |
. . . . . . . . . . . . . 14
 

  |
36 | 24 | simp2d 1021 |
. . . . . . . . . . . . . . 15
   |
37 | 36 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
38 | | iocssre 11714 |
. . . . . . . . . . . . . 14
     ![(,] (,]](_ioc.gif)    |
39 | 35, 37, 38 | syl2anc 667 |
. . . . . . . . . . . . 13
 

  ![(,] (,]](_ioc.gif)    |
40 | 24 | simp3d 1022 |
. . . . . . . . . . . . . . 15
   |
41 | | fourierdlem37.t |
. . . . . . . . . . . . . . 15
   |
42 | | fourierdlem37.e |
. . . . . . . . . . . . . . 15
 
             |
43 | 25, 36, 40, 41, 42 | fourierdlem4 37973 |
. . . . . . . . . . . . . 14
       ![(,] (,]](_ioc.gif)    |
44 | 43 | fnvinran 37335 |
. . . . . . . . . . . . 13
 

      ![(,] (,]](_ioc.gif)    |
45 | 39, 44 | sseldd 3433 |
. . . . . . . . . . . 12
 

      |
46 | 23 | adantr 467 |
. . . . . . . . . . . . 13
 

      |
47 | | elioc2 11697 |
. . . . . . . . . . . . . . . 16
          ![(,] (,]](_ioc.gif) 
        
        |
48 | 35, 37, 47 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 

       ![(,] (,]](_ioc.gif) 
        
        |
49 | 44, 48 | mpbid 214 |
. . . . . . . . . . . . . 14
 

        
       |
50 | 49 | simp2d 1021 |
. . . . . . . . . . . . 13
 

      |
51 | 46, 50 | eqbrtrd 4423 |
. . . . . . . . . . . 12
 

          |
52 | 33, 45, 51 | ltled 9783 |
. . . . . . . . . . 11
 

          |
53 | 52 | adantr 467 |
. . . . . . . . . 10
            
      |
54 | | iffalse 3890 |
. . . . . . . . . . . 12
                        |
55 | 54 | eqcomd 2457 |
. . . . . . . . . . 11
                
       |
56 | 55 | adantl 468 |
. . . . . . . . . 10
                    
       |
57 | 53, 56 | breqtrd 4427 |
. . . . . . . . 9
            
       
       |
58 | 32, 57 | pm2.61dan 800 |
. . . . . . . 8
 

                   |
59 | | fourierdlem37.l |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)         |
60 | 59 | a1i 11 |
. . . . . . . . 9
 

   ![(,] (,]](_ioc.gif)          |
61 | | eqeq1 2455 |
. . . . . . . . . . 11
     
       |
62 | | id 22 |
. . . . . . . . . . 11
           |
63 | 61, 62 | ifbieq2d 3906 |
. . . . . . . . . 10
                 
       |
64 | 63 | adantl 468 |
. . . . . . . . 9
                     
       |
65 | 34, 45 | ifcld 3924 |
. . . . . . . . 9
 

       
       |
66 | 60, 64, 44, 65 | fvmptd 5954 |
. . . . . . . 8
 

                       |
67 | 58, 66 | breqtrrd 4429 |
. . . . . . 7
 

              |
68 | | fveq2 5865 |
. . . . . . . . 9
           |
69 | 68 | breq1d 4412 |
. . . . . . . 8
     
       
               |
70 | 69 | elrab 3196 |
. . . . . . 7
   ..^                ..^                |
71 | 16, 67, 70 | sylanbrc 670 |
. . . . . 6
 

  ..^    
           |
72 | | ne0i 3737 |
. . . . . 6
   ..^                ..^                |
73 | 71, 72 | syl 17 |
. . . . 5
 

  ..^                |
74 | | fzssz 11801 |
. . . . . . . . 9
     |
75 | 5, 74 | sstri 3441 |
. . . . . . . 8
 ..^  |
76 | | zssre 10944 |
. . . . . . . 8
 |
77 | 75, 76 | sstri 3441 |
. . . . . . 7
 ..^  |
78 | 1, 77 | sstri 3441 |
. . . . . 6
  ..^               |
79 | 78 | a1i 11 |
. . . . 5
 

  ..^                |
80 | | fisupcl 7985 |
. . . . 5
    ..^    
           ..^                ..^                    ..^    
          
  ..^    
           |
81 | 3, 9, 73, 79, 80 | syl13anc 1270 |
. . . 4
 

    ..^    
          
  ..^    
           |
82 | 1, 81 | sseldi 3430 |
. . 3
 

    ..^    
          
 ..^   |
83 | | fourierdlem37.i |
. . 3
     ..^                  |
84 | 82, 83 | fmptd 6046 |
. 2
      ..^   |
85 | 81 | ex 436 |
. 2
      ..^                  ..^                 |
86 | 84, 85 | jca 535 |
1
       ..^ 
    ..^                  ..^                  |