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

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
21 | 20 | simprbi 466 |
. . 3
     
               ![]_ ]_](_urbrack.gif)                                                           |
22 | 1, 21 | syl 17 |
. 2
                     ![]_ ]_](_urbrack.gif)                                                           |
23 | | elrabi 3193 |
. . . . . . . . . . . 12
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
24 | 23, 19 | eleq2s 2547 |
. . . . . . . . . . 11
     ..^                            |
25 | 1, 24 | syl 17 |
. . . . . . . . . 10
     ..^                            |
26 | | xp1st 6823 |
. . . . . . . . . 10
     ..^                                 ..^                       |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
        ..^                       |
28 | | xp1st 6823 |
. . . . . . . . 9
        ..^                               ..^        |
29 | 27, 28 | syl 17 |
. . . . . . . 8
           ..^        |
30 | | elmapfn 7494 |
. . . . . . . 8
           ..^                    |
31 | 29, 30 | syl 17 |
. . . . . . 7
               |
32 | 31 | adantr 467 |
. . . . . 6
 
   
                 |
33 | | 1ex 9638 |
. . . . . . . . . 10
 |
34 | | fnconstg 5771 |
. . . . . . . . . 10
                                       |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . 9
                                     |
36 | | c0ex 9637 |
. . . . . . . . . 10
 |
37 | | fnconstg 5771 |
. . . . . . . . . 10
                                           |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
                                         |
39 | 35, 38 | pm3.2i 457 |
. . . . . . . 8
                                                                               |
40 | | xp2nd 6824 |
. . . . . . . . . . . . 13
        ..^                                             |
41 | 27, 40 | syl 17 |
. . . . . . . . . . . 12
                         |
42 | | fvex 5875 |
. . . . . . . . . . . . 13
         |
43 | | f1oeq1 5805 |
. . . . . . . . . . . . 13
                                             |
44 | 42, 43 | elab 3185 |
. . . . . . . . . . . 12
                      
                      |
45 | 41, 44 | sylib 200 |
. . . . . . . . . . 11
                       |
46 | | dff1o3 5820 |
. . . . . . . . . . . 12
                                         
            |
47 | 46 | simprbi 466 |
. . . . . . . . . . 11
                    
           |
48 | 45, 47 | syl 17 |
. . . . . . . . . 10
            |
49 | | imain 5659 |
. . . . . . . . . 10
                         
                                              |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
                                                               |
51 | | elfznn0 11887 |
. . . . . . . . . . . . . 14
         |
52 | 51 | nn0red 10926 |
. . . . . . . . . . . . 13
         |
53 | 52 | ltp1d 10537 |
. . . . . . . . . . . 12
           |
54 | | fzdisj 11826 |
. . . . . . . . . . . 12
       
         |
55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
           
         |
56 | 55 | imaeq2d 5168 |
. . . . . . . . . 10
                                             |
57 | | ima0 5183 |
. . . . . . . . . 10
             |
58 | 56, 57 | syl6eq 2501 |
. . . . . . . . 9
                                 |
59 | 50, 58 | sylan9req 2506 |
. . . . . . . 8
 
   
                                         |
60 | | fnun 5682 |
. . . . . . . 8
                                                                                                                                                                                                       |
61 | 39, 59, 60 | sylancr 669 |
. . . . . . 7
 
   
                                                                                     |
62 | | imaundi 5248 |
. . . . . . . . 9
                                                             |
63 | | nn0p1nn 10909 |
. . . . . . . . . . . . . . 15

    |
64 | 51, 63 | syl 17 |
. . . . . . . . . . . . . 14
           |
65 | | nnuz 11194 |
. . . . . . . . . . . . . 14
     |
66 | 64, 65 | syl6eleq 2539 |
. . . . . . . . . . . . 13
               |
67 | 66 | adantl 468 |
. . . . . . . . . . . 12
 
   
           |
68 | | poimir.0 |
. . . . . . . . . . . . . . . 16
   |
69 | 68 | nncnd 10625 |
. . . . . . . . . . . . . . 15
   |
70 | | npcan1 10044 |
. . . . . . . . . . . . . . 15
       |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . 14
       |
72 | 71 | adantr 467 |
. . . . . . . . . . . . 13
 
   
         |
73 | | elfzuz3 11797 |
. . . . . . . . . . . . . . 15
       
       |
74 | | peano2uz 11212 |
. . . . . . . . . . . . . . 15
      
 
        |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . 14
                 |
76 | 75 | adantl 468 |
. . . . . . . . . . . . 13
 
   
             |
77 | 72, 76 | eqeltrrd 2530 |
. . . . . . . . . . . 12
 
   
         |
78 | | fzsplit2 11824 |
. . . . . . . . . . . 12
            
                  |
79 | 67, 77, 78 | syl2anc 667 |
. . . . . . . . . . 11
 
   
                     |
80 | 79 | imaeq2d 5168 |
. . . . . . . . . 10
 
   
                                             |
81 | | f1ofo 5821 |
. . . . . . . . . . . 12
                    
                      |
82 | | foima 5798 |
. . . . . . . . . . . 12
                                           |
83 | 45, 81, 82 | 3syl 18 |
. . . . . . . . . . 11
                       |
84 | 83 | adantr 467 |
. . . . . . . . . 10
 
   
                         |
85 | 80, 84 | eqtr3d 2487 |
. . . . . . . . 9
 
   
                                 |
86 | 62, 85 | syl5eqr 2499 |
. . . . . . . 8
 
   
                                             |
87 | 86 | fneq2d 5667 |
. . . . . . 7
 
   
                                                                                   
                                                   |
88 | 61, 87 | mpbid 214 |
. . . . . 6
 
   
                                                     |
89 | | ovex 6318 |
. . . . . . 7
     |
90 | 89 | a1i 11 |
. . . . . 6
 
   
         |
91 | | inidm 3641 |
. . . . . 6
               |
92 | | eqidd 2452 |
. . . . . 6
      
                                  |
93 | | eqidd 2452 |
. . . . . 6
      
                                                                                                          |
94 | 32, 88, 90, 90, 91, 92, 93 | offval 6538 |
. . . . 5
 
   
                                                                                                                                |
95 | | elmapi 7493 |
. . . . . . . . . . . . 13
           ..^                       ..^   |
96 | 29, 95 | syl 17 |
. . . . . . . . . . . 12
                  ..^   |
97 | 96 | ffvelrnda 6022 |
. . . . . . . . . . 11
 
                  ..^   |
98 | | elfzonn0 11960 |
. . . . . . . . . . 11
              ..^               |
99 | 97, 98 | syl 17 |
. . . . . . . . . 10
 
                   |
100 | 99 | nn0cnd 10927 |
. . . . . . . . 9
 
                   |
101 | 100 | adantlr 721 |
. . . . . . . 8
      
                      |
102 | | ax-1cn 9597 |
. . . . . . . . . 10
 |
103 | | 0cn 9635 |
. . . . . . . . . 10
 |
104 | 102, 103 | keepel 3948 |
. . . . . . . . 9
                  |
105 | 104 | a1i 11 |
. . . . . . . 8
      
         
                 |
106 | | snssi 4116 |
. . . . . . . . . . 11
  
  |
107 | 102, 106 | ax-mp 5 |
. . . . . . . . . 10
 
 |
108 | | snssi 4116 |
. . . . . . . . . . 11
  
  |
109 | 103, 108 | ax-mp 5 |
. . . . . . . . . 10
 
 |
110 | 107, 109 | unssi 3609 |
. . . . . . . . 9
       |
111 | 33 | fconst 5769 |
. . . . . . . . . . . . 13
                                                                             |
112 | 36 | fconst 5769 |
. . . . . . . . . . . . 13
                                                                                 |
113 | 111, 112 | pm3.2i 457 |
. . . . . . . . . . . 12
                                                                                                                                                               |
114 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
 
               |
115 | 68 | nnzd 11039 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
116 | | 1z 10967 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
117 | | peano2z 10978 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
119 | 115, 118 | jctil 540 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
120 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
121 | 120, 116 | jctir 541 |
. . . . . . . . . . . . . . . . . . . . . 22
       
   |
122 | | fzsubel 11834 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
123 | 119, 121,
122 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
 
             
         
     |
124 | 114, 123 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
 
                     |
125 | 102, 102 | pncan3oi 9891 |
. . . . . . . . . . . . . . . . . . . . 21
     |
126 | 125 | oveq1i 6300 |
. . . . . . . . . . . . . . . . . . . 20
             
   |
127 | 124, 126 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
128 | 127 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . 18
                   |
129 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
      
    |
130 | | peano2zm 10980 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
131 | 115, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
132 | 131, 116 | jctil 540 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
133 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
134 | 133, 116 | jctir 541 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
   |
135 | | fzaddel 11833 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               |
136 | 132, 134,
135 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
         
               |
137 | 129, 136 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
                 |
138 | 71 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
139 | 138 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
                     |
140 | 137, 139 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . 20
 
   
             |
141 | 120 | zcnd 11041 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
142 | 133 | zcnd 11041 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
143 | | subadd2 9879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   
     |
144 | 102, 143 | mp3an2 1352 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
         |
145 | | eqcom 2458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    |
146 | | eqcom 2458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    |
147 | 144, 145,
146 | 3bitr4g 292 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         |
148 | 141, 142,
147 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
       
         
     |
149 | 148 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . . . 21
                 
     |
150 | 149 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
   
             
     |
151 | | reu6i 3229 |
. . . . . . . . . . . . . . . . . . . 20
                    
    
           |
152 | 140, 150,
151 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
 
   
   
           |
153 | 152 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . 18
                     |
154 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
                     |
155 | 154 | f1ompt 6044 |
. . . . . . . . . . . . . . . . . 18
                          
 
               
                    |
156 | 128, 153,
155 | sylanbrc 670 |
. . . . . . . . . . . . . . . . 17
                             |
157 | | f1osng 5853 |
. . . . . . . . . . . . . . . . . 18
 
                |
158 | 33, 68, 157 | sylancr 669 |
. . . . . . . . . . . . . . . . 17
                |
159 | 68 | nnred 10624 |
. . . . . . . . . . . . . . . . . . . . 21
   |
160 | 159 | ltm1d 10539 |
. . . . . . . . . . . . . . . . . . . 20
     |
161 | 131 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . 21
     |
162 | 161, 159 | ltnled 9782 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
163 | 160, 162 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
 
   |
164 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . 19
           |
165 | 163, 164 | nsyl 125 |
. . . . . . . . . . . . . . . . . 18
         |
166 | | disjsn 4032 |
. . . . . . . . . . . . . . . . . 18
     
    
        |
167 | 165, 166 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
             |
168 | | 1re 9642 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
169 | 168 | ltp1i 10510 |
. . . . . . . . . . . . . . . . . . . . 21
   |
170 | 118 | zrei 10943 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
171 | 168, 170 | ltnlei 9755 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
172 | 169, 171 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . 20
   |
173 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . 20
           |
174 | 172, 173 | mto 180 |
. . . . . . . . . . . . . . . . . . 19
       |
175 | | disjsn 4032 |
. . . . . . . . . . . . . . . . . . 19
       
  
        |
176 | 174, 175 | mpbir 213 |
. . . . . . . . . . . . . . . . . 18
           |
177 | | f1oun 5833 |
. . . . . . . . . . . . . . . . . 18
                          
    
                     
    
                                                  |
178 | 176, 177 | mpanr1 689 |
. . . . . . . . . . . . . . . . 17
                          
    
                                                                 |
179 | 156, 158,
167, 178 | syl21anc 1267 |
. . . . . . . . . . . . . . . 16
                                            |
180 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
         |
181 | 174, 180 | mtbiri 305 |
. . . . . . . . . . . . . . . . . . . . . 22

        |
182 | 181 | necon2ai 2653 |
. . . . . . . . . . . . . . . . . . . . 21
         |
183 | | ifnefalse 3893 |
. . . . . . . . . . . . . . . . . . . . 21
  
         |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
        
         |
185 | 184 | mpteq2ia 4485 |
. . . . . . . . . . . . . . . . . . 19
                          |
186 | 185 | uneq1i 3584 |
. . . . . . . . . . . . . . . . . 18
                                   
    |
187 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   |
188 | | ssv 3452 |
. . . . . . . . . . . . . . . . . . . 20
 |
189 | 188, 68 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . 19
   |
190 | 68, 65 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . . . 21
       |
191 | | fzpred 11844 |
. . . . . . . . . . . . . . . . . . . . 21
    
                |
192 | 190, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                 |
193 | | uncom 3578 |
. . . . . . . . . . . . . . . . . . . 20
                     |
194 | 192, 193 | syl6req 2502 |
. . . . . . . . . . . . . . . . . . 19
                 |
195 | | iftrue 3887 |
. . . . . . . . . . . . . . . . . . . 20
  
       |
196 | 195 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
  
       |
197 | 187, 189,
194, 196 | fmptapd 6088 |
. . . . . . . . . . . . . . . . . 18
                                      |
198 | 186, 197 | syl5eqr 2499 |
. . . . . . . . . . . . . . . . 17
                                 |
199 | 71, 190 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . 19
           |
200 | | uzid 11173 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
    |
201 | | peano2uz 11212 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
 
          |
202 | 131, 200,
201 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
        
    |
203 | 71, 202 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . . . . 19
    
    |
204 | | fzsplit2 11824 |
. . . . . . . . . . . . . . . . . . 19
                
                      |
205 | 199, 203,
204 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                       |
206 | 71 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . 20
               |
207 | | fzsn 11840 |
. . . . . . . . . . . . . . . . . . . . 21
         |
208 | 115, 207 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         |
209 | 206, 208 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19
             |
210 | 209 | uneq2d 3588 |
. . . . . . . . . . . . . . . . . 18
                             |
211 | 205, 210 | eqtr2d 2486 |
. . . . . . . . . . . . . . . . 17
                 |
212 | 198, 194,
211 | f1oeq123d 5811 |
. . . . . . . . . . . . . . . 16
                                                                       |
213 | 179, 212 | mpbid 214 |
. . . . . . . . . . . . . . 15
                            |
214 | | f1oco 5836 |
. . . . . . . . . . . . . . 15
                     
                                                               |
215 | 45, 213, 214 | syl2anc 667 |
. . . . . . . . . . . . . 14
                                      |
216 | | dff1o3 5820 |
. . . . . . . . . . . . . . 15
                                   
                                                               |
217 | 216 | simprbi 466 |
. . . . . . . . . . . . . 14
                                                              |
218 | | imain 5659 |
. . . . . . . . . . . . . 14
                                                                                                                                            |
219 | 215, 217,
218 | 3syl 18 |
. . . . . . . . . . . . 13
                                                                                                                    |
220 | 64 | nnred 10624 |
. . . . . . . . . . . . . . . . 17
           |
221 | 220 | ltp1d 10537 |
. . . . . . . . . . . . . . . 16
               |
222 | | fzdisj 11826 |
. . . . . . . . . . . . . . . 16
                         |
223 | 221, 222 | syl 17 |
. . . . . . . . . . . . . . 15
                         |
224 | 223 | imaeq2d 5168 |
. . . . . . . . . . . . . 14
                                                                               |
225 | | ima0 5183 |
. . . . . . . . . . . . . 14
                            |
226 | 224, 225 | syl6eq 2501 |
. . . . . . . . . . . . 13
                                                    |
227 | 219, 226 | sylan9req 2506 |
. . . . . . . . . . . 12
 
   
                                                                           |
228 | | fun 5746 |
. . . . . . . . . . . 12
                                                                                                                                                                                                                                      
                                                                                                                                                                |
229 | 113, 227,
228 | sylancr 669 |
. . . . . . . . . . 11
 
   
                                                                                                                                                                   |
230 | | imaundi 5248 |
. . . . . . . . . . . . 13
                                                                                                                  |
231 | 64 | peano2nnd 10626 |
. . . . . . . . . . . . . . . . . 18
             |
232 | 231, 65 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . 17
                 |
233 | 232 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
   
             |
234 | | eluzp1p1 11184 |
. . . . . . . . . . . . . . . . . . 19
      
 
          |
235 | 73, 234 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                   |
236 | 235 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
   
               |
237 | 72, 236 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . 16
 
   
           |
238 | | fzsplit2 11824 |
. . . . . . . . . . . . . . . 16
                
                      |
239 | 233, 237,
238 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
   
                         |
240 | 239 | imaeq2d 5168 |
. . . . . . . . . . . . . 14
 
   
                                                                               |
241 | | f1ofo 5821 |
. . . . . . . . . . . . . . . 16
                                                                         |
242 | | foima 5798 |
. . . . . . . . . . . . . . . 16
                                                                         |
243 | 215, 241,
242 | 3syl 18 |
. . . . . . . . . . . . . . 15
                                      |
244 | 243 | adantr 467 |
. . . . . . . . . . . . . 14
 
   
                                        |
245 | 240, 244 | eqtr3d 2487 |
. . . . . . . . . . . . 13
 
   
                                                    |
246 | 230, 245 | syl5eqr 2499 |
. . . . . . . . . . . 12
 
   
                                                                               |
247 | 246 | feq2d 5715 |
. . . . . . . . . . 11
 
   
                                                                                                                                                                 
                                                                                               |
248 | 229, 247 | mpbid 214 |
. . . . . . . . . 10
 
   
                                                                                                 |
249 | 248 | ffvelrnda 6022 |
. . . . . . . . 9
      
                                                                                                  |
250 | 110, 249 | sseldi 3430 |
. . . . . . . 8
      
                                                                                            |
251 | 101, 105,
250 | subadd23d 10008 |
. . . . . . 7
      
                                                                                                                                                                                                                                                |
252 | | oveq2 6298 |
. . . . . . . . . 10
                                                                                                                                                                                                             |
253 | 252 | eqeq1d 2453 |
. . . . . . . . 9
                                                                                                                                                      
                                                                                                                                                        |
254 | | oveq2 6298 |
. . . . . . . . . 10
                                                                                                                                                                                                             |
255 | 254 | eqeq1d 2453 |
. . . . . . . . 9
                                                                                                                                                      
                                                                                                                                                        |
256 | | 1m1e0 10678 |
. . . . . . . . . . . . 13
   |
257 | | f1ofn 5815 |
. . . . . . . . . . . . . . . . . . . 20
                    
              |
258 | 45, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
               |
259 | 258 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   
                 |
260 | | imassrn 5179 |
. . . . . . . . . . . . . . . . . . . 20
                      
              |
261 | | f1of 5814 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                     |
262 | 213, 261 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                            |
263 | | frn 5735 |
. . . . . . . . . . . . . . . . . . . . 21
                         
            
      |
264 | 262, 263 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                    |
265 | 260, 264 | syl5ss 3443 |
. . . . . . . . . . . . . . . . . . 19
        |