Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . . . 9
   |
2 | 1 | nnnn0d 10925 |
. . . . . . . 8
   |
3 | | elnn0uz 11196 |
. . . . . . . 8

      |
4 | 2, 3 | sylib 200 |
. . . . . . 7
       |
5 | | fzpred 11844 |
. . . . . . 7
    
                |
6 | 4, 5 | syl 17 |
. . . . . 6
                 |
7 | | 0p1e1 10721 |
. . . . . . . . 9
   |
8 | 7 | oveq1i 6300 |
. . . . . . . 8
           |
9 | 8 | a1i 11 |
. . . . . . 7
             |
10 | 9 | uneq2d 3588 |
. . . . . 6
                     |
11 | 6, 10 | eqtrd 2485 |
. . . . 5
               |
12 | 11 | eleq2d 2514 |
. . . 4
                 |
13 | | elun 3574 |
. . . . . . 7
                   |
14 | | elsn 3982 |
. . . . . . . 8
     |
15 | 14 | orbi1i 523 |
. . . . . . 7
        
        |
16 | 13, 15 | bitri 253 |
. . . . . 6
                 |
17 | | fzisfzounsn 12020 |
. . . . . . . . . . 11
    
      ..^      |
18 | 4, 17 | syl 17 |
. . . . . . . . . 10
       ..^      |
19 | 18 | eleq2d 2514 |
. . . . . . . . 9
        ..^       |
20 | | elun 3574 |
. . . . . . . . . 10
   ..^   
  ..^      |
21 | | elsn 3982 |
. . . . . . . . . . 11
     |
22 | 21 | orbi2i 522 |
. . . . . . . . . 10
   ..^      ..^    |
23 | 20, 22 | bitri 253 |
. . . . . . . . 9
   ..^   
  ..^    |
24 | 19, 23 | syl6bb 265 |
. . . . . . . 8
        ..^     |
25 | | iccpartgtprec.p |
. . . . . . . . . . . . . . . . . . 19
 RePart    |
26 | 1, 25 | iccpartigtl 38737 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
27 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^   ..^   |
28 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^    |
29 | 28 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^    |
30 | | fzo1fzo0n0 11957 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^   ..^    |
31 | 27, 29, 30 | sylanbrc 670 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^   ..^   |
32 | 31 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
  ..^    ..^   |
33 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
34 | 33 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . 21
     
   
           |
35 | 34 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
 
 ..^         
           |
36 | 32, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
  ..^    
 ..^                     |
37 | 36 | ex 436 |
. . . . . . . . . . . . . . . . . 18
    ..^ 
 
 ..^         
            |
38 | 26, 37 | mpid 42 |
. . . . . . . . . . . . . . . . 17
    ..^ 
           |
39 | 38 | expd 438 |
. . . . . . . . . . . . . . . 16
   ..^     
        |
40 | 39 | impcom 432 |
. . . . . . . . . . . . . . 15
   ..^  
           |
41 | | breq1 4405 |
. . . . . . . . . . . . . . . 16
 
   |
42 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
43 | 42 | breq1d 4412 |
. . . . . . . . . . . . . . . 16
     
   
           |
44 | 41, 43 | imbi12d 322 |
. . . . . . . . . . . . . . 15
      
    
             |
45 | 40, 44 | syl5ibr 225 |
. . . . . . . . . . . . . 14
    ..^ 

            |
46 | 45 | expd 438 |
. . . . . . . . . . . . 13
   ..^  
             |
47 | 46 | com12 32 |
. . . . . . . . . . . 12
  ..^
  
             |
48 | 1, 25 | iccpartlt 38738 |
. . . . . . . . . . . . . . 15
    
      |
49 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
50 | 42, 49 | breqan12rd 4419 |
. . . . . . . . . . . . . . 15
 
                     |
51 | 48, 50 | syl5ibr 225 |
. . . . . . . . . . . . . 14
 
             |
52 | 51 | a1dd 47 |
. . . . . . . . . . . . 13
 
      
        |
53 | 52 | ex 436 |
. . . . . . . . . . . 12
  
              |
54 | 47, 53 | jaoi 381 |
. . . . . . . . . . 11
   ..^   
              |
55 | 54 | com12 32 |
. . . . . . . . . 10
    ..^       
         |
56 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . 17
       |
57 | 56 | ad3antlr 737 |
. . . . . . . . . . . . . . . 16
     ..^          |
58 | 56 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . . . 20
         |
59 | 58 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . 19
    ..^
     
    |
60 | | elfzoelz 11920 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
61 | 60 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
    ..^
     
  |
62 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
    ..^
     
  |
63 | 60, 56 | anim12ci 571 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^      
   |
64 | 63 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^
     
    |
65 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    ..^
     
      |
67 | 62, 66 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
    ..^
     
    |
68 | 59, 61, 67 | 3jca 1188 |
. . . . . . . . . . . . . . . . . 18
    ..^
     
        |
69 | 68 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     ..^                |
70 | | eluz2 11165 |
. . . . . . . . . . . . . . . . 17
               |
71 | 69, 70 | sylibr 216 |
. . . . . . . . . . . . . . . 16
     ..^                |
72 | 1 | ad2antlr 733 |
. . . . . . . . . . . . . . . . 17
      ..^            
  |
73 | 25 | ad2antlr 733 |
. . . . . . . . . . . . . . . . 17
      ..^            
RePart    |
74 | | 1zzd 10968 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
75 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . 20
       |
76 | 75 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
77 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
78 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
79 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
80 | | elfzel1 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
81 | 80 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
82 | 75 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
83 | | letr 9727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
    |
84 | 79, 81, 82, 83 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
    |
85 | 78, 84 | mpan2d 680 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   |
86 | 77, 85 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . 21
         
   |
87 | 86 | ad3antlr 737 |
. . . . . . . . . . . . . . . . . . . 20
     ..^            
   |
88 | 87 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
89 | | eluz2 11165 |
. . . . . . . . . . . . . . . . . . 19
         |
90 | 74, 76, 88, 89 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . . . 18
      ..^            
      |
91 | | elfzel2 11798 |
. . . . . . . . . . . . . . . . . . . 20
       |
92 | 91 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . 19
    ..^
     
  |
93 | 92 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
      ..^            
  |
94 | 82 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
95 | 60 | zred 11040 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
96 | 95 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
97 | 72 | nnred 10624 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
98 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . 20
       |
99 | 98 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
100 | | elfzolt2 11929 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
101 | 100 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . 19
      ..^            
  |
102 | 94, 96, 97, 99, 101 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . 18
      ..^            
  |
103 | | elfzo2 11923 |
. . . . . . . . . . . . . . . . . 18
  ..^     
   |
104 | 90, 93, 102, 103 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . . 17
      ..^            
 ..^   |
105 | 72, 73, 104 | iccpartipre 38735 |
. . . . . . . . . . . . . . . 16
      ..^            
      |
106 | 1 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
      ..^              
  |
107 | 25 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
      ..^              
RePart    |
108 | 60 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . 21
     ..^          |
109 | | fzoval 11921 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^         |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     ..^         ..^         |
111 | | elfzo0le 11959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
  |
112 | | 0le1 10137 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
113 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
114 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
115 | 56 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
116 | | letr 9727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
    |
117 | 113, 114,
115, 116 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
    |
118 | 112, 117 | mpani 682 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
   |
119 | 77, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
120 | 111, 119 | anim12ci 571 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ..^      
   |
121 | 120 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^
     
    |
122 | | 0zd 10949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ..^
  |
123 | | elfzoel2 11919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ..^
  |
124 | 122, 123 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
    |
125 | 124 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ..^
     
    |
126 | | ssfzo12bi 12006 |
. . . . . . . . . . . . . . . . . . . . . . 23
         ..^  ..^ 
    |
127 | 64, 125, 62, 126 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^
     
  ..^  ..^
     |
128 | 121, 127 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^
     
 ..^  ..^   |
129 | 128 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     ..^         ..^
 ..^   |
130 | 110, 129 | eqsstr3d 3467 |
. . . . . . . . . . . . . . . . . . 19
     ..^               ..^   |
131 | 130 | sselda 3432 |
. . . . . . . . . . . . . . . . . 18
      ..^              
 ..^   |
132 | | iccpartimp 38731 |
. . . . . . . . . . . . . . . . . 18
 
RePart 
 ..^   
                  |
133 | 106, 107,
131, 132 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
      ..^              
 
                  |
134 | 133 | simprd 465 |
. . . . . . . . . . . . . . . 16
      ..^              
            |
135 | 57, 71, 105, 134 | smonoord 38718 |
. . . . . . . . . . . . . . 15
     ..^                  |
136 | 135 | exp31 609 |
. . . . . . . . . . . . . 14
   ..^      
             |
137 | 136 | com23 81 |
. . . . . . . . . . . . 13
   ..^       
            |
138 | 137 | ex 436 |
. . . . . . . . . . . 12
  ..^
    
     
         |
139 | 1, 25 | iccpartiltu 38736 |
. . . . . . . . . . . . . . . . . . 19
   ..^            |
140 | | elfzuz 11796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
141 | 140 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
142 | 91 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
  |
143 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
  |
144 | | elfzo2 11923 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^     
   |
145 | 141, 142,
143, 144 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
        ..^   |
146 | 145 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
   ..^   |
147 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
148 | 147 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   
           |
149 | 148 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
 
 ..^         
           |
150 | 146, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
    
   
 ..^                     |
151 | 150 | ex 436 |
. . . . . . . . . . . . . . . . . . 19
      

 
 ..^         
            |
152 | 139, 151 | mpid 42 |
. . . . . . . . . . . . . . . . . 18
      

           |
153 | 152 | expd 438 |
. . . . . . . . . . . . . . . . 17
      
            |
154 | 153 | impcom 432 |
. . . . . . . . . . . . . . . 16
      

           |
155 | 154 | imp 431 |
. . . . . . . . . . . . . . 15
            
      |
156 | 155 | a1i 11 |
. . . . . . . . . . . . . 14
       
     
       |
157 | | breq2 4406 |
. . . . . . . . . . . . . . 15
 
   |
158 | 157 | anbi2d 710 |
. . . . . . . . . . . . . 14
       
 
           |
159 | 49 | breq2d 4414 |
. . . . . . . . . . . . . 14
     
   
           |
160 | 156, 158,
159 | 3imtr4d 272 |
. . . . . . . . . . . . 13
       
     
       |
161 | 160 | exp4c 613 |
. . . . . . . . . . . 12
      
              |
162 | 138, 161 | jaoi 381 |
. . . . . . . . . . 11
   ..^       
              |
163 | 162 | com12 32 |
. . . . . . . . . 10
        ..^       
         |
164 | 55, 163 | jaoi 381 |
. . . . . . . . 9
          ..^   
             |
165 | 164 | com13 83 |
. . . . . . . 8
    ..^ 
       
             |
166 | 24, 165 | sylbid 219 |
. . . . . . 7
             
             |
167 | 166 | com3r 82 |
. . . . . 6
                 
         |
168 | 16, 167 | sylbi 199 |
. . . . 5
                   
         |
169 | 168 | com12 32 |
. . . 4
                   
         |
170 | 12, 169 | sylbid 219 |
. . 3
          

             |
171 | 170 | imp32 435 |
. 2
 
    
          
       |
172 | 171 | ralrimivva 2809 |
1
                 
       |