Step | Hyp | Ref
| Expression |
1 | | elioo3g 11665 |
. . 3
              
           
     
   
      |
2 | | iccpartnel.x |
. . . . . . 7
   |
3 | | iccpartnel.p |
. . . . . . . . 9
 RePart    |
4 | | iccpartnel.m |
. . . . . . . . . . 11
   |
5 | | iccpart 38730 |
. . . . . . . . . . 11
 
RePart   
       ..^     
          |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
  RePart 
 
       ..^     
          |
7 | | elmapfn 7494 |
. . . . . . . . . . 11
             |
8 | 7 | adantr 467 |
. . . . . . . . . 10
        
 ..^                   |
9 | 6, 8 | syl6bi 232 |
. . . . . . . . 9
  RePart         |
10 | 3, 9 | mpd 15 |
. . . . . . . 8
       |
11 | | fvelrnb 5912 |
. . . . . . . 8
     
             |
12 | 10, 11 | syl 17 |
. . . . . . 7
  
            |
13 | 2, 12 | mpbid 214 |
. . . . . 6
             |
14 | | elfzelz 11800 |
. . . . . . . . . . . . 13
       |
15 | 14 | zred 11040 |
. . . . . . . . . . . 12
       |
16 | 15 | adantl 468 |
. . . . . . . . . . 11
 
       |
17 | | elfzoelz 11920 |
. . . . . . . . . . . 12
  ..^
  |
18 | 17 | zred 11040 |
. . . . . . . . . . 11
  ..^
  |
19 | | lelttric 9741 |
. . . . . . . . . . 11
 
 
   |
20 | 16, 18, 19 | syl2an 480 |
. . . . . . . . . 10
         ..^ 
    |
21 | | breq2 4406 |
. . . . . . . . . . . . . . . . . 18
         
   
       |
22 | | breq1 4405 |
. . . . . . . . . . . . . . . . . 18
         
     
         |
23 | 21, 22 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
                  
      
               |
24 | | leloe 9720 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
25 | 16, 18, 24 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
         ..^ 
      |
26 | 4, 3 | iccpartgt 38741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
       |
27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                 
           |
28 | 27 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         ..^ 
            
           |
29 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
           |
30 | | elfzofz 11935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^
      |
31 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
32 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
33 | 32 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
   
           |
34 | 31, 33 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
    

            |
35 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
36 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
37 | 36 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
   
           |
38 | 35, 37 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
    

            |
39 | 34, 38 | rspc2v 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                  
        

            |
40 | 29, 30, 39 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         ..^ 
 
     
         
         
        |
41 | 28, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         ..^ 

           |
42 | | pm3.35 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
   
                |
43 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
       |
44 | 3 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
     RePart    |
45 | 43, 44, 29 | iccpartxr 38733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
           |
46 | 45 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
         ..^ 
      |
47 | | simp1 1008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
           
       |
48 | | xrltle 11448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
               
               |
49 | 46, 47, 48 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               
      ..^       
               |
50 | | xrlenlt 9699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
               
   
           |
51 | 46, 47, 50 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               
      ..^       
   
           |
52 | 49, 51 | sylibd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               
      ..^       
               |
53 | 52 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           
   
      ..^          
            |
54 | 53 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
      ..^       
     
             |
55 | 54 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
     
      ..^                           |
56 | 55 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            
      ..^       
     
     
      |
57 | 56 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            
      ..^       
     
                            |
58 | 57 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
     
      ..^                    
   
                  |
59 | 58 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
      ..^       
     
     
   
                   |
60 | 42, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
   
        
      ..^ 
           
     
   
                   |
61 | 60 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
              ..^       
     
     
   
                    |
62 | 61 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         ..^ 
 
               
                                    |
63 | 41, 62 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         ..^ 

           
     
   
                   |
64 | 63 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^       
     
     
   
                   |
65 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
66 | 65 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
   
           |
67 | 66 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                   |
68 | | xrltnr 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
          |
69 | 68 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
           |
70 | 69 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
      |
71 | 70 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                         |
72 | 67, 71 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                         |
73 | 72 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  
   
                  |
74 | 73 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^       
     
     
   
                   |
75 | 64, 74 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      ..^ 
           
     
   
                   |
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
         ..^ 
 
      
                                   |
77 | 25, 76 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . 20
         ..^ 

           
     
   
                   |
78 | 77 | com23 81 |
. . . . . . . . . . . . . . . . . . 19
         ..^ 
           
 
    
   
                   |
79 | 78 | com14 91 |
. . . . . . . . . . . . . . . . . 18
                      
  
      ..^ 
                   |
80 | 79 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
                            
  
      ..^ 
                   |
81 | 23, 80 | syl6bir 233 |
. . . . . . . . . . . . . . . 16
          
            
     
 
  
      ..^ 
                    |
82 | 81 | com14 91 |
. . . . . . . . . . . . . . 15
      
            
     
               ..^ 
                    |
83 | 82 | com23 81 |
. . . . . . . . . . . . . 14
                   
           
  
      ..^ 
                    |
84 | 83 | impd 433 |
. . . . . . . . . . . . 13
       
           
       
    
         ..^ 
                   |
85 | 84 | com24 90 |
. . . . . . . . . . . 12
   
      ..^      
                  
   
   
                   |
86 | 14 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
87 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
88 | 17, 86, 87 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . 21
         ..^ 
      |
89 | 17 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
    |
90 | 89 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
    |
91 | | leloe 9720 |
. . . . . . . . . . . . . . . . . . . . . 22
   
             |
92 | 90, 16, 91 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . 21
         ..^ 
  
         |
93 | 88, 92 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . 20
         ..^ 
          |
94 | | fzofzp1 12008 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^
        |
95 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
     |
96 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
    |
97 | 96 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
   
             |
98 | 95, 97 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
    
                 |
99 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
     |
100 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
101 | 100 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
             |
102 | 99, 101 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                 |
103 | 98, 102 | rspc2v 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
                  
        
                 |
104 | 94, 29, 103 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         ..^ 
 
     
         
                      |
105 | 28, 104 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         ..^ 
                |
106 | | pm3.35 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
            |
107 | | simp2 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           
         |
108 | | xrltnsym 11436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 
                   |
109 | 46, 107, 108 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
      ..^      
       
          
             |
110 | 109 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           ..^      
       
          
            |
111 | 110 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           ..^      
       
          
          
                 |
112 | 111 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        
            ..^      
       
          
                  |
113 | 112 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        
    
      ..^       
     
           
                   |
114 | 113 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                 
      ..^       
     
           
                   |
115 | 114 | com14 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
      ..^       
     
              
      
                   |
116 | 106, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                  
  
      ..^ 
           
              
      
                   |
117 | 116 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                    
      ..^ 
           
              
      
                    |
118 | 117 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         ..^ 
                 
           
              
      
                    |
119 | 105, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
         ..^ 
                             
      
                   |
120 | 119 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      ..^       
     
              
      
                   |
121 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
122 | 121 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
     
           |
123 | 121 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
             |
124 | 122, 123 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  
                 
              |
125 | | xrltnr 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
         
    |
126 | 125 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
          
    |
127 | 126 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             
                 |
128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
              
                 |
129 | 128 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
               
        
                        |
130 | 124, 129 | syl6bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
            
                         |
131 | 130 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             
      
                  |
132 | 131 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      ..^       
     
              
      
                   |
133 | 120, 132 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . 21
         
      ..^ 
           
              
      
                   |
134 | 133 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
         ..^ 
            
     
              
      
                   |
135 | 93, 134 | sylbid 219 |
. . . . . . . . . . . . . . . . . . 19
         ..^ 

           
              
      
                   |
136 | 135 | com23 81 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
           
 
             
      
                   |
137 | 136 | com14 91 |
. . . . . . . . . . . . . . . . 17
     
                            
  
      ..^ 
                   |
138 | 23, 137 | syl6bir 233 |
. . . . . . . . . . . . . . . 16
          
            
     
 
  
      ..^ 
                    |
139 | 138 | com14 91 |
. . . . . . . . . . . . . . 15
      
            
     
               ..^ 
                    |
140 | 139 | com23 81 |
. . . . . . . . . . . . . 14
                   
           
  
      ..^ 
                    |
141 | 140 | impd 433 |
. . . . . . . . . . . . 13
       
           
       
    
         ..^ 
                   |
142 | 141 | com24 90 |
. . . . . . . . . . . 12
   
      ..^      
                  
   
   
                   |
143 | 85, 142 | jaoi 381 |
. . . . . . . . . . 11
 
          ..^      
                  
   
   
                   |
144 | 143 | com12 32 |
. . . . . . . . . 10
         ..^ 
 
                  
     
   
   
                   |
145 | 20, 144 | mpd 15 |
. . . . . . . . 9
         ..^ 
    
                  
   
   
                  |
146 | 145 | ex 436 |
. . . . . . . 8
 
       ..^            
     
     
   
   
                   |
147 | 146 | com23 81 |
. . . . . . 7
 
            ..^       
     
     
   
   
                   |
148 | 147 | rexlimdva 2879 |
. . . . . 6
              ..^             
     
   
   
                   |
149 | 13, 148 | mpd 15 |
. . . . 5
   ..^       
     
     
   
   
                  |
150 | 149 | imp 431 |
. . . 4
 
 ..^              
     
   
   
                 |
151 | 150 | com12 32 |
. . 3
                  
   
       ..^ 
                 |
152 | 1, 151 | sylbi 199 |
. 2
                
 ..^ 
                 |
153 | | ax-1 6 |
. 2
           
    
 ..^ 
                 |
154 | 152, 153 | pm2.61i 168 |
1
 
 ..^ 
                |