Proof of Theorem itgsinexp
Step | Hyp | Ref
| Expression |
1 | | itgsinexp.2 |
. . . . . . . 8
       |
2 | | eluzelz 11192 |
. . . . . . . 8
    
  |
3 | | zcn 10966 |
. . . . . . . 8
   |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
   |
5 | | 1cnd 9677 |
. . . . . . 7
   |
6 | 4, 5 | npcand 10009 |
. . . . . 6
       |
7 | 6 | eqcomd 2477 |
. . . . 5
       |
8 | 7 | oveq1d 6323 |
. . . 4
                   |
9 | | uz2m1nn 11256 |
. . . . . . 7
    
    |
10 | 1, 9 | syl 17 |
. . . . . 6
     |
11 | 10 | nncnd 10647 |
. . . . 5
     |
12 | | itgsinexp.1 |
. . . . . . . 8
                  |
13 | 12 | a1i 11 |
. . . . . . 7
 
                  |
14 | | oveq2 6316 |
. . . . . . . . 9
                   |
15 | 14 | ad2antlr 741 |
. . . . . . . 8
                           |
16 | 15 | itgeq2dv 22818 |
. . . . . . 7
 
                                 |
17 | | 2cnd 10704 |
. . . . . . . . 9
   |
18 | | npcan 9904 |
. . . . . . . . . 10
 
       |
19 | 18 | eqcomd 2477 |
. . . . . . . . 9
 
       |
20 | 4, 17, 19 | syl2anc 673 |
. . . . . . . 8
       |
21 | | uznn0sub 11214 |
. . . . . . . . . 10
    
    |
22 | 1, 21 | syl 17 |
. . . . . . . . 9
     |
23 | | 2nn0 10910 |
. . . . . . . . . 10
 |
24 | 23 | a1i 11 |
. . . . . . . . 9
   |
25 | 22, 24 | nn0addcld 10953 |
. . . . . . . 8
       |
26 | 20, 25 | eqeltrd 2549 |
. . . . . . 7
   |
27 | | itgex 22807 |
. . . . . . . 8
                |
28 | 27 | a1i 11 |
. . . . . . 7
                  |
29 | 13, 16, 26, 28 | fvmptd 5969 |
. . . . . 6
                      |
30 | | ioosscn 37687 |
. . . . . . . . . . 11
     |
31 | 30 | sseli 3414 |
. . . . . . . . . 10
       |
32 | 31 | sincld 14261 |
. . . . . . . . 9
           |
33 | 32 | adantl 473 |
. . . . . . . 8
 
           |
34 | 26 | adantr 472 |
. . . . . . . 8
 
       |
35 | 33, 34 | expcld 12454 |
. . . . . . 7
 
               |
36 | | ioossicc 11745 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)   |
37 | 36 | a1i 11 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)    |
38 | | ioombl 22597 |
. . . . . . . . 9
     |
39 | 38 | a1i 11 |
. . . . . . . 8
    
  |
40 | | 0re 9661 |
. . . . . . . . . . . . . 14
 |
41 | | pire 23492 |
. . . . . . . . . . . . . 14
 |
42 | | iccssre 11741 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)    |
43 | 40, 41, 42 | mp2an 686 |
. . . . . . . . . . . . 13
  ![[,] [,]](_icc.gif)   |
44 | | ax-resscn 9614 |
. . . . . . . . . . . . 13
 |
45 | 43, 44 | sstri 3427 |
. . . . . . . . . . . 12
  ![[,] [,]](_icc.gif)   |
46 | 45 | sseli 3414 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
47 | 46 | sincld 14261 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)        |
48 | 47 | adantl 473 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)         |
49 | 26 | adantr 472 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)     |
50 | 48, 49 | expcld 12454 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)             |
51 | 40 | a1i 11 |
. . . . . . . . 9
   |
52 | 41 | a1i 11 |
. . . . . . . . 9
   |
53 | 46 | adantl 473 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)     |
54 | | eqid 2471 |
. . . . . . . . . . . . . 14
                     |
55 | 54 | fvmpt2 5972 |
. . . . . . . . . . . . 13
                                   |
56 | 53, 50, 55 | syl2anc 673 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                           |
57 | 56 | eqcomd 2477 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                           |
58 | 57 | mpteq2dva 4482 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)                   |
59 | | nfmpt1 4485 |
. . . . . . . . . . 11
             |
60 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
61 | | sincn 23478 |
. . . . . . . . . . . . 13
     |
62 | 61 | a1i 11 |
. . . . . . . . . . . 12
       |
63 | 60, 62, 26 | expcnfg 37768 |
. . . . . . . . . . 11
                 |
64 | 45 | a1i 11 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
65 | 59, 63, 64 | cncfmptss 37762 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)       |
66 | 58, 65 | eqeltrd 2549 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
67 | | cniccibl 22877 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)              |
68 | 51, 52, 66, 67 | syl3anc 1292 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              |
69 | 37, 39, 50, 68 | iblss 22841 |
. . . . . . 7
                  |
70 | 35, 69 | itgcl 22820 |
. . . . . 6
                  |
71 | 29, 70 | eqeltrd 2549 |
. . . . 5
       |
72 | 11, 71 | adddirp1d 37598 |
. . . 4
                           |
73 | | eluz2b2 11254 |
. . . . . . . . . . . 12
         |
74 | 1, 73 | sylib 201 |
. . . . . . . . . . 11
     |
75 | 74 | simpld 466 |
. . . . . . . . . 10
   |
76 | | expm1t 12338 |
. . . . . . . . . 10
     
                           |
77 | 32, 75, 76 | syl2anr 486 |
. . . . . . . . 9
 
                               |
78 | 77 | itgeq2dv 22818 |
. . . . . . . 8
                              
          |
79 | | eqid 2471 |
. . . . . . . . . 10
                    
    |
80 | | eqid 2471 |
. . . . . . . . . 10
               |
81 | | eqid 2471 |
. . . . . . . . . 10
                                                 |
82 | | eqid 2471 |
. . . . . . . . . 10
                           
         |
83 | | eqid 2471 |
. . . . . . . . . 10
                                                               |
84 | | eqid 2471 |
. . . . . . . . . 10
                                                 |
85 | 79, 80, 81, 82, 83, 84, 10 | itgsinexplem1 37927 |
. . . . . . . . 9
                                                           |
86 | 4, 5, 5 | subsub4d 10036 |
. . . . . . . . . . . . . . 15
           |
87 | | 1p1e2 10745 |
. . . . . . . . . . . . . . . . 17
   |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
     |
89 | 88 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
         |
90 | 86, 89 | eqtrd 2505 |
. . . . . . . . . . . . . 14
         |
91 | 90 | adantr 472 |
. . . . . . . . . . . . 13
 
             |
92 | 91 | oveq2d 6324 |
. . . . . . . . . . . 12
 
                        
    |
93 | 92 | oveq2d 6324 |
. . . . . . . . . . 11
 
                                           
     |
94 | 93 | itgeq2dv 22818 |
. . . . . . . . . 10
                                                    
      |
95 | 94 | oveq2d 6324 |
. . . . . . . . 9
                                                           
       |
96 | | sincossq 14307 |
. . . . . . . . . . . . . . . . 17
                     |
97 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . 18
   |
98 | | sincl 14257 |
. . . . . . . . . . . . . . . . . . 19
       |
99 | 98 | sqcld 12452 |
. . . . . . . . . . . . . . . . . 18
           |
100 | | coscl 14258 |
. . . . . . . . . . . . . . . . . . 19
       |
101 | 100 | sqcld 12452 |
. . . . . . . . . . . . . . . . . 18
           |
102 | 97, 99, 101 | subaddd 10023 |
. . . . . . . . . . . . . . . . 17
                   
                     |
103 | 96, 102 | mpbird 240 |
. . . . . . . . . . . . . . . 16
                     |
104 | 103 | eqcomd 2477 |
. . . . . . . . . . . . . . 15
                     |
105 | 31, 104 | syl 17 |
. . . . . . . . . . . . . 14
                         |
106 | 105 | oveq1d 6323 |
. . . . . . . . . . . . 13
                     
                           |
107 | 106 | adantl 473 |
. . . . . . . . . . . 12
 
                     
                           |
108 | 107 | itgeq2dv 22818 |
. . . . . . . . . . 11
                       
                                   |
109 | | 1cnd 9677 |
. . . . . . . . . . . . . 14
 
       |
110 | 32 | sqcld 12452 |
. . . . . . . . . . . . . . 15
               |
111 | 110 | adantl 473 |
. . . . . . . . . . . . . 14
 
               |
112 | 90 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
         |
113 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . . . . 18
         |
114 | 10, 113 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
115 | 112, 114 | eqeltrd 2549 |
. . . . . . . . . . . . . . . 16
     |
116 | 115 | adantr 472 |
. . . . . . . . . . . . . . 15
 
     
   |
117 | 33, 116 | expcld 12454 |
. . . . . . . . . . . . . 14
 
                 |
118 | 109, 111,
117 | subdird 10096 |
. . . . . . . . . . . . 13
 
                                    
                   
      |
119 | 117 | mulid2d 9679 |
. . . . . . . . . . . . . 14
 
                        
    |
120 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
       |
121 | 33, 116, 120 | expaddd 12456 |
. . . . . . . . . . . . . . 15
 
                                       |
122 | 17, 4 | pncan3d 10008 |
. . . . . . . . . . . . . . . . 17
       |
123 | 122 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                       |
124 | 123 | adantr 472 |
. . . . . . . . . . . . . . 15
 
                           |
125 | 121, 124 | eqtr3d 2507 |
. . . . . . . . . . . . . 14
 
                     
             |
126 | 119, 125 | oveq12d 6326 |
. . . . . . . . . . . . 13
 
                                  
            
             |
127 | 118, 126 | eqtrd 2505 |
. . . . . . . . . . . 12
 
                                                 |
128 | 127 | itgeq2dv 22818 |
. . . . . . . . . . 11
                         
                                 |
129 | 115 | adantr 472 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)   
   |
130 | 48, 129 | expcld 12454 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)               |
131 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
                    
    |
132 | 131 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . 18
                      
                  |
133 | 53, 130, 132 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)                          
    |
134 | 133 | eqcomd 2477 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)                               |
135 | 134 | mpteq2dva 4482 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)                     |
136 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . 16
               |
137 | 60, 62, 115 | expcnfg 37768 |
. . . . . . . . . . . . . . . 16
                   |
138 | 136, 137,
64 | cncfmptss 37762 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)           
          ![[,] [,]](_icc.gif)       |
139 | 135, 138 | eqeltrd 2549 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       |
140 | | cniccibl 22877 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)                |
141 | 51, 52, 139, 140 | syl3anc 1292 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)                |
142 | 37, 39, 130, 141 | iblss 22841 |
. . . . . . . . . . . 12
                    |
143 | 117, 142,
35, 69 | itgsub 22862 |
. . . . . . . . . . 11
                                                                |
144 | 108, 128,
143 | 3eqtrd 2509 |
. . . . . . . . . 10
                       
                                        |
145 | 144 | oveq2d 6324 |
. . . . . . . . 9
                                                                        |
146 | 85, 95, 145 | 3eqtrd 2509 |
. . . . . . . 8
                                                                |
147 | 29, 78, 146 | 3eqtrd 2509 |
. . . . . . 7
                                             |
148 | | oveq2 6316 |
. . . . . . . . . . . . 13
                  
    |
149 | 148 | adantr 472 |
. . . . . . . . . . . 12
   
                         |
150 | 149 | itgeq2dv 22818 |
. . . . . . . . . . 11
                                     |
151 | 150 | adantl 473 |
. . . . . . . . . 10
 

                                    |
152 | | itgex 22807 |
. . . . . . . . . . 11
                  |
153 | 152 | a1i 11 |
. . . . . . . . . 10
                    |
154 | 13, 151, 115, 153 | fvmptd 5969 |
. . . . . . . . 9
    
                     |
155 | 154, 29 | oveq12d 6326 |
. . . . . . . 8
     
                     
                     |
156 | 155 | oveq2d 6324 |
. . . . . . 7
        
                                                |
157 | 117, 142 | itgcl 22820 |
. . . . . . . . 9
                    |
158 | 154, 157 | eqeltrd 2549 |
. . . . . . . 8
    
    |
159 | 11, 158, 71 | subdid 10095 |
. . . . . . 7
        
                              |
160 | 147, 156,
159 | 3eqtr2d 2511 |
. . . . . 6
                           |
161 | 160 | eqcomd 2477 |
. . . . 5
        
                  |
162 | 11, 158 | mulcld 9681 |
. . . . . 6
             |
163 | 11, 71 | mulcld 9681 |
. . . . . 6
           |
164 | 162, 163,
71 | subaddd 10023 |
. . . . 5
         
                                    
      |
165 | 161, 164 | mpbid 215 |
. . . 4
                     
     |
166 | 8, 72, 165 | 3eqtrd 2509 |
. . 3
             
     |
167 | 166 | oveq1d 6323 |
. 2
                       |
168 | 75 | nnne0d 10676 |
. . 3
   |
169 | 71, 4, 168 | divcan3d 10410 |
. 2
               |
170 | 11, 158, 4, 168 | div23d 10442 |
. 2
        
            
     |
171 | 167, 169,
170 | 3eqtr3d 2513 |
1
             
     |