Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . . . . 9
   |
2 | 1 | ad2antrr 731 |
. . . . . . . 8
   
 
             |
3 | | poimirlem22.s |
. . . . . . . 8
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
4 | | poimirlem22.1 |
. . . . . . . . 9
               
       |
5 | 4 | ad2antrr 731 |
. . . . . . . 8
   
 
                                 |
6 | | simplrl 769 |
. . . . . . . 8
   
 
             |
7 | | simprl 763 |
. . . . . . . 8
   
 
                 |
8 | 2, 3, 5, 6, 7 | poimirlem10 31943 |
. . . . . . 7
   
 
               
                      |
9 | | simplrr 770 |
. . . . . . . 8
   
 
             |
10 | | simprr 765 |
. . . . . . . 8
   
 
                 |
11 | 2, 3, 5, 9, 10 | poimirlem10 31943 |
. . . . . . 7
   
 
               
                      |
12 | 8, 11 | eqtr3d 2486 |
. . . . . 6
   
 
                             |
13 | | elrabi 3192 |
. . . . . . . . . . . . . 14
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
14 | 13, 3 | eleq2s 2546 |
. . . . . . . . . . . . 13
     ..^                            |
15 | | xp1st 6820 |
. . . . . . . . . . . . 13
     ..^                                 ..^                       |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
        ..^                       |
17 | | xp2nd 6821 |
. . . . . . . . . . . 12
        ..^                                             |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
                         |
19 | | fvex 5873 |
. . . . . . . . . . . 12
         |
20 | | f1oeq1 5803 |
. . . . . . . . . . . 12
                                             |
21 | 19, 20 | elab 3184 |
. . . . . . . . . . 11
                      
                      |
22 | 18, 21 | sylib 200 |
. . . . . . . . . 10
                       |
23 | | f1ofn 5813 |
. . . . . . . . . 10
                    
              |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
               |
25 | 24 | adantr 467 |
. . . . . . . 8
 
               |
26 | 25 | ad2antlr 732 |
. . . . . . 7
   
 
                         |
27 | | elrabi 3192 |
. . . . . . . . . . . . . 14
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
28 | 27, 3 | eleq2s 2546 |
. . . . . . . . . . . . 13
     ..^                            |
29 | | xp1st 6820 |
. . . . . . . . . . . . 13
     ..^                                 ..^                       |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
        ..^                       |
31 | | xp2nd 6821 |
. . . . . . . . . . . 12
        ..^                                             |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
                         |
33 | | fvex 5873 |
. . . . . . . . . . . 12
         |
34 | | f1oeq1 5803 |
. . . . . . . . . . . 12
                                             |
35 | 33, 34 | elab 3184 |
. . . . . . . . . . 11
                      
                      |
36 | 32, 35 | sylib 200 |
. . . . . . . . . 10
                       |
37 | | f1ofn 5813 |
. . . . . . . . . 10
                    
              |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
               |
39 | 38 | adantl 468 |
. . . . . . . 8
 
               |
40 | 39 | ad2antlr 732 |
. . . . . . 7
   
 
                         |
41 | | eleq1 2516 |
. . . . . . . . . . . . 13
     
       |
42 | 41 | anbi2d 709 |
. . . . . . . . . . . 12
     
                 
  

 
                   |
43 | | oveq2 6296 |
. . . . . . . . . . . . . 14
           |
44 | 43 | imaeq2d 5167 |
. . . . . . . . . . . . 13
                                   |
45 | 43 | imaeq2d 5167 |
. . . . . . . . . . . . 13
                                   |
46 | 44, 45 | eqeq12d 2465 |
. . . . . . . . . . . 12
                                 
                                   |
47 | 42, 46 | imbi12d 322 |
. . . . . . . . . . 11
     

                                                      

                                                      |
48 | 1 | ad3antrrr 735 |
. . . . . . . . . . . . 13
    
                    |
49 | 4 | ad3antrrr 735 |
. . . . . . . . . . . . 13
    
                                        |
50 | | simpl 459 |
. . . . . . . . . . . . . 14
 
   |
51 | 50 | ad3antlr 736 |
. . . . . . . . . . . . 13
    
                    |
52 | | simplrl 769 |
. . . . . . . . . . . . 13
    
                        |
53 | | simpr 463 |
. . . . . . . . . . . . . 14
 
   |
54 | 53 | ad3antlr 736 |
. . . . . . . . . . . . 13
    
                    |
55 | | simplrr 770 |
. . . . . . . . . . . . 13
    
                        |
56 | | simpr 463 |
. . . . . . . . . . . . 13
    
                        |
57 | 48, 3, 49, 51, 52, 54, 55, 56 | poimirlem11 31944 |
. . . . . . . . . . . 12
    
                                                    |
58 | 48, 3, 49, 54, 55, 51, 52, 56 | poimirlem11 31944 |
. . . . . . . . . . . 12
    
                                                    |
59 | 57, 58 | eqssd 3448 |
. . . . . . . . . . 11
    
                                                    |
60 | 47, 59 | chvarv 2106 |
. . . . . . . . . 10
    
                                                    |
61 | | simpll 759 |
. . . . . . . . . . . . . 14
   
 
             |
62 | | elfznn 11825 |
. . . . . . . . . . . . . . . . . . 19
       |
63 | | nnm1nn0 10908 |
. . . . . . . . . . . . . . . . . . 19
     |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
65 | 64 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     

    |
66 | 62 | nncnd 10622 |
. . . . . . . . . . . . . . . . . . . 20
       |
67 | | ax-1cn 9594 |
. . . . . . . . . . . . . . . . . . . 20
 |
68 | | subeq0 9897 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
69 | 66, 67, 68 | sylancl 667 |
. . . . . . . . . . . . . . . . . . 19
           |
70 | 69 | necon3abid 2659 |
. . . . . . . . . . . . . . . . . 18
       
   |
71 | 70 | biimpar 488 |
. . . . . . . . . . . . . . . . 17
     

    |
72 | | elnnne0 10880 |
. . . . . . . . . . . . . . . . 17
  
  
     |
73 | 65, 71, 72 | sylanbrc 669 |
. . . . . . . . . . . . . . . 16
     

    |
74 | 73 | adantl 468 |
. . . . . . . . . . . . . . 15
 
    
      |
75 | 64 | nn0red 10923 |
. . . . . . . . . . . . . . . . . 18
         |
76 | 75 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
         |
77 | 62 | nnred 10621 |
. . . . . . . . . . . . . . . . . 18
       |
78 | 77 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
       |
79 | 1 | nnred 10621 |
. . . . . . . . . . . . . . . . . 18
   |
80 | 79 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
       |
81 | 77 | lem1d 10537 |
. . . . . . . . . . . . . . . . . 18
         |
82 | 81 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
         |
83 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . 18
       |
84 | 83 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
       |
85 | 76, 78, 80, 82, 84 | letrd 9789 |
. . . . . . . . . . . . . . . 16
 
         |
86 | 85 | adantrr 722 |
. . . . . . . . . . . . . . 15
 
    
      |
87 | 1 | nnzd 11036 |
. . . . . . . . . . . . . . . . 17
   |
88 | | fznn 11860 |
. . . . . . . . . . . . . . . . 17
       
         |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
            
    |
90 | 89 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
                  |
91 | 74, 86, 90 | mpbir2and 932 |
. . . . . . . . . . . . . 14
 
    
          |
92 | 61, 91 | sylan 474 |
. . . . . . . . . . . . 13
    
                 
 
        |
93 | | ovex 6316 |
. . . . . . . . . . . . . 14
   |
94 | | eleq1 2516 |
. . . . . . . . . . . . . . . 16
       
         |
95 | 94 | anbi2d 709 |
. . . . . . . . . . . . . . 15
       
                 
  

 
                     |
96 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
               |
97 | 96 | imaeq2d 5167 |
. . . . . . . . . . . . . . . 16
                                       |
98 | 96 | imaeq2d 5167 |
. . . . . . . . . . . . . . . 16
                                       |
99 | 97, 98 | eqeq12d 2465 |
. . . . . . . . . . . . . . 15
                                   
                                       |
100 | 95, 99 | imbi12d 322 |
. . . . . . . . . . . . . 14
       

                                                      

                                                            |
101 | 93, 100, 59 | vtocl 3099 |
. . . . . . . . . . . . 13
    
                                                          |
102 | 92, 101 | syldan 473 |
. . . . . . . . . . . 12
    
                 
 
                                      |
103 | 102 | expr 619 |
. . . . . . . . . . 11
    
                  
                                       |
104 | | ima0 5182 |
. . . . . . . . . . . . 13
             |
105 | | ima0 5182 |
. . . . . . . . . . . . 13
             |
106 | 104, 105 | eqtr4i 2475 |
. . . . . . . . . . . 12
                         |
107 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
       |
108 | | 1m1e0 10675 |
. . . . . . . . . . . . . . . 16
   |
109 | 107, 108 | syl6eq 2500 |
. . . . . . . . . . . . . . 15
     |
110 | 109 | oveq2d 6304 |
. . . . . . . . . . . . . 14
             |
111 | | fz10 11817 |
. . . . . . . . . . . . . 14
     |
112 | 110, 111 | syl6eq 2500 |
. . . . . . . . . . . . 13
         |
113 | 112 | imaeq2d 5167 |
. . . . . . . . . . . 12
                                 |
114 | 112 | imaeq2d 5167 |
. . . . . . . . . . . 12
                                 |
115 | 106, 113,
114 | 3eqtr4a 2510 |
. . . . . . . . . . 11
                                       |
116 | 103, 115 | pm2.61d2 164 |
. . . . . . . . . 10
    
                                                        |
117 | 60, 116 | difeq12d 3551 |
. . . . . . . . 9
    
                                                                                            |
118 | | fnsnfv 5923 |
. . . . . . . . . . . 12
                                                 |
119 | 24, 118 | sylan 474 |
. . . . . . . . . . 11
 
                                   |
120 | 62 | adantl 468 |
. . . . . . . . . . . . 13
 
       |
121 | | uncom 3577 |
. . . . . . . . . . . . . . . 16
                     |
122 | 121 | difeq1i 3546 |
. . . . . . . . . . . . . . 15
                                     |
123 | | difun2 3846 |
. . . . . . . . . . . . . . 15
                             |
124 | 122, 123 | eqtri 2472 |
. . . . . . . . . . . . . 14
                             |
125 | | nncn 10614 |
. . . . . . . . . . . . . . . . . . 19
   |
126 | | npcan1 10041 |
. . . . . . . . . . . . . . . . . . 19
       |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
128 | | elnnuz 11192 |
. . . . . . . . . . . . . . . . . . 19

      |
129 | 128 | biimpi 198 |
. . . . . . . . . . . . . . . . . 18
       |
130 | 127, 129 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . 17
           |
131 | 63 | nn0zd 11035 |
. . . . . . . . . . . . . . . . . . . 20
     |
132 | | uzid 11170 |
. . . . . . . . . . . . . . . . . . . 20
             |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
           |
134 | | peano2uz 11209 |
. . . . . . . . . . . . . . . . . . 19
        
            |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
             |
136 | 127, 135 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . 17
         |
137 | | fzsplit2 11821 |
. . . . . . . . . . . . . . . . 17
                
                      |
138 | 130, 136,
137 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
                       |
139 | 127 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
               |
140 | | nnz 10956 |
. . . . . . . . . . . . . . . . . . 19
   |
141 | | fzsn 11837 |
. . . . . . . . . . . . . . . . . . 19
         |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
143 | 139, 142 | eqtrd 2484 |
. . . . . . . . . . . . . . . . 17
             |
144 | 143 | uneq2d 3587 |
. . . . . . . . . . . . . . . 16
                             |
145 | 138, 144 | eqtrd 2484 |
. . . . . . . . . . . . . . 15
                 |
146 | 145 | difeq1d 3549 |
. . . . . . . . . . . . . 14
     
                 
         |
147 | | nnre 10613 |
. . . . . . . . . . . . . . . 16
   |
148 | | ltm1 10442 |
. . . . . . . . . . . . . . . . . 18
     |
149 | | peano2rem 9938 |
. . . . . . . . . . . . . . . . . . 19
     |
150 | | ltnle 9710 |
. . . . . . . . . . . . . . . . . . 19
   
   
     |
151 | 149, 150 | mpancom 674 |
. . . . . . . . . . . . . . . . . 18
   
     |
152 | 148, 151 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
     |
153 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . 17
           |
154 | 152, 153 | nsyl 125 |
. . . . . . . . . . . . . . . 16

        |
155 | 147, 154 | syl 17 |
. . . . . . . . . . . . . . 15

        |
156 | | incom 3624 |
. . . . . . . . . . . . . . . . 17
                     |
157 | 156 | eqeq1i 2455 |
. . . . . . . . . . . . . . . 16
                       |
158 | | disjsn 4031 |
. . . . . . . . . . . . . . . 16
          
        |
159 | | disj3 3808 |
. . . . . . . . . . . . . . . 16
                         |
160 | 157, 158,
159 | 3bitr3i 279 |
. . . . . . . . . . . . . . 15
      
 
            |
161 | 155, 160 | sylib 200 |
. . . . . . . . . . . . . 14
  
            |
162 | 124, 146,
161 | 3eqtr4a 2510 |
. . . . . . . . . . . . 13
     
           |
163 | 120, 162 | syl 17 |
. . . . . . . . . . . 12
 
                     |
164 | 163 | imaeq2d 5167 |
. . . . . . . . . . 11
 
                    
                        |
165 | | dff1o3 5818 |
. . . . . . . . . . . . . . 15
                                         
            |
166 | 165 | simprbi 466 |
. . . . . . . . . . . . . 14
                    
           |
167 | 22, 166 | syl 17 |
. . . . . . . . . . . . 13
            |
168 | | imadif 5656 |
. . . . . . . . . . . . 13
                         
                                              |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . 12
                                                               |
170 | 169 | adantr 467 |
. . . . . . . . . . 11
 
                    
                                              |
171 | 119, 164,
170 | 3eqtr2d 2490 |
. . . . . . . . . 10
 
                                                         |
172 | 6, 171 | sylan 474 |
. . . . . . . . 9
    
                                                                      |
173 | | eleq1 2516 |
. . . . . . . . . . . . 13
 
   |
174 | 173 | anbi1d 710 |
. . . . . . . . . . . 12
  
     
        |
175 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
176 | 175 | fveq2d 5867 |
. . . . . . . . . . . . . . 15
                   |
177 | 176 | fveq1d 5865 |
. . . . . . . . . . . . . 14
                           |
178 | 177 | sneqd 3979 |
. . . . . . . . . . . . 13
                               |
179 | 176 | imaeq1d 5166 |
. . . . . . . . . . . . . 14
                                   |
180 | 176 | imaeq1d 5166 |
. . . . . . . . . . . . . 14
                                       |
181 | 179, 180 | difeq12d 3551 |
. . . . . . . . . . . . 13
                                                                           |
182 | 178, 181 | eqeq12d 2465 |
. . . . . . . . . . . 12
                                                                                                         |
183 | 174, 182 | imbi12d 322 |
. . . . . . . . . . 11
                                                                                                                         |
184 | 183, 171 | chvarv 2106 |
. . . . . . . . . 10
 
                                                         |
185 | 9, 184 | sylan 474 |
. . . . . . . . 9
    
                                                                      |
186 | 117, 172,
185 | 3eqtr4d 2494 |
. . . . . . . 8
    
                                                |
187 | | fvex 5873 |
. . . . . . . . 9
             |
188 | 187 | sneqr 4138 |
. . . . . . . 8
                                                       |
189 | 186, 188 | syl 17 |
. . . . . . 7
    
                                            |
190 | 26, 40, 189 | eqfnfvd 5977 |
. . . . . 6
   
 
                             |
191 | | xpopth 6829 |
. . . . . . . 8
         ..^                            ..^                                                                    |
192 | 16, 30, 191 | syl2an 480 |
. . . . . . 7
 
                                               |
193 | 192 | ad2antlr 732 |
. . . . . 6
   
 
                                                         |
194 | 12, 190, 193 | mpbi2and 931 |
. . . . 5
   
 
                     |
195 | | eqtr3 2471 |
. . . . . 6
                     |
196 | 195 | adantl 468 |
. . . . 5
   
 
                     |
197 | | xpopth 6829 |
. . . . . . 7
      ..^                              ..^                          
                  
   |
198 | 14, 28, 197 | syl2an 480 |
. . . . . 6
 
                   
   |
199 | 198 | ad2antlr 732 |
. . . . 5
   
 
                             
   |
200 | 194, 196,
199 | mpbi2and 931 |
. . . 4
   
 
             |
201 | 200 | ex 436 |
. . 3
 

                |
202 | 201 | ralrimivva 2808 |
. 2
  
              |
203 | | fveq2 5863 |
. . . 4
           |
204 | 203 | eqeq1d 2452 |
. . 3
             |
205 | 204 | rmo4 3230 |
. 2
     


              |
206 | 202, 205 | sylibr 216 |
1
        |