Step | Hyp | Ref
| Expression |
1 | | itgiccshift.a |
. . . . 5
   |
2 | | itgiccshift.b |
. . . . 5
   |
3 | | itgiccshift.t |
. . . . . 6
   |
4 | 3 | rpred 11341 |
. . . . 5
   |
5 | | itgiccshift.aleb |
. . . . 5

  |
6 | 1, 2, 4, 5 | leadd1dd 10227 |
. . . 4
  
    |
7 | 6 | ditgpos 22811 |
. . 3
 _      ![] ]](rbrack.gif)                       |
8 | 1, 4 | readdcld 9670 |
. . . 4
     |
9 | 2, 4 | readdcld 9670 |
. . . 4
     |
10 | | itgiccshift.f |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       |
11 | | cncff 21925 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)      |
12 | 10, 11 | syl 17 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)      |
13 | 12 | adantr 467 |
. . . . . . 7
 
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif)      |
14 | 1 | adantr 467 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
     |
15 | 2 | adantr 467 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
     |
16 | 8 | adantr 467 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
   
   |
17 | 9 | adantr 467 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
   
   |
18 | | simpr 463 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif) 
    |
19 | | eliccre 37603 |
. . . . . . . . . 10
    

 
  ![[,] [,]](_icc.gif)    
  |
20 | 16, 17, 18, 19 | syl3anc 1268 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
     |
21 | 4 | adantr 467 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
     |
22 | 20, 21 | resubcld 10047 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
       |
23 | 1 | recnd 9669 |
. . . . . . . . . . . 12
   |
24 | 4 | recnd 9669 |
. . . . . . . . . . . 12
   |
25 | 23, 24 | pncand 9987 |
. . . . . . . . . . 11
       |
26 | 25 | eqcomd 2457 |
. . . . . . . . . 10
       |
27 | 26 | adantr 467 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
         |
28 | | elicc2 11699 |
. . . . . . . . . . . . 13
    
       ![[,] [,]](_icc.gif) 
     
     |
29 | 16, 17, 28 | syl2anc 667 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)   
   
     |
30 | 18, 29 | mpbid 214 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
    

     |
31 | 30 | simp2d 1021 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
   
   |
32 | 16, 20, 21, 31 | lesub1dd 10229 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
           |
33 | 27, 32 | eqbrtrd 4423 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
       |
34 | 30 | simp3d 1022 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
       |
35 | 20, 17, 21, 34 | lesub1dd 10229 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
           |
36 | 2 | recnd 9669 |
. . . . . . . . . . 11
   |
37 | 36, 24 | pncand 9987 |
. . . . . . . . . 10
       |
38 | 37 | adantr 467 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
         |
39 | 35, 38 | breqtrd 4427 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
       |
40 | 14, 15, 22, 33, 39 | eliccd 37601 |
. . . . . . 7
 
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif)    |
41 | 13, 40 | ffvelrnd 6023 |
. . . . . 6
 
    ![[,] [,]](_icc.gif) 
           |
42 | | itgiccshift.g |
. . . . . 6
     ![[,] [,]](_icc.gif)            |
43 | 41, 42 | fmptd 6046 |
. . . . 5
       ![[,] [,]](_icc.gif)        |
44 | 43 | fnvinran 37335 |
. . . 4
 
    ![[,] [,]](_icc.gif) 
         |
45 | 8, 9, 44 | itgioo 22773 |
. . 3
                     ![[,] [,]](_icc.gif)            |
46 | 7, 45 | eqtr2d 2486 |
. 2
      ![[,] [,]](_icc.gif)          _  
   ![] ]](rbrack.gif)        |
47 | | eqid 2451 |
. . . 4
         |
48 | 47 | addccncf 21948 |
. . . . 5
           |
49 | 24, 48 | syl 17 |
. . . 4
           |
50 | 1, 2 | iccssred 37602 |
. . . . 5
   ![[,] [,]](_icc.gif) 
  |
51 | | ax-resscn 9596 |
. . . . 5
 |
52 | 50, 51 | syl6ss 3444 |
. . . 4
   ![[,] [,]](_icc.gif) 
  |
53 | 8, 9 | iccssred 37602 |
. . . . 5
     ![[,] [,]](_icc.gif) 
 
  |
54 | 53, 51 | syl6ss 3444 |
. . . 4
     ![[,] [,]](_icc.gif) 
 
  |
55 | 8 | adantr 467 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
    |
56 | 9 | adantr 467 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
    |
57 | 50 | sselda 3432 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
  |
58 | 4 | adantr 467 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
  |
59 | 57, 58 | readdcld 9670 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
    |
60 | 1 | adantr 467 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
  |
61 | | simpr 463 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
62 | 2 | adantr 467 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
  |
63 | | elicc2 11699 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif)  
    |
64 | 60, 62, 63 | syl2anc 667 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)  
    |
65 | 61, 64 | mpbid 214 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  

   |
66 | 65 | simp2d 1021 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
  |
67 | 60, 57, 58, 66 | leadd1dd 10227 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
      |
68 | 65 | simp3d 1022 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
  |
69 | 57, 62, 58, 68 | leadd1dd 10227 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
  
   |
70 | 55, 56, 59, 67, 69 | eliccd 37601 |
. . . 4
 
  ![[,] [,]](_icc.gif)  
      ![[,] [,]](_icc.gif)      |
71 | 47, 49, 52, 54, 70 | cncfmptssg 37747 |
. . 3
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
72 | | oveq1 6297 |
. . . . . . . . 9
       |
73 | 72 | fveq2d 5869 |
. . . . . . . 8
               |
74 | 73 | cbvmptv 4495 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif) 
     
    |
75 | 1, 2, 4 | iccshift 37619 |
. . . . . . . 8
     ![[,] [,]](_icc.gif) 
      ![[,] [,]](_icc.gif)        |
76 | 75 | mpteq1d 4484 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)         
     |
77 | 74, 76 | syl5eq 2497 |
. . . . . 6
      ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)         
     |
78 | 42, 77 | syl5eq 2497 |
. . . . 5
      ![[,] [,]](_icc.gif)         
     |
79 | | eqeq1 2455 |
. . . . . . . . . 10
   
     |
80 | 79 | rexbidv 2901 |
. . . . . . . . 9
  
  ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)        |
81 | | oveq1 6297 |
. . . . . . . . . . 11
       |
82 | 81 | eqeq2d 2461 |
. . . . . . . . . 10
   
     |
83 | 82 | cbvrexv 3020 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)       |
84 | 80, 83 | syl6bb 265 |
. . . . . . . 8
  
  ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)        |
85 | 84 | cbvrabv 3044 |
. . . . . . 7
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
86 | 85 | eqcomi 2460 |
. . . . . 6
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
87 | | eqid 2451 |
. . . . . 6
     ![[,] [,]](_icc.gif)         
     
  ![[,] [,]](_icc.gif)              |
88 | 52, 24, 86, 10, 87 | cncfshift 37751 |
. . . . 5
   
  ![[,] [,]](_icc.gif)               
  ![[,] [,]](_icc.gif)           |
89 | 78, 88 | eqeltrd 2529 |
. . . 4
   
  ![[,] [,]](_icc.gif)           |
90 | 43 | feqmptd 5918 |
. . . 4
      ![[,] [,]](_icc.gif)           |
91 | 75 | eqcomd 2457 |
. . . . 5
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      |
92 | 91 | oveq1d 6305 |
. . . 4
      ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif) 
       |
93 | 89, 90, 92 | 3eltr3d 2543 |
. . 3
      ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif) 
       |
94 | | ioosscn 37591 |
. . . . . 6
     |
95 | 94 | a1i 11 |
. . . . 5
    
  |
96 | | 1cnd 9659 |
. . . . 5
   |
97 | | ssid 3451 |
. . . . . 6
 |
98 | 97 | a1i 11 |
. . . . 5

  |
99 | 95, 96, 98 | constcncfg 37748 |
. . . 4
                 |
100 | | fconstmpt 4878 |
. . . . 5
               |
101 | | ioombl 22518 |
. . . . . . 7
     |
102 | 101 | a1i 11 |
. . . . . 6
       |
103 | | ioovolcl 22522 |
. . . . . . 7
 
           |
104 | 1, 2, 103 | syl2anc 667 |
. . . . . 6
           |
105 | | iblconst 22775 |
. . . . . 6
                          |
106 | 102, 104,
96, 105 | syl3anc 1268 |
. . . . 5
            |
107 | 100, 106 | syl5eqelr 2534 |
. . . 4
          |
108 | 99, 107 | elind 3618 |
. . 3
                    |
109 | 50 | resmptd 5156 |
. . . . . . 7
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
110 | 109 | eqcomd 2457 |
. . . . . 6
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)     |
111 | 110 | oveq2d 6306 |
. . . . 5
     ![[,] [,]](_icc.gif)           
  ![[,] [,]](_icc.gif)      |
112 | 51 | a1i 11 |
. . . . . 6

  |
113 | 112 | sselda 3432 |
. . . . . . . 8
 

  |
114 | 24 | adantr 467 |
. . . . . . . 8
 

  |
115 | 113, 114 | addcld 9662 |
. . . . . . 7
 

    |
116 | | eqid 2451 |
. . . . . . 7
         |
117 | 115, 116 | fmptd 6046 |
. . . . . 6
           |
118 | | ssid 3451 |
. . . . . . 7
 |
119 | 118 | a1i 11 |
. . . . . 6

  |
120 | | eqid 2451 |
. . . . . . 7
  ℂfld   ℂfld |
121 | 120 | tgioo2 21821 |
. . . . . . 7
       ℂfld
↾t   |
122 | 120, 121 | dvres 22866 |
. . . . . 6
           
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                 
      ![[,] [,]](_icc.gif)      |
123 | 112, 117,
119, 50, 122 | syl22anc 1269 |
. . . . 5
         ![[,] [,]](_icc.gif)          
             ![[,] [,]](_icc.gif)      |
124 | 111, 123 | eqtrd 2485 |
. . . 4
     ![[,] [,]](_icc.gif)                   
      ![[,] [,]](_icc.gif)      |
125 | | iccntr 21839 |
. . . . . 6
 
       
      ![[,] [,]](_icc.gif)         |
126 | 1, 2, 125 | syl2anc 667 |
. . . . 5
       
      ![[,] [,]](_icc.gif)         |
127 | 126 | reseq2d 5105 |
. . . 4
              
      ![[,] [,]](_icc.gif)                  |
128 | | reelprrecn 9631 |
. . . . . . . 8
    |
129 | 128 | a1i 11 |
. . . . . . 7
      |
130 | | 1cnd 9659 |
. . . . . . 7
 

  |
131 | 129 | dvmptid 22911 |
. . . . . . 7
         |
132 | | 0cnd 9636 |
. . . . . . 7
 

  |
133 | 129, 24 | dvmptc 22912 |
. . . . . . 7
         |
134 | 129, 113,
130, 131, 114, 132, 133 | dvmptadd 22914 |
. . . . . 6
             |
135 | 134 | reseq1d 5104 |
. . . . 5
                 
       |
136 | | ioossre 11696 |
. . . . . . 7
     |
137 | 136 | a1i 11 |
. . . . . 6
    
  |
138 | 137 | resmptd 5156 |
. . . . 5
                     |
139 | | 1p0e1 10722 |
. . . . . . 7
   |
140 | 139 | mpteq2i 4486 |
. . . . . 6
               |
141 | 140 | a1i 11 |
. . . . 5
                 |
142 | 135, 138,
141 | 3eqtrd 2489 |
. . . 4
                     |
143 | 124, 127,
142 | 3eqtrd 2489 |
. . 3
     ![[,] [,]](_icc.gif)              |
144 | | fveq2 5865 |
. . 3
               |
145 | | oveq1 6297 |
. . 3
       |
146 | | oveq1 6297 |
. . 3
       |
147 | 1, 2, 5, 71, 93, 108, 143, 144, 145, 146, 8, 9 | itgsubsticc 37853 |
. 2
 _      ![] ]](rbrack.gif)      _  ![] ]](rbrack.gif)            |
148 | 5 | ditgpos 22811 |
. . 3
 _  ![] ]](rbrack.gif)                           |
149 | 43 | adantr 467 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
      ![[,] [,]](_icc.gif) 
      |
150 | 149, 70 | ffvelrnd 6023 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
        |
151 | | 1cnd 9659 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
  |
152 | 150, 151 | mulcld 9663 |
. . . 4
 
  ![[,] [,]](_icc.gif)  
          |
153 | 1, 2, 152 | itgioo 22773 |
. . 3
                   ![[,] [,]](_icc.gif)              |
154 | | oveq1 6297 |
. . . . . . 7
       |
155 | 154 | fveq2d 5869 |
. . . . . 6
               |
156 | 155 | oveq1d 6305 |
. . . . 5
                   |
157 | 156 | cbvitgv 22734 |
. . . 4
   ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)             |
158 | 43 | adantr 467 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
      ![[,] [,]](_icc.gif) 
      |
159 | 8 | adantr 467 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
    |
160 | 9 | adantr 467 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
    |
161 | 50 | sselda 3432 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
162 | 4 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
163 | 161, 162 | readdcld 9670 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
    |
164 | 1 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
165 | 1 | rexrd 9690 |
. . . . . . . . . . . 12
   |
166 | 165 | adantr 467 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  |
167 | 2 | rexrd 9690 |
. . . . . . . . . . . 12
   |
168 | 167 | adantr 467 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  |
169 | | simpr 463 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
170 | | iccgelb 11691 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)     |
171 | 166, 168,
169, 170 | syl3anc 1268 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
172 | 164, 161,
162, 171 | leadd1dd 10227 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
      |
173 | 2 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
174 | | iccleub 11690 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)     |
175 | 166, 168,
169, 174 | syl3anc 1268 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
176 | 161, 173,
162, 175 | leadd1dd 10227 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
  
   |
177 | 159, 160,
163, 172, 176 | eliccd 37601 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
      ![[,] [,]](_icc.gif)      |
178 | 158, 177 | ffvelrnd 6023 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  
        |
179 | 178 | mulid1d 9660 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
                |
180 | 42, 74 | eqtri 2473 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)            |
181 | 180 | a1i 11 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  

    ![[,] [,]](_icc.gif)             |
182 | | oveq1 6297 |
. . . . . . . . 9
           |
183 | 182 | fveq2d 5869 |
. . . . . . . 8
                   |
184 | 161 | recnd 9669 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
185 | 24 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
186 | 184, 185 | pncand 9987 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
      |
187 | 186 | fveq2d 5869 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
              |
188 | 183, 187 | sylan9eqr 2507 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                  |
189 | 12 | ffvelrnda 6022 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  
      |
190 | 181, 188,
177, 189 | fvmptd 5954 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
            |
191 | 179, 190 | eqtrd 2485 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
              |
192 | 191 | itgeq2dv 22739 |
. . . 4
    ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
193 | 157, 192 | syl5eq 2497 |
. . 3
    ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
194 | 148, 153,
193 | 3eqtrd 2489 |
. 2
 _  ![] ]](rbrack.gif)             ![[,] [,]](_icc.gif)          |
195 | 46, 147, 194 | 3eqtrd 2489 |
1
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |