Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . 4
   |
2 | | fveq2 5865 |
. . . . . . . . . . . 12
           |
3 | 2 | breq2d 4414 |
. . . . . . . . . . 11
 
   
       |
4 | 3 | ifbid 3903 |
. . . . . . . . . 10
                         |
5 | 4 | csbeq1d 3370 |
. . . . . . . . 9
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
6 | | fveq2 5865 |
. . . . . . . . . . . 12
           |
7 | 6 | fveq2d 5869 |
. . . . . . . . . . 11
                   |
8 | 6 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                   |
9 | 8 | imaeq1d 5167 |
. . . . . . . . . . . . 13
                                   |
10 | 9 | xpeq1d 4857 |
. . . . . . . . . . . 12
                                           |
11 | 8 | imaeq1d 5167 |
. . . . . . . . . . . . 13
                                       |
12 | 11 | xpeq1d 4857 |
. . . . . . . . . . . 12
                                               |
13 | 10, 12 | uneq12d 3589 |
. . . . . . . . . . 11
                                                                                           |
14 | 7, 13 | oveq12d 6308 |
. . . . . . . . . 10
                                                                                                                 |
15 | 14 | csbeq2dv 3781 |
. . . . . . . . 9
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
16 | 5, 15 | eqtrd 2485 |
. . . . . . . 8
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
17 | 16 | mpteq2dv 4490 |
. . . . . . 7
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
18 | 17 | eqeq2d 2461 |
. . . . . 6
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
19 | | poimirlem22.s |
. . . . . 6
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
20 | 18, 19 | elrab2 3198 |
. . . . 5

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
21 | 20 | simprbi 466 |
. . . 4
     
               ![]_ ]_](_urbrack.gif)                                                           |
22 | 1, 21 | syl 17 |
. . 3
                     ![]_ ]_](_urbrack.gif)                                                           |
23 | | breq1 4405 |
. . . . . . 7
 
   
       |
24 | | id 22 |
. . . . . . 7
   |
25 | 23, 24 | ifbieq1d 3904 |
. . . . . 6
                         |
26 | | poimirlem5.2 |
. . . . . . 7
       |
27 | 26 | iftrued 3889 |
. . . . . 6
              |
28 | 25, 27 | sylan9eqr 2507 |
. . . . 5
 
              |
29 | 28 | csbeq1d 3370 |
. . . 4
 
              ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
30 | | c0ex 9637 |
. . . . . . 7
 |
31 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
32 | | fz10 11820 |
. . . . . . . . . . . . 13
     |
33 | 31, 32 | syl6eq 2501 |
. . . . . . . . . . . 12
       |
34 | 33 | imaeq2d 5168 |
. . . . . . . . . . 11
                               |
35 | 34 | xpeq1d 4857 |
. . . . . . . . . 10
                                       |
36 | | oveq1 6297 |
. . . . . . . . . . . . . 14
       |
37 | | 0p1e1 10721 |
. . . . . . . . . . . . . 14
   |
38 | 36, 37 | syl6eq 2501 |
. . . . . . . . . . . . 13
     |
39 | 38 | oveq1d 6305 |
. . . . . . . . . . . 12
             |
40 | 39 | imaeq2d 5168 |
. . . . . . . . . . 11
                                     |
41 | 40 | xpeq1d 4857 |
. . . . . . . . . 10
                                             |
42 | 35, 41 | uneq12d 3589 |
. . . . . . . . 9
                                                                                     |
43 | | ima0 5183 |
. . . . . . . . . . . . 13
             |
44 | 43 | xpeq1i 4854 |
. . . . . . . . . . . 12
                
    |
45 | | 0xp 4915 |
. . . . . . . . . . . 12
     |
46 | 44, 45 | eqtri 2473 |
. . . . . . . . . . 11
                 |
47 | 46 | uneq1i 3584 |
. . . . . . . . . 10
                                      
                      |
48 | | uncom 3578 |
. . . . . . . . . 10
                                             |
49 | | un0 3759 |
. . . . . . . . . 10
                                           |
50 | 47, 48, 49 | 3eqtri 2477 |
. . . . . . . . 9
                                                           |
51 | 42, 50 | syl6eq 2501 |
. . . . . . . 8
                                                                   |
52 | 51 | oveq2d 6306 |
. . . . . . 7
                                                                                         |
53 | 30, 52 | csbie 3389 |
. . . . . 6
  ![]_ ]_](_urbrack.gif)                                                                                        |
54 | | elrabi 3193 |
. . . . . . . . . . . . . . 15
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
55 | 54, 19 | eleq2s 2547 |
. . . . . . . . . . . . . 14
     ..^                            |
56 | 1, 55 | syl 17 |
. . . . . . . . . . . . 13
     ..^                            |
57 | | xp1st 6823 |
. . . . . . . . . . . . 13
     ..^                                 ..^                       |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
        ..^                       |
59 | | xp2nd 6824 |
. . . . . . . . . . . 12
        ..^                                             |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
                         |
61 | | fvex 5875 |
. . . . . . . . . . . 12
         |
62 | | f1oeq1 5805 |
. . . . . . . . . . . 12
                                             |
63 | 61, 62 | elab 3185 |
. . . . . . . . . . 11
                      
                      |
64 | 60, 63 | sylib 200 |
. . . . . . . . . 10
                       |
65 | | f1ofo 5821 |
. . . . . . . . . 10
                    
                      |
66 | 64, 65 | syl 17 |
. . . . . . . . 9
                       |
67 | | foima 5798 |
. . . . . . . . 9
                                           |
68 | 66, 67 | syl 17 |
. . . . . . . 8
                       |
69 | 68 | xpeq1d 4857 |
. . . . . . 7
                               |
70 | 69 | oveq2d 6306 |
. . . . . 6
                                                     |
71 | 53, 70 | syl5eq 2497 |
. . . . 5
   ![]_ ]_](_urbrack.gif)                                                                             |
72 | 71 | adantr 467 |
. . . 4
 
   ![]_ ]_](_urbrack.gif)                                                                             |
73 | 29, 72 | eqtrd 2485 |
. . 3
 
              ![]_ ]_](_urbrack.gif)                                                                             |
74 | | poimir.0 |
. . . . 5
   |
75 | | nnm1nn0 10911 |
. . . . 5
 
   |
76 | 74, 75 | syl 17 |
. . . 4
     |
77 | | 0elfz 11889 |
. . . 4
  
   
    |
78 | 76, 77 | syl 17 |
. . 3
         |
79 | | ovex 6318 |
. . . 4
                    |
80 | 79 | a1i 11 |
. . 3
                      |
81 | 22, 73, 78, 80 | fvmptd 5954 |
. 2
                          |
82 | | ovex 6318 |
. . . 4
     |
83 | 82 | a1i 11 |
. . 3
       |
84 | | xp1st 6823 |
. . . . 5
        ..^                               ..^        |
85 | 58, 84 | syl 17 |
. . . 4
           ..^        |
86 | | elmapfn 7494 |
. . . 4
           ..^                    |
87 | 85, 86 | syl 17 |
. . 3
               |
88 | | fnconstg 5771 |
. . . 4
               |
89 | 30, 88 | mp1i 13 |
. . 3
               |
90 | | eqidd 2452 |
. . 3
 
                               |
91 | 30 | fvconst2 6120 |
. . . 4
                   |
92 | 91 | adantl 468 |
. . 3
 
                   |
93 | | elmapi 7493 |
. . . . . . . 8
           ..^                       ..^   |
94 | 85, 93 | syl 17 |
. . . . . . 7
                  ..^   |
95 | 94 | ffvelrnda 6022 |
. . . . . 6
 
                  ..^   |
96 | | elfzonn0 11960 |
. . . . . 6
              ..^               |
97 | 95, 96 | syl 17 |
. . . . 5
 
                   |
98 | 97 | nn0cnd 10927 |
. . . 4
 
                   |
99 | 98 | addid1d 9833 |
. . 3
 
                                 |
100 | 83, 87, 89, 87, 90, 92, 99 | offveq 6552 |
. 2
                              |
101 | 81, 100 | eqtrd 2485 |
1
               |