Step | Hyp | Ref
| Expression |
1 | | ovex 6318 |
. . 3
     |
2 | 1 | a1i 11 |
. 2
       |
3 | | poimirlem22.1 |
. . . 4
               
       |
4 | | poimir.0 |
. . . . . 6
   |
5 | | nnm1nn0 10911 |
. . . . . 6
 
   |
6 | 4, 5 | syl 17 |
. . . . 5
     |
7 | | nn0fz0 11890 |
. . . . 5
  
          |
8 | 6, 7 | sylib 200 |
. . . 4
           |
9 | 3, 8 | ffvelrnd 6023 |
. . 3
    
              |
10 | | elmapfn 7494 |
. . 3
                             |
11 | 9, 10 | syl 17 |
. 2
    
        |
12 | | 1ex 9638 |
. . 3
 |
13 | | fnconstg 5771 |
. . 3
               |
14 | 12, 13 | mp1i 13 |
. 2
               |
15 | | poimirlem12.2 |
. . . . . 6
   |
16 | | elrabi 3193 |
. . . . . . 7
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
17 | | poimirlem22.s |
. . . . . . 7
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
18 | 16, 17 | eleq2s 2547 |
. . . . . 6
     ..^                            |
19 | 15, 18 | syl 17 |
. . . . 5
     ..^                            |
20 | | xp1st 6823 |
. . . . 5
     ..^                                 ..^                       |
21 | 19, 20 | syl 17 |
. . . 4
        ..^                       |
22 | | xp1st 6823 |
. . . 4
        ..^                               ..^        |
23 | 21, 22 | syl 17 |
. . 3
           ..^        |
24 | | elmapfn 7494 |
. . 3
           ..^                    |
25 | 23, 24 | syl 17 |
. 2
               |
26 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
27 | 26 | breq2d 4414 |
. . . . . . . . . . . . . 14
 
   
       |
28 | 27 | ifbid 3903 |
. . . . . . . . . . . . 13
                         |
29 | 28 | csbeq1d 3370 |
. . . . . . . . . . . 12
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
30 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
31 | 30 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                   |
32 | 30 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
                   |
33 | 32 | imaeq1d 5167 |
. . . . . . . . . . . . . . . 16
                                   |
34 | 33 | xpeq1d 4857 |
. . . . . . . . . . . . . . 15
                                           |
35 | 32 | imaeq1d 5167 |
. . . . . . . . . . . . . . . 16
                                       |
36 | 35 | xpeq1d 4857 |
. . . . . . . . . . . . . . 15
                                               |
37 | 34, 36 | uneq12d 3589 |
. . . . . . . . . . . . . 14
                                                                                           |
38 | 31, 37 | oveq12d 6308 |
. . . . . . . . . . . . 13
                                                                                                                 |
39 | 38 | csbeq2dv 3781 |
. . . . . . . . . . . 12
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
40 | 29, 39 | eqtrd 2485 |
. . . . . . . . . . 11
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
41 | 40 | mpteq2dv 4490 |
. . . . . . . . . 10
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
42 | 41 | eqeq2d 2461 |
. . . . . . . . 9
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
43 | 42, 17 | elrab2 3198 |
. . . . . . . 8

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
44 | 43 | simprbi 466 |
. . . . . . 7
     
               ![]_ ]_](_urbrack.gif)                                                           |
45 | 15, 44 | syl 17 |
. . . . . 6
                     ![]_ ]_](_urbrack.gif)                                                           |
46 | | poimirlem11.3 |
. . . . . . . . . . . 12
       |
47 | | breq12 4407 |
. . . . . . . . . . . 12
             
     |
48 | 46, 47 | sylan2 477 |
. . . . . . . . . . 11
    
          |
49 | 48 | ancoms 455 |
. . . . . . . . . 10
 

  
   
     |
50 | | oveq1 6297 |
. . . . . . . . . . 11
           |
51 | 4 | nncnd 10625 |
. . . . . . . . . . . 12
   |
52 | | npcan1 10044 |
. . . . . . . . . . . 12
       |
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
       |
54 | 50, 53 | sylan9eqr 2507 |
. . . . . . . . . 10
 

      |
55 | 49, 54 | ifbieq2d 3906 |
. . . . . . . . 9
 

                      |
56 | 6 | nn0ge0d 10928 |
. . . . . . . . . . . 12

    |
57 | | 0red 9644 |
. . . . . . . . . . . . 13
   |
58 | 6 | nn0red 10926 |
. . . . . . . . . . . . 13
     |
59 | 57, 58 | lenltd 9781 |
. . . . . . . . . . . 12
  
      |
60 | 56, 59 | mpbid 214 |
. . . . . . . . . . 11
     |
61 | 60 | iffalsed 3892 |
. . . . . . . . . 10
          |
62 | 61 | adantr 467 |
. . . . . . . . 9
 

           |
63 | 55, 62 | eqtrd 2485 |
. . . . . . . 8
 

               |
64 | 63 | csbeq1d 3370 |
. . . . . . 7
 

               ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
65 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
           |
66 | 65 | imaeq2d 5168 |
. . . . . . . . . . . . . 14
                                   |
67 | | xp2nd 6824 |
. . . . . . . . . . . . . . . . 17
        ..^                                             |
68 | 21, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
                         |
69 | | fvex 5875 |
. . . . . . . . . . . . . . . . 17
         |
70 | | f1oeq1 5805 |
. . . . . . . . . . . . . . . . 17
                                             |
71 | 69, 70 | elab 3185 |
. . . . . . . . . . . . . . . 16
                      
                      |
72 | 68, 71 | sylib 200 |
. . . . . . . . . . . . . . 15
                       |
73 | | f1ofo 5821 |
. . . . . . . . . . . . . . 15
                    
                      |
74 | | foima 5798 |
. . . . . . . . . . . . . . 15
                                           |
75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . . . . . 14
                       |
76 | 66, 75 | sylan9eqr 2507 |
. . . . . . . . . . . . 13
 
                       |
77 | 76 | xpeq1d 4857 |
. . . . . . . . . . . 12
 
                               |
78 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
       |
79 | 78 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
               |
80 | 4 | nnred 10624 |
. . . . . . . . . . . . . . . . . 18
   |
81 | 80 | ltp1d 10537 |
. . . . . . . . . . . . . . . . 17
     |
82 | 4 | nnzd 11039 |
. . . . . . . . . . . . . . . . . . 19
   |
83 | 82 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . 18
     |
84 | | fzn 11815 |
. . . . . . . . . . . . . . . . . 18
   
  
          |
85 | 83, 82, 84 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
  
          |
86 | 81, 85 | mpbid 214 |
. . . . . . . . . . . . . . . 16
         |
87 | 79, 86 | sylan9eqr 2507 |
. . . . . . . . . . . . . . 15
 
         |
88 | 87 | imaeq2d 5168 |
. . . . . . . . . . . . . 14
 
                                 |
89 | 88 | xpeq1d 4857 |
. . . . . . . . . . . . 13
 
                                         |
90 | | ima0 5183 |
. . . . . . . . . . . . . . 15
             |
91 | 90 | xpeq1i 4854 |
. . . . . . . . . . . . . 14
                
    |
92 | | 0xp 4915 |
. . . . . . . . . . . . . 14
     |
93 | 91, 92 | eqtri 2473 |
. . . . . . . . . . . . 13
                 |
94 | 89, 93 | syl6eq 2501 |
. . . . . . . . . . . 12
 
                         |
95 | 77, 94 | uneq12d 3589 |
. . . . . . . . . . 11
 
                                                         |
96 | | un0 3759 |
. . . . . . . . . . 11
                   |
97 | 95, 96 | syl6eq 2501 |
. . . . . . . . . 10
 
                                                       |
98 | 97 | oveq2d 6306 |
. . . . . . . . 9
 
                                                                             |
99 | 4, 98 | csbied 3390 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)                                                                             |
100 | 99 | adantr 467 |
. . . . . . 7
 

    ![]_ ]_](_urbrack.gif)                                                                             |
101 | 64, 100 | eqtrd 2485 |
. . . . . 6
 

               ![]_ ]_](_urbrack.gif)                                                                             |
102 | | ovex 6318 |
. . . . . . 7
                    |
103 | 102 | a1i 11 |
. . . . . 6
                      |
104 | 45, 101, 8, 103 | fvmptd 5954 |
. . . . 5
    
                       |
105 | 104 | fveq1d 5867 |
. . . 4
     
                              |
106 | 105 | adantr 467 |
. . 3
 
         
                              |
107 | | inidm 3641 |
. . . 4
               |
108 | | eqidd 2452 |
. . . 4
 
                               |
109 | 12 | fvconst2 6120 |
. . . . 5
                   |
110 | 109 | adantl 468 |
. . . 4
 
                   |
111 | 25, 14, 2, 2, 107, 108, 110 | ofval 6540 |
. . 3
 
                                            |
112 | 106, 111 | eqtrd 2485 |
. 2
 
         
                     |
113 | | elmapi 7493 |
. . . . . . 7
           ..^                       ..^   |
114 | 23, 113 | syl 17 |
. . . . . 6
                  ..^   |
115 | 114 | ffvelrnda 6022 |
. . . . 5
 
                  ..^   |
116 | | elfzonn0 11960 |
. . . . 5
              ..^               |
117 | 115, 116 | syl 17 |
. . . 4
 
                   |
118 | 117 | nn0cnd 10927 |
. . 3
 
                   |
119 | | pncan1 10043 |
. . 3
            
                              |
120 | 118, 119 | syl 17 |
. 2
 
                                   |
121 | 2, 11, 14, 25, 112, 110, 120 | offveq 6552 |
1
     
                      |