Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . . . . . 9
   |
2 | | i1ff 22634 |
. . . . . . . . 9
       |
3 | 1, 2 | syl 17 |
. . . . . . . 8
       |
4 | | ffn 5728 |
. . . . . . . 8
       |
5 | 3, 4 | syl 17 |
. . . . . . 7
   |
6 | | i1fadd.2 |
. . . . . . . . 9
   |
7 | | i1ff 22634 |
. . . . . . . . 9
       |
8 | 6, 7 | syl 17 |
. . . . . . . 8
       |
9 | | ffn 5728 |
. . . . . . . 8
       |
10 | 8, 9 | syl 17 |
. . . . . . 7
   |
11 | | reex 9630 |
. . . . . . . 8
 |
12 | 11 | a1i 11 |
. . . . . . 7
   |
13 | | inidm 3641 |
. . . . . . 7
   |
14 | 5, 10, 12, 12, 13 | offn 6542 |
. . . . . 6
      |
15 | 14 | adantr 467 |
. . . . 5
 

     |
16 | | fniniseg 6003 |
. . . . 5
        
         
        |
17 | 15, 16 | syl 17 |
. . . 4
 

          
            |
18 | 10 | ad2antrr 732 |
. . . . . . . 8
       
        |
19 | | simprl 764 |
. . . . . . . 8
       
        |
20 | | fnfvelrn 6019 |
. . . . . . . 8
 
       |
21 | 18, 19, 20 | syl2anc 667 |
. . . . . . 7
       
            |
22 | | simprr 766 |
. . . . . . . . . . . 12
       
               |
23 | | eqidd 2452 |
. . . . . . . . . . . . . 14
 

          |
24 | | eqidd 2452 |
. . . . . . . . . . . . . 14
 

          |
25 | 5, 10, 12, 12, 13, 23, 24 | ofval 6540 |
. . . . . . . . . . . . 13
 

                   |
26 | 25 | ad2ant2r 753 |
. . . . . . . . . . . 12
       
                         |
27 | 22, 26 | eqtr3d 2487 |
. . . . . . . . . . 11
       
                  |
28 | 27 | oveq1d 6305 |
. . . . . . . . . 10
       
      
                       |
29 | | ax-resscn 9596 |
. . . . . . . . . . . . . 14
 |
30 | | fss 5737 |
. . . . . . . . . . . . . 14
             |
31 | 3, 29, 30 | sylancl 668 |
. . . . . . . . . . . . 13
       |
32 | 31 | ad2antrr 732 |
. . . . . . . . . . . 12
       
            |
33 | 32, 19 | ffvelrnd 6023 |
. . . . . . . . . . 11
       
            |
34 | | fss 5737 |
. . . . . . . . . . . . . 14
             |
35 | 8, 29, 34 | sylancl 668 |
. . . . . . . . . . . . 13
       |
36 | 35 | ad2antrr 732 |
. . . . . . . . . . . 12
       
            |
37 | 36, 19 | ffvelrnd 6023 |
. . . . . . . . . . 11
       
            |
38 | 33, 37 | pncand 9987 |
. . . . . . . . . 10
       
                            |
39 | 28, 38 | eqtr2d 2486 |
. . . . . . . . 9
       
                  |
40 | 5 | ad2antrr 732 |
. . . . . . . . . 10
       
        |
41 | | fniniseg 6003 |
. . . . . . . . . 10
              
               |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
       
                   
               |
43 | 19, 39, 42 | mpbir2and 933 |
. . . . . . . 8
       
                     |
44 | | eqidd 2452 |
. . . . . . . . 9
       
                |
45 | | fniniseg 6003 |
. . . . . . . . . 10
            
             |
46 | 18, 45 | syl 17 |
. . . . . . . . 9
       
                 
             |
47 | 19, 44, 46 | mpbir2and 933 |
. . . . . . . 8
       
                   |
48 | 43, 47 | elind 3618 |
. . . . . . 7
       
                                  |
49 | | oveq2 6298 |
. . . . . . . . . . . 12
     
         |
50 | 49 | sneqd 3980 |
. . . . . . . . . . 11
                   |
51 | 50 | imaeq2d 5168 |
. . . . . . . . . 10
                             |
52 | | sneq 3978 |
. . . . . . . . . . 11
               |
53 | 52 | imaeq2d 5168 |
. . . . . . . . . 10
                         |
54 | 51, 53 | ineq12d 3635 |
. . . . . . . . 9
                                                   |
55 | 54 | eleq2d 2514 |
. . . . . . . 8
                       
                             |
56 | 55 | rspcev 3150 |
. . . . . . 7
     
                                                |
57 | 21, 48, 56 | syl2anc 667 |
. . . . . 6
       
                           |
58 | 57 | ex 436 |
. . . . 5
 

    
    
                      |
59 | | elin 3617 |
. . . . . . 7
                  
                    |
60 | 5 | adantr 467 |
. . . . . . . . . 10
 

  |
61 | | fniniseg 6003 |
. . . . . . . . . 10
          
           |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
 

                     |
63 | 10 | adantr 467 |
. . . . . . . . . 10
 

  |
64 | | fniniseg 6003 |
. . . . . . . . . 10
        
         |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
 

                 |
66 | 62, 65 | anbi12d 717 |
. . . . . . . 8
 

                                      |
67 | | anandi 837 |
. . . . . . . . 9
              
                  |
68 | | simprl 764 |
. . . . . . . . . . 11
                     |
69 | 25 | ad2ant2r 753 |
. . . . . . . . . . . 12
                     
                |
70 | | simprrl 774 |
. . . . . . . . . . . . 13
                           |
71 | | simprrr 775 |
. . . . . . . . . . . . 13
                         |
72 | 70, 71 | oveq12d 6308 |
. . . . . . . . . . . 12
                                   |
73 | | simplr 762 |
. . . . . . . . . . . . 13
                  
  |
74 | 35 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                         |
75 | 74, 68 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
                         |
76 | 71, 75 | eqeltrrd 2530 |
. . . . . . . . . . . . 13
                     |
77 | 73, 76 | npcand 9990 |
. . . . . . . . . . . 12
                         |
78 | 69, 72, 77 | 3eqtrd 2489 |
. . . . . . . . . . 11
                     
      |
79 | 68, 78 | jca 535 |
. . . . . . . . . 10
                      
       |
80 | 79 | ex 436 |
. . . . . . . . 9
 

                  
        |
81 | 67, 80 | syl5bir 222 |
. . . . . . . 8
 

                    
        |
82 | 66, 81 | sylbid 219 |
. . . . . . 7
 

                  
            |
83 | 59, 82 | syl5bi 221 |
. . . . . 6
 

                      
        |
84 | 83 | rexlimdvw 2882 |
. . . . 5
 

 
                     
        |
85 | 58, 84 | impbid 194 |
. . . 4
 

    
                           |
86 | 17, 85 | bitrd 257 |
. . 3
 

          
                      |
87 | | eliun 4283 |
. . 3
                    
                     |
88 | 86, 87 | syl6bbr 267 |
. 2
 

          
                       |
89 | 88 | eqrdv 2449 |
1
 

                                |