Step | Hyp | Ref
| Expression |
1 | | poimirlem3.4 |
. . . . . . . . . . . . . . 15
          ..^   |
2 | | ffn 5733 |
. . . . . . . . . . . . . . 15
          ..^       |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . 14
       |
4 | 3 | adantr 467 |
. . . . . . . . . . . . 13
 
           |
5 | | 1ex 9643 |
. . . . . . . . . . . . . . . . 17
 |
6 | | fnconstg 5776 |
. . . . . . . . . . . . . . . . 17
                       |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
                     |
8 | | c0ex 9642 |
. . . . . . . . . . . . . . . . 17
 |
9 | | fnconstg 5776 |
. . . . . . . . . . . . . . . . 17
                           |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
                         |
11 | 7, 10 | pm3.2i 457 |
. . . . . . . . . . . . . . 15
                                               |
12 | | poimirlem3.5 |
. . . . . . . . . . . . . . . . 17
               |
13 | | dff1o3 5825 |
. . . . . . . . . . . . . . . . . 18
                              |
14 | 13 | simprbi 466 |
. . . . . . . . . . . . . . . . 17
            
   |
15 | | imain 5664 |
. . . . . . . . . . . . . . . . 17
 
                                      |
16 | 12, 14, 15 | 3syl 18 |
. . . . . . . . . . . . . . . 16
        
                              |
17 | | elfznn0 11894 |
. . . . . . . . . . . . . . . . . . . . 21
       |
18 | 17 | nn0red 10933 |
. . . . . . . . . . . . . . . . . . . 20
       |
19 | 18 | ltp1d 10544 |
. . . . . . . . . . . . . . . . . . 19
         |
20 | | fzdisj 11833 |
. . . . . . . . . . . . . . . . . . 19
       
         |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         
         |
22 | 21 | imaeq2d 5171 |
. . . . . . . . . . . . . . . . 17
                           |
23 | | ima0 5186 |
. . . . . . . . . . . . . . . . 17
     |
24 | 22, 23 | syl6eq 2503 |
. . . . . . . . . . . . . . . 16
                       |
25 | 16, 24 | sylan9req 2508 |
. . . . . . . . . . . . . . 15
 
                           |
26 | | fnun 5687 |
. . . . . . . . . . . . . . 15
                                                                                                                       |
27 | 11, 25, 26 | sylancr 670 |
. . . . . . . . . . . . . 14
 
                                                       |
28 | | imaundi 5251 |
. . . . . . . . . . . . . . . 16
                                     |
29 | | nn0p1nn 10916 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
30 | | nnuz 11201 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
31 | 29, 30 | syl6eleq 2541 |
. . . . . . . . . . . . . . . . . . . . 21

        |
32 | 17, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
             |
33 | | elfzuz3 11804 |
. . . . . . . . . . . . . . . . . . . 20
           |
34 | | fzsplit2 11831 |
. . . . . . . . . . . . . . . . . . . 20
            
                  |
35 | 32, 33, 34 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
                       |
36 | 35 | eqcomd 2459 |
. . . . . . . . . . . . . . . . . 18
                       |
37 | 36 | imaeq2d 5171 |
. . . . . . . . . . . . . . . . 17
                               |
38 | | f1ofo 5826 |
. . . . . . . . . . . . . . . . . 18
            
              |
39 | | foima 5803 |
. . . . . . . . . . . . . . . . . 18
                           |
40 | 12, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
               |
41 | 37, 40 | sylan9eqr 2509 |
. . . . . . . . . . . . . . . 16
 
                           |
42 | 28, 41 | syl5eqr 2501 |
. . . . . . . . . . . . . . 15
 
                               |
43 | 42 | fneq2d 5672 |
. . . . . . . . . . . . . 14
 
                                                     
                                   |
44 | 27, 43 | mpbid 214 |
. . . . . . . . . . . . 13
 
                                       |
45 | | ovex 6323 |
. . . . . . . . . . . . . 14
     |
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
 
           |
47 | | inidm 3643 |
. . . . . . . . . . . . 13
               |
48 | | eqidd 2454 |
. . . . . . . . . . . . 13
                       |
49 | | eqidd 2454 |
. . . . . . . . . . . . 13
                                                                               |
50 | 4, 44, 46, 46, 47, 48, 49 | offval 6543 |
. . . . . . . . . . . 12
 
                                                                                  |
51 | | poimirlem4.2 |
. . . . . . . . . . . . . . . . . . . 20
   |
52 | | nn0p1nn 10916 |
. . . . . . . . . . . . . . . . . . . 20

    |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     |
54 | 53 | nnzd 11046 |
. . . . . . . . . . . . . . . . . 18
     |
55 | | uzid 11180 |
. . . . . . . . . . . . . . . . . 18
   
    
    |
56 | | peano2uz 11219 |
. . . . . . . . . . . . . . . . . 18
      
 
 
          |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
        
    |
58 | | poimirlem4.3 |
. . . . . . . . . . . . . . . . . 18
   |
59 | 51 | nn0zd 11045 |
. . . . . . . . . . . . . . . . . . 19
   |
60 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . 20
   |
61 | 60 | nnzd 11046 |
. . . . . . . . . . . . . . . . . . 19
   |
62 | | zltp1le 10993 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
63 | | peano2z 10985 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
64 | | eluz 11179 |
. . . . . . . . . . . . . . . . . . . . 21
   
       
     |
65 | 63, 64 | sylan 474 |
. . . . . . . . . . . . . . . . . . . 20
 
       
     |
66 | 62, 65 | bitr4d 260 |
. . . . . . . . . . . . . . . . . . 19
 
     
     |
67 | 59, 61, 66 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
     
     |
68 | 58, 67 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
    
    |
69 | | fzsplit2 11831 |
. . . . . . . . . . . . . . . . 17
         
        
 
                        |
70 | 57, 68, 69 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                           |
71 | | fzsn 11847 |
. . . . . . . . . . . . . . . . . 18
                 |
72 | 54, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
      
        |
73 | 72 | uneq1d 3589 |
. . . . . . . . . . . . . . . 16
                                   |
74 | 70, 73 | eqtrd 2487 |
. . . . . . . . . . . . . . 15
                       |
75 | 74 | xpeq1d 4860 |
. . . . . . . . . . . . . 14
                               |
76 | | xpundir 4891 |
. . . . . . . . . . . . . . 15
                                         |
77 | | ovex 6323 |
. . . . . . . . . . . . . . . . 17
   |
78 | 77, 8 | xpsn 6071 |
. . . . . . . . . . . . . . . 16
                |
79 | 78 | uneq1i 3586 |
. . . . . . . . . . . . . . 15
                             
              |
80 | 76, 79 | eqtri 2475 |
. . . . . . . . . . . . . 14
                     
                  |
81 | 75, 80 | syl6eq 2503 |
. . . . . . . . . . . . 13
              
                   |
82 | 81 | adantr 467 |
. . . . . . . . . . . 12
 
                                      |
83 | 50, 82 | uneq12d 3591 |
. . . . . . . . . . 11
 
                                                                                                
                    |
84 | | unass 3593 |
. . . . . . . . . . 11
                                                                                                                   
                   |
85 | 83, 84 | syl6eqr 2505 |
. . . . . . . . . 10
 
                                                                                                                     |
86 | 51 | nn0red 10933 |
. . . . . . . . . . . . . . . . . . . . 21
   |
87 | 86 | ltp1d 10544 |
. . . . . . . . . . . . . . . . . . . 20
     |
88 | 53 | nnred 10631 |
. . . . . . . . . . . . . . . . . . . . 21
     |
89 | 86, 88 | ltnled 9787 |
. . . . . . . . . . . . . . . . . . . 20
  
  
   |
90 | 87, 89 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
     |
91 | | elfzle2 11810 |
. . . . . . . . . . . . . . . . . . 19
       
   |
92 | 90, 91 | nsyl 125 |
. . . . . . . . . . . . . . . . . 18
         |
93 | | disjsn 4034 |
. . . . . . . . . . . . . . . . . 18
     
 
   
       |
94 | 92, 93 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
             |
95 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . 19
               |
96 | 77, 8 | fsn 6066 |
. . . . . . . . . . . . . . . . . . 19
                 
  
             |
97 | 95, 96 | mpbir 213 |
. . . . . . . . . . . . . . . . . 18
                  |
98 | | fun 5751 |
. . . . . . . . . . . . . . . . . 18
            ..^   
                   
 
                             ..^      |
99 | 97, 98 | mpanl2 688 |
. . . . . . . . . . . . . . . . 17
           ..^           
   
                     ..^      |
100 | 1, 94, 99 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                          ..^      |
101 | | 1z 10974 |
. . . . . . . . . . . . . . . . . . 19
 |
102 | | nn0uz 11200 |
. . . . . . . . . . . . . . . . . . . . 21
     |
103 | | 1m1e0 10685 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
104 | 103 | fveq2i 5873 |
. . . . . . . . . . . . . . . . . . . . 21
           |
105 | 102, 104 | eqtr4i 2478 |
. . . . . . . . . . . . . . . . . . . 20
       |
106 | 51, 105 | syl6eleq 2541 |
. . . . . . . . . . . . . . . . . . 19
         |
107 | | fzsuc2 11860 |
. . . . . . . . . . . . . . . . . . 19
 
          
              |
108 | 101, 106,
107 | sylancr 670 |
. . . . . . . . . . . . . . . . . 18
    
              |
109 | 108 | eqcomd 2459 |
. . . . . . . . . . . . . . . . 17
              
    |
110 | | poimirlem4.1 |
. . . . . . . . . . . . . . . . . . . 20
   |
111 | | lbfzo0 11962 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
112 | 110, 111 | sylibr 216 |
. . . . . . . . . . . . . . . . . . 19
  ..^   |
113 | 112 | snssd 4120 |
. . . . . . . . . . . . . . . . . 18
    ..^   |
114 | | ssequn2 3609 |
. . . . . . . . . . . . . . . . . 18
    ..^
  ..^     ..^   |
115 | 113, 114 | sylib 200 |
. . . . . . . . . . . . . . . . 17
   ..^     ..^   |
116 | 109, 115 | feq23d 5728 |
. . . . . . . . . . . . . . . 16
                           ..^                        ..^    |
117 | 100, 116 | mpbid 214 |
. . . . . . . . . . . . . . 15
                     ..^   |
118 | | ffn 5733 |
. . . . . . . . . . . . . . 15
                     ..^ 
  
             |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . 14
                  |
120 | 119 | adantr 467 |
. . . . . . . . . . . . 13
 
     
  
             |
121 | | fnconstg 5776 |
. . . . . . . . . . . . . . . . 17
                                             |
122 | 5, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
                                           |
123 | | fnconstg 5776 |
. . . . . . . . . . . . . . . . 17
                                                     |
124 | 8, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
                                                   |
125 | 122, 124 | pm3.2i 457 |
. . . . . . . . . . . . . . 15
                                                
                         
                    |
126 | 77, 77 | f1osn 5857 |
. . . . . . . . . . . . . . . . . . 19
                      |
127 | | f1oun 5838 |
. . . . . . . . . . . . . . . . . . 19
                 
                                  
 
     
  
                                 |
128 | 126, 127 | mpanl2 688 |
. . . . . . . . . . . . . . . . . 18
                        
    
 
     
  
                                 |
129 | 12, 94, 94, 128 | syl12anc 1267 |
. . . . . . . . . . . . . . . . 17
                                      |
130 | | dff1o3 5825 |
. . . . . . . . . . . . . . . . . 18
                                   
 
  
                                              |
131 | 130 | simprbi 466 |
. . . . . . . . . . . . . . . . 17
                                                  |
132 | | imain 5664 |
. . . . . . . . . . . . . . . . 17
                               
                                  
                     |
133 | 129, 131,
132 | 3syl 18 |
. . . . . . . . . . . . . . . 16
                   
                                  
                     |
134 | | fzdisj 11833 |
. . . . . . . . . . . . . . . . . . 19
       
           |
135 | 19, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         
           |
136 | 135 | imaeq2d 5171 |
. . . . . . . . . . . . . . . . 17
                       
                           |
137 | | ima0 5186 |
. . . . . . . . . . . . . . . . 17
                |
138 | 136, 137 | syl6eq 2503 |
. . . . . . . . . . . . . . . 16
                       
            |
139 | 133, 138 | sylan9req 2508 |
. . . . . . . . . . . . . . 15
 
                             
                     |
140 | | fnun 5687 |
. . . . . . . . . . . . . . 15
                              
                   
                         
                                                                                                                         
                                        |
141 | 125, 139,
140 | sylancr 670 |
. . . . . . . . . . . . . 14
 
           
                                                                     
                     |
142 | | f1ofo 5826 |
. . . . . . . . . . . . . . . . . . 19
                                    
  
                                 |
143 | | foima 5803 |
. . . . . . . . . . . . . . . . . . 19
                                                                         |
144 | 129, 142,
143 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
                                      |
145 | 108 | imaeq2d 5171 |
. . . . . . . . . . . . . . . . . 18
                          
                      |
146 | 144, 145,
108 | 3eqtr4d 2497 |
. . . . . . . . . . . . . . . . 17
                              |
147 | | peano2uz 11219 |
. . . . . . . . . . . . . . . . . . . 20
    
        |
148 | 33, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     
       |
149 | | fzsplit2 11831 |
. . . . . . . . . . . . . . . . . . 19
        
                            |
150 | 32, 148, 149 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                           |
151 | 150 | imaeq2d 5171 |
. . . . . . . . . . . . . . . . 17
                              
                   
      |
152 | 146, 151 | sylan9req 2508 |
. . . . . . . . . . . . . . . 16
 
                                          |
153 | | imaundi 5251 |
. . . . . . . . . . . . . . . 16
                        
         
                                       |
154 | 152, 153 | syl6eq 2503 |
. . . . . . . . . . . . . . 15
 
                
                                        |
155 | 154 | fneq2d 5672 |
. . . . . . . . . . . . . 14
 
                                                               
                                                         
                                         |
156 | 141, 155 | mpbird 236 |
. . . . . . . . . . . . 13
 
           
                                                     |
157 | | ovex 6323 |
. . . . . . . . . . . . . 14
       |
158 | 157 | a1i 11 |
. . . . . . . . . . . . 13
 
             |
159 | | inidm 3643 |
. . . . . . . . . . . . 13
                 
   |
160 | | eqidd 2454 |
. . . . . . . . . . . . 13
           
                               |
161 | | eqidd 2454 |
. . . . . . . . . . . . 13
           
                                                                                                                     |
162 | 120, 156,
158, 158, 159, 160, 161 | offval 6543 |
. . . . . . . . . . . 12
 
                                                                         
                                                                            |
163 | 77 | a1i 11 |
. . . . . . . . . . . . 13
 
     
   |
164 | 8 | a1i 11 |
. . . . . . . . . . . . 13
 
       |
165 | 109 | adantr 467 |
. . . . . . . . . . . . 13
 
                       |
166 | | fveq2 5870 |
. . . . . . . . . . . . . . . . 17
                                 |
167 | 77 | snid 3998 |
. . . . . . . . . . . . . . . . . . . 20
       |
168 | 77, 8 | fnsn 5638 |
. . . . . . . . . . . . . . . . . . . . 21
            |
169 | | fvun2 5942 |
. . . . . . . . . . . . . . . . . . . . 21
            
 
       
 
                       
                 |
170 | 168, 169 | mp3an2 1354 |
. . . . . . . . . . . . . . . . . . . 20
                

                   
                 |
171 | 167, 170 | mpanr2 691 |
. . . . . . . . . . . . . . . . . . 19
                
                  
      
    |
172 | 3, 94, 171 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
             
                 |
173 | 77, 8 | fvsn 6102 |
. . . . . . . . . . . . . . . . . 18
              |
174 | 172, 173 | syl6eq 2503 |
. . . . . . . . . . . . . . . . 17
             
    |
175 | 166, 174 | sylan9eqr 2509 |
. . . . . . . . . . . . . . . 16
 

                 |
176 | 175 | adantlr 722 |
. . . . . . . . . . . . . . 15
                          |
177 | | fveq2 5870 |
. . . . . . . . . . . . . . . 16
                                                                                                                  
    |
178 | | imadmrn 5181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
                      |
179 | 77, 77 | xpsn 6071 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                    |
180 | 179 | imaeq1i 5168 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
                                   |
181 | | dmxpid 5057 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
182 | 181 | imaeq2i 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                         |
183 | 180, 182 | eqtri 2475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
                             |
184 | | rnxpid 5273 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
185 | 178, 183,
184 | 3eqtr3ri 2484 |
. . . . . . . . . . . . . . . . . . . . . . 23
                      |
186 | | eluzp1p1 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
          |
187 | | eluzfz2 11814 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
       
    |
188 | 33, 186, 187 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
           |
189 | 188 | snssd 4120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
          |
190 | | imass2 5207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                               
     |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                             |
192 | 185, 191 | syl5eqss 3478 |
. . . . . . . . . . . . . . . . . . . . . 22
        
                       |
193 | | ssel 3428 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                    
      |
194 | 192, 167,
193 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . 21
     
                  
     |
195 | | elun2 3604 |
. . . . . . . . . . . . . . . . . . . . 21
                    
   
                 
             
      |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     
                 
             
      |
197 | | imaundir 5252 |
. . . . . . . . . . . . . . . . . . . 20
                                
                          |
198 | 196, 197 | syl6eleqr 2542 |
. . . . . . . . . . . . . . . . . . 19
     
     
                    |
199 | 198 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
     
     
                    |
200 | | fvun2 5942 |
. . . . . . . . . . . . . . . . . . 19
       
                     
                   
                         
                                                                                         
       
                                                                                
    |
201 | 122, 124,
200 | mp3an12 1356 |
. . . . . . . . . . . . . . . . . 18
       
                                                                                                                       
        
                            |
202 | 139, 199,
201 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
                                                                                             
    |
203 | 8 | fvconst2 6125 |
. . . . . . . . . . . . . . . . . . 19
       
                                                     |
204 | 198, 203 | syl 17 |
. . . . . . . . . . . . . . . . . 18
           
                            |
205 | 204 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
           
                            |
206 | 202, 205 | eqtrd 2487 |
. . . . . . . . . . . . . . . 16
 
                                                                 |
207 | 177, 206 | sylan9eqr 2509 |
. . . . . . . . . . . . . . 15
                                                                     |
208 | 176, 207 | oveq12d 6313 |
. . . . . . . . . . . . . 14
                
                                                                     |
209 | | 00id 9813 |
. . . . . . . . . . . . . 14
   |
210 | 208, 209 | syl6eq 2503 |
. . . . . . . . . . . . 13
                
                                                                   |
211 | 163, 164,
165, 210 | fmptapd 6093 |
. . . . . . . . . . . 12
 
                
                                                                    
         
                                                                            |
212 | 3, 94 | jca 535 |
. . . . . . . . . . . . . . . . 17
                   |
213 | | fvun1 5941 |
. . . . . . . . . . . . . . . . . . 19
            
 
       
 
        
 
  
              |
214 | 168, 213 | mp3an2 1354 |
. . . . . . . . . . . . . . . . . 18
                
                         |
215 | 214 | anassrs 654 |
. . . . . . . . . . . . . . . . 17
                 
                        |
216 | 212, 215 | sylan 474 |
. . . . . . . . . . . . . . . 16
 
                        |
217 | 216 | adantlr 722 |
. . . . . . . . . . . . . . 15
                                |
218 | | fvres 5884 |
. . . . . . . . . . . . . . . . 17
                                                                          
                                                  |
219 | 218 | eqcomd 2459 |
. . . . . . . . . . . . . . . 16
                                                                     
                                            
          |
220 | | resundir 5122 |
. . . . . . . . . . . . . . . . . 18
       
                                            
                             
                                        |
221 | | relxp 4945 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
222 | | dmxpss 5271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
         |
223 | | imassrn 5182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
224 | 222, 223 | sstri 3443 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
 |
225 | | f1of 5819 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
              |
226 | | frn 5740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
      |
227 | 12, 225, 226 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
228 | 224, 227 | syl5ss 3445 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
229 | | relssres 5145 |
. . . . . . . . . . . . . . . . . . . . . . 23
                         
                 
                   |
230 | 221, 228,
229 | sylancr 670 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 |
231 | 230 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
                                     |
232 | | imassrn 5182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
233 | 77 | rnsnop 5320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
 
   |
234 | 232, 233 | sseqtri 3466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                      |
235 | | ssrin 3659 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                         |
236 | 234, 235 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                  |
237 | | incom 3627 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                     |
238 | 237, 94 | syl5eq 2499 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
239 | 236, 238 | syl5sseq 3482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                          |
240 | | ss0 3767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                 
                         |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
242 | | fnconstg 5776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                   
               |
243 | | fnresdisj 5691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                   
                                    
                     
        |
244 | 5, 242, 243 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                 
                     
       |
245 | 241, 244 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . 22
                              |
246 | 245 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
                                  |
247 | 231, 246 | uneq12d 3591 |
. . . . . . . . . . . . . . . . . . . 20
 
                                                                    |
248 | | imaundir 5252 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                               |
249 | 248 | xpeq1i 4857 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                       |
250 | | xpundir 4891 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                   |
251 | 249, 250 | eqtri 2475 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                           |
252 | 251 | reseq1i 5104 |
. . . . . . . . . . . . . . . . . . . . 21
                       
                                               |
253 | | resundir 5122 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                         |
254 | 252, 253 | eqtr2i 2476 |
. . . . . . . . . . . . . . . . . . . 20
                                                                             |
255 | | un0 3761 |
. . . . . . . . . . . . . . . . . . . 20
                           |
256 | 247, 254,
255 | 3eqtr3g 2510 |
. . . . . . . . . . . . . . . . . . 19
 
           
                                    |
257 | | f1odm 5823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            
      |
258 | 12, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
259 | 258 | ineq2d 3636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                           |
260 | 259 | reseq2d 5108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
    
                 |
261 | | f1orel 5822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
  |
262 | | resindm 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

            
           |
263 | 12, 261, 262 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
    
           |
264 | 260, 263 | eqtr3d 2489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
              
     |
265 | 35 | ineq2d 3636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           
                               |
266 | | fzssp1 11848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
   |
267 | | dfss1 3639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
                        |
268 | 266, 267 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       |
269 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
                 |
270 | | incom 3627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                             |
271 | 270, 135 | syl5eq 2499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
         |
272 | 269, 271 | uneq12d 3591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                               |
273 | | uncom 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
                                             
           |
274 | | indi 3691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                           
           |
275 | 273, 274 | eqtr4i 2478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
                                               |
276 | | un0 3761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               |
277 | 272, 275,
276 | 3eqtr3g 2510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           
                       |
278 | 265, 277 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
               |
279 | 278 | reseq2d 5108 |