Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. 2
   |
2 | | ral0 3873 |
. . . . 5
          |
3 | | oveq2 6296 |
. . . . . . 7
  ..^  ..^   |
4 | | fzo0 11939 |
. . . . . . 7
 ..^  |
5 | 3, 4 | syl6eq 2500 |
. . . . . 6
  ..^   |
6 | | fveq2 5863 |
. . . . . . 7
           |
7 | 6 | breq2d 4413 |
. . . . . 6
     
   
           |
8 | 5, 7 | raleqbidv 3000 |
. . . . 5
  
 ..^         
            |
9 | 2, 8 | mpbiri 237 |
. . . 4
   ..^     
      |
10 | 9 | 2a1d 27 |
. . 3
  
  ..^     
        |
11 | | simpr 463 |
. . . . . . 7
  
    |
12 | | iccpartgtprec.p |
. . . . . . . . 9
 RePart    |
13 | 12 | adantr 467 |
. . . . . . . 8
 

RePart    |
14 | 13 | adantr 467 |
. . . . . . 7
  
  RePart    |
15 | | nnnn0 10873 |
. . . . . . . . 9
   |
16 | | nn0fz0 11887 |
. . . . . . . . 9

      |
17 | 15, 16 | sylib 200 |
. . . . . . . 8
       |
18 | 17 | adantl 468 |
. . . . . . 7
  
        |
19 | 11, 14, 18 | iccpartxr 38727 |
. . . . . 6
  
        |
20 | | elxr 11413 |
. . . . . . 7
    
                |
21 | | elfzoelz 11917 |
. . . . . . . . . . . . . 14
  ..^
  |
22 | 21 | ad2antll 734 |
. . . . . . . . . . . . 13
            ..^     |
23 | | elfzo2 11920 |
. . . . . . . . . . . . . . 15
  ..^     
   |
24 | | eluzelz 11165 |
. . . . . . . . . . . . . . . . . 18
    
  |
25 | 24 | peano2zd 11040 |
. . . . . . . . . . . . . . . . 17
    
    |
26 | 25 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . 16
           |
27 | | simp2 1008 |
. . . . . . . . . . . . . . . 16
         |
28 | | zltp1le 10983 |
. . . . . . . . . . . . . . . . . 18
 
       |
29 | 24, 28 | sylan 474 |
. . . . . . . . . . . . . . . . 17
       
     |
30 | 29 | biimp3a 1368 |
. . . . . . . . . . . . . . . 16
           |
31 | | eluz2 11162 |
. . . . . . . . . . . . . . . 16
               |
32 | 26, 27, 30, 31 | syl3anbrc 1191 |
. . . . . . . . . . . . . . 15
               |
33 | 23, 32 | sylbi 199 |
. . . . . . . . . . . . . 14
  ..^
        |
34 | 33 | ad2antll 734 |
. . . . . . . . . . . . 13
            ..^           |
35 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
           |
36 | 35 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . 19
           |
37 | 36 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . 18
     
       |
38 | 37 | biimpcd 228 |
. . . . . . . . . . . . . . . . 17
             |
39 | 38 | adantr 467 |
. . . . . . . . . . . . . . . 16
            ..^           |
40 | 39 | adantr 467 |
. . . . . . . . . . . . . . 15
             ..^                |
41 | 40 | com12 32 |
. . . . . . . . . . . . . 14
          
   ..^               |
42 | 11 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   


 ..^ 
  |
43 | 42 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
            ..^     |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . . . . 17
             ..^          |
45 | 44 | adantl 468 |
. . . . . . . . . . . . . . . 16
          


 ..^        
  |
46 | 14 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   


 ..^ 
RePart    |
47 | 46 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
            ..^   RePart    |
48 | 47 | adantr 467 |
. . . . . . . . . . . . . . . . 17
             ..^        RePart    |
49 | 48 | adantl 468 |
. . . . . . . . . . . . . . . 16
          


 ..^        
RePart    |
50 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
 
 
    |
51 | | eluz2 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
52 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
53 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
54 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
55 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   |
56 | 55 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
57 | | letr 9724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
  
    |
58 | 52, 54, 56, 57 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
  

   |
59 | 58 | expcomd 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
  
    |
60 | 59 | adantrd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
  

     |
61 | 60 | 3adant2 1026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
  
 
    |
62 | 61 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
 
 
    |
63 | 62 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
     |
64 | 63 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     
     |
65 | 51, 64 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  
 
 
   |
66 | 65 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
     |
67 | 23, 66 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ..^
  
 
 
   |
68 | 50, 67 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
    
   |
69 | 68 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^        |
70 | 69 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^    
   |
71 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
72 | 71, 55 | anim12ci 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
     |
73 | 72 | 3adant1 1025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
 
   |
74 | | ltlen 9732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
  
    |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
 
     |
76 | | nesym 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
77 | 76 | anbi2i 699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

    |
78 | 75, 77 | syl6rbb 266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
79 | 78 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   
   |
80 | 79 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
     |
81 | 80 | adantld 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
 
    |
82 | 81 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 
 

   |
83 | 50, 82 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
84 | 83 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

  |
85 | 84 | 3adant1 1025 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^    
   |
86 | 70, 85 | jca 535 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^    
 
   |
87 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
88 | | 1zzd 10965 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
89 | | elfzel2 11795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
90 | 87, 88, 89 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
   |
91 | 90 | 3ad2ant2 1029 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^    
 
   |
92 | | elfzo 11919 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   ..^
     |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^    
   ..^
     |
94 | 86, 93 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . 20
   ..^    
  ..^   |
95 | 94 | 3exp 1206 |
. . . . . . . . . . . . . . . . . . 19
  ..^
    

 ..^     |
96 | 95 | ad2antll 734 |
. . . . . . . . . . . . . . . . . 18
            ..^        
 ..^     |
97 | 96 | imp 431 |
. . . . . . . . . . . . . . . . 17
             ..^        
 ..^    |
98 | 97 | impcom 432 |
. . . . . . . . . . . . . . . 16
          


 ..^          ..^   |
99 | 45, 49, 98 | iccpartipre 38729 |
. . . . . . . . . . . . . . 15
          


 ..^               |
100 | 99 | ex 436 |
. . . . . . . . . . . . . 14
          


 ..^               |
101 | 41, 100 | pm2.61i 168 |
. . . . . . . . . . . . 13
             ..^              |
102 | 43 | adantr 467 |
. . . . . . . . . . . . . . 15
             ..^      
     |
103 | 47 | adantr 467 |
. . . . . . . . . . . . . . 15
             ..^      
   RePart    |
104 | | 1eluzge0 11199 |
. . . . . . . . . . . . . . . . . . . 20
     |
105 | | fzoss1 11942 |
. . . . . . . . . . . . . . . . . . . 20
    
 ..^  ..^   |
106 | 104, 105 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
   ..^    
    ..^  ..^   |
107 | | elfzoel2 11916 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
  |
108 | | fzoval 11918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^    
    |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
 ..^         |
110 | 109 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
       ..^   |
111 | 110 | eleq2d 2513 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
    
   ..^    |
112 | | elfzouz 11921 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
      |
113 | | fzoss1 11942 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 ..^  ..^   |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
 ..^  ..^   |
115 | 114 | sseld 3430 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  ..^  ..^    |
116 | 111, 115 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
    
 
 ..^    |
117 | 116 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
   ..^    
    ..^   |
118 | 106, 117 | sseldd 3432 |
. . . . . . . . . . . . . . . . . 18
   ..^    
    ..^   |
119 | 118 | ex 436 |
. . . . . . . . . . . . . . . . 17
  ..^
    
 
 ..^    |
120 | 119 | ad2antll 734 |
. . . . . . . . . . . . . . . 16
            ..^           ..^    |
121 | 120 | imp 431 |
. . . . . . . . . . . . . . 15
             ..^      
    ..^   |
122 | | iccpartimp 38725 |
. . . . . . . . . . . . . . 15
 
RePart 
 ..^   
                  |
123 | 102, 103,
121, 122 | syl3anc 1267 |
. . . . . . . . . . . . . 14
             ..^      
   
                   |
124 | 123 | simprd 465 |
. . . . . . . . . . . . 13
             ..^      
               |
125 | 22, 34, 101, 124 | smonoord 38712 |
. . . . . . . . . . . 12
            ..^             |
126 | 125 | ex 436 |
. . . . . . . . . . 11
            ..^ 
           |
127 | | simpr 463 |
. . . . . . . . . . . . . 14
   


 ..^ 
 ..^   |
128 | 42, 46, 127 | iccpartipre 38729 |
. . . . . . . . . . . . 13
   


 ..^ 
      |
129 | | ltpnf 11419 |
. . . . . . . . . . . . 13
           |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . 12
   


 ..^ 
      |
131 | | breq2 4405 |
. . . . . . . . . . . 12
         
   
       |
132 | 130, 131 | syl5ibr 225 |
. . . . . . . . . . 11
            ..^ 
           |
133 | 42 | adantl 468 |
. . . . . . . . . . . . . . 15
            ..^     |
134 | 46 | adantl 468 |
. . . . . . . . . . . . . . 15
            ..^   RePart    |
135 | | elfzofz 11932 |
. . . . . . . . . . . . . . . . 17
  ..^
      |
136 | 135 | ad2antll 734 |
. . . . . . . . . . . . . . . 16
            ..^         |
137 | | elfzubelfz 11808 |
. . . . . . . . . . . . . . . 16
           |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . 15
            ..^         |
139 | 133, 134,
138 | iccpartgtprec 38728 |
. . . . . . . . . . . . . 14
            ..^               |
140 | | breq2 4405 |
. . . . . . . . . . . . . . . 16
        
 
             |
141 | 140 | eqcoms 2458 |
. . . . . . . . . . . . . . 15
         
 
             |
142 | 141 | adantr 467 |
. . . . . . . . . . . . . 14
            ..^       
 
             |
143 | 139, 142 | mpbird 236 |
. . . . . . . . . . . . 13
            ..^           |
144 | 15 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
  
    |
145 | 144 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   


 ..^ 
  |
146 | | nnne0 10639 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
147 | 146 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
148 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
149 | 148 | biimpri 210 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
150 | 149 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
151 | 150 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
152 | 144, 147,
151 | 3jca 1187 |
. . . . . . . . . . . . . . . . . . . 20
  
  
   |
153 | 152 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   


 ..^ 
    |
154 | | nn0n0n1ge2 10929 |
. . . . . . . . . . . . . . . . . . 19
     |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   


 ..^ 
  |
156 | 145, 155 | jca 535 |
. . . . . . . . . . . . . . . . 17
   


 ..^ 
    |
157 | 156 | adantl 468 |
. . . . . . . . . . . . . . . 16
            ..^   
   |
158 | | ige2m1fz 11881 |
. . . . . . . . . . . . . . . 16
           |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . 15
            ..^   
       |
160 | 133, 134,
159 | iccpartxr 38727 |
. . . . . . . . . . . . . 14
            ..^           |
161 | | nltmnf 11428 |
. . . . . . . . . . . . . 14
      
        |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . 13
            ..^           |
163 | 143, 162 | pm2.21dd 178 |
. . . . . . . . . . . 12
            ..^             |
164 | 163 | ex 436 |
. . . . . . . . . . 11
            ..^ 
           |
165 | 126, 132,
164 | 3jaoi 1330 |
. . . . . . . . . 10
                      ..^ 
           |
166 | 165 | impl 625 |
. . . . . . . . 9
                  

 
 ..^            |
167 | 166 | ralrimiva 2801 |
. . . . . . . 8
                 

    ..^     
      |
168 | 167 | ex 436 |
. . . . . . 7
                 


  ..^     
       |
169 | 20, 168 | sylbi 199 |
. . . . . 6
    
  
    ..^             |
170 | 19, 169 | mpcom 37 |
. . . . 5
  
    ..^            |
171 | 170 | ex 436 |
. . . 4
 
    ..^             |
172 | 171 | expcom 437 |
. . 3
 
   ..^     
        |
173 | 10, 172 | pm2.61i 168 |
. 2
    ..^             |
174 | 1, 173 | mpd 15 |
1
   ..^            |