Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
   |
2 | | poimirlem22.s |
. . 3
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
3 | | poimirlem22.1 |
. . 3
               
       |
4 | | poimirlem22.2 |
. . 3
   |
5 | | poimirlem22.3 |
. . 3
 
             |
6 | | poimirlem21.4 |
. . 3
       |
7 | 1, 2, 3, 4, 5, 6 | poimirlem20 32024 |
. 2
    |
8 | 6 | adantr 472 |
. . . . . . . 8
 
       |
9 | 1 | nnred 10646 |
. . . . . . . . . . . . . . . 16
   |
10 | 9 | ltm1d 10561 |
. . . . . . . . . . . . . . 15
     |
11 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . . . . 18
 
   |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
     |
13 | 12 | nn0red 10950 |
. . . . . . . . . . . . . . . 16
     |
14 | 13, 9 | ltnled 9799 |
. . . . . . . . . . . . . . 15
   
     |
15 | 10, 14 | mpbid 215 |
. . . . . . . . . . . . . 14
 
   |
16 | | elfzle2 11829 |
. . . . . . . . . . . . . 14
           |
17 | 15, 16 | nsyl 125 |
. . . . . . . . . . . . 13
         |
18 | | eleq1 2537 |
. . . . . . . . . . . . . 14
               
   
     |
19 | 18 | notbid 301 |
. . . . . . . . . . . . 13
               
   
     |
20 | 17, 19 | syl5ibrcom 230 |
. . . . . . . . . . . 12
                   |
21 | 20 | necon2ad 2658 |
. . . . . . . . . . 11
                   |
22 | 21 | adantr 472 |
. . . . . . . . . 10
 
                   |
23 | 1 | ad2antrr 740 |
. . . . . . . . . . . . . 14
           
     |
24 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
25 | 24 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
       |
26 | 25 | ifbid 3894 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
27 | 26 | csbeq1d 3356 |
. . . . . . . . . . . . . . . . . . . 20
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
28 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
29 | 28 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
30 | 28 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
31 | 30 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                   |
32 | 31 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                           |
33 | 30 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                       |
34 | 33 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                               |
35 | 32, 34 | uneq12d 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                                                           |
36 | 29, 35 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                                                 |
37 | 36 | csbeq2dv 3785 |
. . . . . . . . . . . . . . . . . . . 20
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
38 | 27, 37 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
39 | 38 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . 18
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
40 | 39 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . 17
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
41 | 40, 2 | elrab2 3186 |
. . . . . . . . . . . . . . . 16

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
42 | 41 | simprbi 471 |
. . . . . . . . . . . . . . 15
     
               ![]_ ]_](_urbrack.gif)                                                           |
43 | 42 | ad2antlr 741 |
. . . . . . . . . . . . . 14
           
       
               ![]_ ]_](_urbrack.gif)                                                           |
44 | | elrabi 3181 |
. . . . . . . . . . . . . . . . . . . 20
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
45 | 44, 2 | eleq2s 2567 |
. . . . . . . . . . . . . . . . . . 19
     ..^                            |
46 | | xp1st 6842 |
. . . . . . . . . . . . . . . . . . 19
     ..^                                 ..^                       |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
        ..^                       |
48 | | xp1st 6842 |
. . . . . . . . . . . . . . . . . 18
        ..^                               ..^        |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
           ..^        |
50 | | elmapi 7511 |
. . . . . . . . . . . . . . . . 17
           ..^                       ..^   |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
                  ..^   |
52 | | elfzoelz 11947 |
. . . . . . . . . . . . . . . . 17
  ..^
  |
53 | 52 | ssriv 3422 |
. . . . . . . . . . . . . . . 16
 ..^  |
54 | | fss 5749 |
. . . . . . . . . . . . . . . 16
                   ..^  ..^ 
                  |
55 | 51, 53, 54 | sylancl 675 |
. . . . . . . . . . . . . . 15
                   |
56 | 55 | ad2antlr 741 |
. . . . . . . . . . . . . 14
           
                     |
57 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . 17
        ..^                                             |
58 | 47, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
                         |
59 | | fvex 5889 |
. . . . . . . . . . . . . . . . 17
         |
60 | | f1oeq1 5818 |
. . . . . . . . . . . . . . . . 17
                                             |
61 | 59, 60 | elab 3173 |
. . . . . . . . . . . . . . . 16
                      
                      |
62 | 58, 61 | sylib 201 |
. . . . . . . . . . . . . . 15
                       |
63 | 62 | ad2antlr 741 |
. . . . . . . . . . . . . 14
           
                         |
64 | | simpr 468 |
. . . . . . . . . . . . . 14
           
          
    |
65 | 23, 43, 56, 63, 64 | poimirlem1 32005 |
. . . . . . . . . . . . 13
           
   
                                 |
66 | 1 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
          
              |
67 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
68 | 67 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   
       |
69 | 68 | ifbid 3894 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
70 | 69 | csbeq1d 3356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
71 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
72 | 71 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
73 | 71 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
74 | 73 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                   |
75 | 74 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                           |
76 | 73 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                       |
77 | 76 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                               |
78 | 75, 77 | uneq12d 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                                                           |
79 | 72, 78 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                                                                                 |
80 | 79 | csbeq2dv 3785 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
81 | 70, 80 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . 23
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
82 | 81 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . . . . . 22
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
83 | 82 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
84 | 83, 2 | elrab2 3186 |
. . . . . . . . . . . . . . . . . . . 20

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
85 | 84 | simprbi 471 |
. . . . . . . . . . . . . . . . . . 19
     
               ![]_ ]_](_urbrack.gif)                                                           |
86 | 4, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                     ![]_ ]_](_urbrack.gif)                                                           |
87 | 86 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
          
                
               ![]_ ]_](_urbrack.gif)                                                           |
88 | | elrabi 3181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
89 | 88, 2 | eleq2s 2567 |
. . . . . . . . . . . . . . . . . . . . . . 23
     ..^                            |
90 | 4, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
     ..^                            |
91 | | xp1st 6842 |
. . . . . . . . . . . . . . . . . . . . . 22
     ..^                                 ..^                       |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
        ..^                       |
93 | | xp1st 6842 |
. . . . . . . . . . . . . . . . . . . . 21
        ..^                               ..^        |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
           ..^        |
95 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . . . 20
           ..^                       ..^   |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                  ..^   |
97 | | fss 5749 |
. . . . . . . . . . . . . . . . . . 19
                   ..^  ..^ 
                  |
98 | 96, 53, 97 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
                   |
99 | 98 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
          
                              |
100 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . 20
        ..^                                             |
101 | 92, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                         |
102 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . 20
         |
103 | | f1oeq1 5818 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
104 | 102, 103 | elab 3173 |
. . . . . . . . . . . . . . . . . . 19
                      
                      |
105 | 101, 104 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
                       |
106 | 105 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
          
                                  |
107 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
          
                   
    |
108 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . 20
     ..^                                    |
109 | 90, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
           |
110 | 109 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
          
          |
111 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . 19
                
        
           |
112 | 111 | biimpri 211 |
. . . . . . . . . . . . . . . . . 18
                                     |
113 | 110, 112 | sylan 479 |
. . . . . . . . . . . . . . . . 17
          
                              |
114 | 66, 87, 99, 106, 107, 113 | poimirlem2 32006 |
. . . . . . . . . . . . . . . 16
          
            
                                 |
115 | 114 | ex 441 |
. . . . . . . . . . . . . . 15
 
          
        
                                   |
116 | 115 | necon1bd 2661 |
. . . . . . . . . . . . . 14
 
          
 
                              
           |
117 | 116 | adantlr 729 |
. . . . . . . . . . . . 13
           
                                   
           |
118 | 65, 117 | mpd 15 |
. . . . . . . . . . . 12
           
             |
119 | 118 | neeq1d 2702 |
. . . . . . . . . . 11
           
       
       |
120 | 119 | exbiri 634 |
. . . . . . . . . 10
 
                         |
121 | 22, 120 | mpdd 40 |
. . . . . . . . 9
 
                   |
122 | 121 | necon2bd 2659 |
. . . . . . . 8
 
                   |
123 | 8, 122 | mpd 15 |
. . . . . . 7
 
             |
124 | | xp2nd 6843 |
. . . . . . . . 9
     ..^                                    |
125 | 45, 124 | syl 17 |
. . . . . . . 8
           |
126 | | nn0uz 11217 |
. . . . . . . . . . . . . . . . . 18
     |
127 | 12, 126 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . 17
         |
128 | | fzpred 11870 |
. . . . . . . . . . . . . . . . 17
      
                    |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
    
                |
130 | | 0p1e1 10743 |
. . . . . . . . . . . . . . . . . 18
   |
131 | 130 | oveq1i 6318 |
. . . . . . . . . . . . . . . . 17
           
   |
132 | 131 | uneq2i 3576 |
. . . . . . . . . . . . . . . 16
                       |
133 | 129, 132 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
    
              |
134 | 133 | eleq2d 2534 |
. . . . . . . . . . . . . 14
           
          
      |
135 | 134 | notbid 301 |
. . . . . . . . . . . . 13
                             |
136 | | ioran 498 |
. . . . . . . . . . . . . 14
                                   |
137 | | elun 3565 |
. . . . . . . . . . . . . . 15
                                   |
138 | | fvex 5889 |
. . . . . . . . . . . . . . . . 17
     |
139 | 138 | elsnc 3984 |
. . . . . . . . . . . . . . . 16
             |
140 | 139 | orbi1i 529 |
. . . . . . . . . . . . . . 15
                                     |
141 | 137, 140 | bitri 257 |
. . . . . . . . . . . . . 14
                                 |
142 | 136, 141 | xchnxbir 316 |
. . . . . . . . . . . . 13
                                 |
143 | 135, 142 | syl6bb 269 |
. . . . . . . . . . . 12
                               |
144 | 143 | anbi2d 718 |
. . . . . . . . . . 11
                                           
       |
145 | | uncom 3569 |
. . . . . . . . . . . . . . . 16
                     |
146 | 145 | difeq1i 3536 |
. . . . . . . . . . . . . . 15
     
                               |
147 | | difun2 3838 |
. . . . . . . . . . . . . . 15
       
                     |
148 | 146, 147 | eqtri 2493 |
. . . . . . . . . . . . . 14
     
                       |
149 | 1 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . 19
   |
150 | | npcan1 10065 |
. . . . . . . . . . . . . . . . . . 19
       |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
152 | 1 | nnnn0d 10949 |
. . . . . . . . . . . . . . . . . . 19
   |
153 | 152, 126 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . 18
       |
154 | 151, 153 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
           |
155 | 12 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . 19
     |
156 | | uzid 11197 |
. . . . . . . . . . . . . . . . . . 19
   
    
    |
157 | | peano2uz 11235 |
. . . . . . . . . . . . . . . . . . 19
      
 
 
          |
158 | 155, 156,
157 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
        
    |
159 | 151, 158 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
    
    |
160 | | fzsplit2 11850 |
. . . . . . . . . . . . . . . . 17
                
                      |
161 | 154, 159,
160 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
                       |
162 | 151 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
               |
163 | 1 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . 19
   |
164 | | fzsn 11866 |
. . . . . . . . . . . . . . . . . . 19
         |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
166 | 162, 165 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
             |
167 | 166 | uneq2d 3579 |
. . . . . . . . . . . . . . . 16
                             |
168 | 161, 167 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
                 |
169 | 168 | difeq1d 3539 |
. . . . . . . . . . . . . 14
                       
         |
170 | | elfzle2 11829 |
. . . . . . . . . . . . . . . 16
           |
171 | 15, 170 | nsyl 125 |
. . . . . . . . . . . . . . 15
         |
172 | | incom 3616 |
. . . . . . . . . . . . . . . . 17
                     |
173 | 172 | eqeq1i 2476 |
. . . . . . . . . . . . . . . 16
     
                 |
174 | | disjsn 4023 |
. . . . . . . . . . . . . . . 16
     
    
        |
175 | | disj3 3813 |
. . . . . . . . . . . . . . . 16
       
    
            |
176 | 173, 174,
175 | 3bitr3i 283 |
. . . . . . . . . . . . . . 15
      
 
  
         |
177 | 171, 176 | sylib 201 |
. . . . . . . . . . . . . 14
         
     |
178 | 148, 169,
177 | 3eqtr4a 2531 |
. . . . . . . . . . . . 13
                 |
179 | 178 | eleq2d 2534 |
. . . . . . . . . . . 12
                 
         |
180 | | eldif 3400 |
. . . . . . . . . . . 12
             
  
        
       
     |
181 | 138 | elsnc 3984 |
. . . . . . . . . . . 12
             |
182 | 179, 180,
181 | 3bitr3g 295 |
. . . . . . . . . . 11
                             |
183 | 144, 182 | bitr3d 263 |
. . . . . . . . . 10
                       
   
       |
184 | 183 | biimpd 212 |
. . . . . . . . 9
                       
           |
185 | 184 | expdimp 444 |
. . . . . . . 8
 
        
                        |
186 | 125, 185 | sylan2 482 |
. . . . . . 7
 
                 
       |
187 | 123, 186 | mpan2d 688 |
. . . . . 6
 
             |
188 | 1, 2, 3 | poimirlem14 32018 |
. . . . . . . . . 10
        |
189 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
190 | 189 | eqeq1d 2473 |
. . . . . . . . . . 11
     
       |
191 | 190 | rmo4 3219 |
. . . . . . . . . 10
     


              |
192 | 188, 191 | sylib 201 |
. . . . . . . . 9
  
              |
193 | 192 | r19.21bi 2776 |
. . . . . . . 8
 
 
              |
194 | 4 | adantr 472 |
. . . . . . . 8
 
   |
195 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
196 | 195 | eqeq1d 2473 |
. . . . . . . . . . 11
     
       |
197 | 196 | anbi2d 718 |
. . . . . . . . . 10
           
             |
198 | | eqeq2 2482 |
. . . . . . . . . 10
 
   |
199 | 197, 198 | imbi12d 327 |
. . . . . . . . 9
                             |
200 | 199 | rspccv 3133 |
. . . . . . . 8
 
            
               |
201 | 193, 194,
200 | sylc 61 |
. . . . . . 7
 
               |
202 | 8, 201 | mpan2d 688 |
. . . . . 6
 
         |
203 | 187, 202 | syld 44 |
. . . . 5
 
         |
204 | 203 | necon1ad 2660 |
. . . 4
 
         |
205 | 204 | ralrimiva 2809 |
. . 3
          |
206 | 1, 2, 3 | poimirlem13 32017 |
. . 3
        |
207 | | rmoim 3227 |
. . 3
 
       
        |
208 | 205, 206,
207 | sylc 61 |
. 2
    |
209 | | reu5 2994 |
. 2
 
 

   |
210 | 7, 208, 209 | sylanbrc 677 |
1
    |