Step | Hyp | Ref
| Expression |
1 | | fveq2 5865 |
. . . . . . . 8
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
2 | 1 | sseq1d 3459 |
. . . . . . 7
   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      |
3 | 2 | elrab 3196 |
. . . . . 6
                     
 ![[,] [,]](_icc.gif)   
                    
 ![[,] [,]](_icc.gif)      |
4 | | simprr 766 |
. . . . . . 7
                            ![[,] [,]](_icc.gif)  
 
 ![[,] [,]](_icc.gif)     |
5 | | fvex 5875 |
. . . . . . . 8
 ![[,] [,]](_icc.gif)    |
6 | 5 | elpw 3957 |
. . . . . . 7
  ![[,] [,]](_icc.gif)   
 ![[,] [,]](_icc.gif)     |
7 | 4, 6 | sylibr 216 |
. . . . . 6
                            ![[,] [,]](_icc.gif)  
 
 ![[,] [,]](_icc.gif)      |
8 | 3, 7 | sylan2b 478 |
. . . . 5
       

                   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
9 | 8 | ralrimiva 2802 |
. . . 4
    
  

                   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
10 | | iccf 11733 |
. . . . . 6
![[,] [,]](_icc.gif)  
     |
11 | | ffun 5731 |
. . . . . 6
 ![[,] [,]](_icc.gif)      
![[,] [,]](_icc.gif)  |
12 | 10, 11 | ax-mp 5 |
. . . . 5
![[,] [,]](_icc.gif) |
13 | | ssrab2 3514 |
. . . . . . 7
  
                   ![[,] [,]](_icc.gif)  
                      |
14 | | oveq1 6297 |
. . . . . . . . . . . 12
               |
15 | | oveq1 6297 |
. . . . . . . . . . . . 13
       |
16 | 15 | oveq1d 6305 |
. . . . . . . . . . . 12
                   |
17 | 14, 16 | opeq12d 4174 |
. . . . . . . . . . 11
                                     |
18 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
19 | 18 | oveq2d 6306 |
. . . . . . . . . . . 12
               |
20 | 18 | oveq2d 6306 |
. . . . . . . . . . . 12
                   |
21 | 19, 20 | opeq12d 4174 |
. . . . . . . . . . 11
                                     |
22 | 17, 21 | cbvmpt2v 6371 |
. . . . . . . . . 10
 
                                       |
23 | 22 | dyadf 22549 |
. . . . . . . . 9
 
                        
   |
24 | | frn 5735 |
. . . . . . . . 9
                           
  

                 
     |
25 | 23, 24 | ax-mp 5 |
. . . . . . . 8
                   
    |
26 | | inss2 3653 |
. . . . . . . . 9
      |
27 | | rexpssxrxp 9685 |
. . . . . . . . 9
     |
28 | 26, 27 | sstri 3441 |
. . . . . . . 8
      |
29 | 25, 28 | sstri 3441 |
. . . . . . 7
                    
  |
30 | 13, 29 | sstri 3441 |
. . . . . 6
  
                   ![[,] [,]](_icc.gif)  
 
  |
31 | 10 | fdmi 5734 |
. . . . . 6
   |
32 | 30, 31 | sseqtr4i 3465 |
. . . . 5
  
                   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif) |
33 | | funimass4 5916 |
. . . . 5
 
  
                   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)   ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
 
    
                   ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)       |
34 | 12, 32, 33 | mp2an 678 |
. . . 4
  ![[,] [,]](_icc.gif)    
                   ![[,] [,]](_icc.gif)  
 
    
                   ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)      |
35 | 9, 34 | sylibr 216 |
. . 3
    
 ![[,] [,]](_icc.gif)   

                   ![[,] [,]](_icc.gif)        |
36 | | sspwuni 4367 |
. . 3
  ![[,] [,]](_icc.gif)    
                   ![[,] [,]](_icc.gif)  
 
   ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
 
  |
37 | 35, 36 | sylib 200 |
. 2
    
  ![[,] [,]](_icc.gif)                      
 ![[,] [,]](_icc.gif)       |
38 | | eqid 2451 |
. . . . . . 7
           |
39 | 38 | rexmet 21809 |
. . . . . 6
           |
40 | | eqid 2451 |
. . . . . . . 8
    
        
     |
41 | 38, 40 | tgioo 21814 |
. . . . . . 7
        
     |
42 | 41 | mopni2 21508 |
. . . . . 6
   
           

        
    
  |
43 | 39, 42 | mp3an1 1351 |
. . . . 5
               
    
  |
44 | | elssuni 4227 |
. . . . . . . . . . 11
    
   
   |
45 | | uniretop 21783 |
. . . . . . . . . . 11
      |
46 | 44, 45 | syl6sseqr 3479 |
. . . . . . . . . 10
    
  |
47 | 46 | sselda 3432 |
. . . . . . . . 9
         |
48 | | rpre 11308 |
. . . . . . . . 9

  |
49 | 38 | bl2ioo 21810 |
. . . . . . . . 9
 
       
                |
50 | 47, 48, 49 | syl2an 480 |
. . . . . . . 8
      


       
               |
51 | 50 | sseq1d 3459 |
. . . . . . 7
      


       
     
           |
52 | | 2re 10679 |
. . . . . . . . . . 11
 |
53 | | 1lt2 10776 |
. . . . . . . . . . 11
 |
54 | | expnlbnd 12402 |
. . . . . . . . . . 11
            |
55 | 52, 53, 54 | mp3an23 1356 |
. . . . . . . . . 10

         |
56 | 55 | ad2antrl 734 |
. . . . . . . . 9
      

           
        |
57 | 47 | ad2antrr 732 |
. . . . . . . . . . . 12
       

           
       
  |
58 | | 2nn 10767 |
. . . . . . . . . . . . . . . . . 18
 |
59 | | nnnn0 10876 |
. . . . . . . . . . . . . . . . . . 19
   |
60 | 59 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . 18
       

           
       
  |
61 | | nnexpcl 12285 |
. . . . . . . . . . . . . . . . . 18
 
       |
62 | 58, 60, 61 | sylancr 669 |
. . . . . . . . . . . . . . . . 17
       

           
       
      |
63 | 62 | nnred 10624 |
. . . . . . . . . . . . . . . 16
       

           
       
      |
64 | 57, 63 | remulcld 9671 |
. . . . . . . . . . . . . . 15
       

           
       
        |
65 | | fllelt 12033 |
. . . . . . . . . . . . . . 15
                 
                           |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
       

           
       
                           
          |
67 | 66 | simpld 461 |
. . . . . . . . . . . . 13
       

           
       
                  |
68 | | reflcl 12032 |
. . . . . . . . . . . . . . 15
                   |
69 | 64, 68 | syl 17 |
. . . . . . . . . . . . . 14
       

           
       
            |
70 | 62 | nngt0d 10653 |
. . . . . . . . . . . . . 14
       

           
       
      |
71 | | ledivmul2 10484 |
. . . . . . . . . . . . . 14
           
                                     
         |
72 | 69, 57, 63, 70, 71 | syl112anc 1272 |
. . . . . . . . . . . . 13
       

           
       
                
                   |
73 | 67, 72 | mpbird 236 |
. . . . . . . . . . . 12
       

           
       
                  |
74 | | peano2re 9806 |
. . . . . . . . . . . . . . 15
                         |
75 | 69, 74 | syl 17 |
. . . . . . . . . . . . . 14
       

           
       
              |
76 | 75, 62 | nndivred 10658 |
. . . . . . . . . . . . 13
       

           
       
                    |
77 | 66 | simprd 465 |
. . . . . . . . . . . . . 14
       

           
       
                    |
78 | | ltmuldiv 10478 |
. . . . . . . . . . . . . . 15
      
                 
                  
     
               |
79 | 57, 75, 63, 70, 78 | syl112anc 1272 |
. . . . . . . . . . . . . 14
       

           
       
                  
     
               |
80 | 77, 79 | mpbid 214 |
. . . . . . . . . . . . 13
       

           
       
     
              |
81 | 57, 76, 80 | ltled 9783 |
. . . . . . . . . . . 12
       

           
       
     
              |
82 | 69, 62 | nndivred 10658 |
. . . . . . . . . . . . 13
       

           
       
                  |
83 | | elicc2 11699 |
. . . . . . . . . . . . 13
      
                                                 ![[,] [,]](_icc.gif)      
                                   
                |
84 | 82, 76, 83 | syl2anc 667 |
. . . . . . . . . . . 12
       

           
       
                   ![[,] [,]](_icc.gif)      
                                   
                |
85 | 57, 73, 81, 84 | mpbir3and 1191 |
. . . . . . . . . . 11
       

           
       
                  ![[,] [,]](_icc.gif)      
               |
86 | 64 | flcld 12034 |
. . . . . . . . . . . . . 14
       

           
       
            |
87 | 22 | dyadval 22550 |
. . . . . . . . . . . . . 14
           
     
        
                                                           |
88 | 86, 60, 87 | syl2anc 667 |
. . . . . . . . . . . . 13
       

           
       
                                                                         |
89 | 88 | fveq2d 5869 |
. . . . . . . . . . . 12
       

           
       
 ![[,] [,]](_icc.gif)      
        
                      ![[,] [,]](_icc.gif)                                          |
90 | | df-ov 6293 |
. . . . . . . . . . . 12
                  ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                                         |
91 | 89, 90 | syl6eqr 2503 |
. . . . . . . . . . 11
       

           
       
 ![[,] [,]](_icc.gif)      
        
                                       ![[,] [,]](_icc.gif)      
               |
92 | 85, 91 | eleqtrrd 2532 |
. . . . . . . . . 10
       

           
       
 ![[,] [,]](_icc.gif)               
                       |
93 | | ffn 5728 |
. . . . . . . . . . . . . . 15
                           
                          |
94 | 23, 93 | ax-mp 5 |
. . . . . . . . . . . . . 14
 
                     |
95 | | fnovrn 6444 |
. . . . . . . . . . . . . 14
   
                                                                                       |
96 | 94, 95 | mp3an1 1351 |
. . . . . . . . . . . . 13
           
     
        
                    

                    |
97 | 86, 60, 96 | syl2anc 667 |
. . . . . . . . . . . 12
       

           
       
                                  

                    |
98 | | simplrl 770 |
. . . . . . . . . . . . . . . . . 18
       

           
       
  |
99 | 98 | rpred 11341 |
. . . . . . . . . . . . . . . . 17
       

           
       
  |
100 | 57, 99 | resubcld 10047 |
. . . . . . . . . . . . . . . 16
       

           
       
    |
101 | 100 | rexrd 9690 |
. . . . . . . . . . . . . . 15
       

           
       
    |
102 | 57, 99 | readdcld 9670 |
. . . . . . . . . . . . . . . 16
       

           
       
    |
103 | 102 | rexrd 9690 |
. . . . . . . . . . . . . . 15
       

           
       
    |
104 | 82, 99 | readdcld 9670 |
. . . . . . . . . . . . . . . . 17
       

           
       
                    |
105 | 69 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
            |
106 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
  |
107 | 63 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
      |
108 | 62 | nnne0d 10654 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
      |
109 | 105, 106,
107, 108 | divdird 10421 |
. . . . . . . . . . . . . . . . . 18
       

           
       
                                            |
110 | 62 | nnrecred 10655 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
        |
111 | | simprr 766 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
        |
112 | 110, 99, 82, 111 | ltadd2dd 9794 |
. . . . . . . . . . . . . . . . . 18
       

           
       
                                            |
113 | 109, 112 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . 17
       

           
       
                                      |
114 | 57, 76, 104, 80, 113 | lttrd 9796 |
. . . . . . . . . . . . . . . 16
       

           
       
     
              |
115 | 57, 99, 82 | ltsubaddd 10209 |
. . . . . . . . . . . . . . . 16
       

           
       
                  
     
               |
116 | 114, 115 | mpbird 236 |
. . . . . . . . . . . . . . 15
       

           
       
      
             |
117 | 57, 110 | readdcld 9670 |
. . . . . . . . . . . . . . . 16
       

           
       
          |
118 | 82, 57, 110, 73 | leadd1dd 10227 |
. . . . . . . . . . . . . . . . 17
       

           
       
                                  |
119 | 109, 118 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . 16
       

           
       
                            |
120 | 110, 99, 57, 111 | ltadd2dd 9794 |
. . . . . . . . . . . . . . . 16
       

           
       
            |
121 | 76, 117, 102, 119, 120 | lelttrd 9793 |
. . . . . . . . . . . . . . 15
       

           
       
                      |
122 | | iccssioo 11703 |
. . . . . . . . . . . . . . 15
                                                      
            ![[,] [,]](_icc.gif)                              |
123 | 101, 103,
116, 121, 122 | syl22anc 1269 |
. . . . . . . . . . . . . 14
       

           
       
                  ![[,] [,]](_icc.gif)                              |
124 | 91, 123 | eqsstrd 3466 |
. . . . . . . . . . . . 13
       

           
       
 ![[,] [,]](_icc.gif)      
        
                               |
125 | | simplrr 771 |
. . . . . . . . . . . . 13
       

           
       
          |
126 | 124, 125 | sstrd 3442 |
. . . . . . . . . . . 12
       

           
       
 ![[,] [,]](_icc.gif)      
        
                       |
127 | | fveq2 5865 |
. . . . . . . . . . . . . 14
                                    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                       |
128 | 127 | sseq1d 3459 |
. . . . . . . . . . . . 13
                                     ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      
        
                        |
129 | 128 | elrab 3196 |
. . . . . . . . . . . 12
                                    

                   ![[,] [,]](_icc.gif)                                       

                 
 ![[,] [,]](_icc.gif)      
        
                        |
130 | 97, 126, 129 | sylanbrc 670 |
. . . . . . . . . . 11
       

           
       
                                                        ![[,] [,]](_icc.gif)  
   |
131 | | funfvima2 6141 |
. . . . . . . . . . . 12
 
  
                   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      
        
                                          ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)                                      ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
     |
132 | 12, 32, 131 | mp2an 678 |
. . . . . . . . . . 11
                                    

                   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)                                      ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
    |
133 | 130, 132 | syl 17 |
. . . . . . . . . 10
       

           
       
 ![[,] [,]](_icc.gif)      
        
                      ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
    |
134 | | elunii 4203 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      
        
                      ![[,] [,]](_icc.gif)               
                      ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
     ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
    |
135 | 92, 133, 134 | syl2anc 667 |
. . . . . . . . 9
       

           
       
  ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
    |
136 | 56, 135 | rexlimddv 2883 |
. . . . . . . 8
      

          
  ![[,] [,]](_icc.gif)                      
 ![[,] [,]](_icc.gif)       |
137 | 136 | expr 620 |
. . . . . . 7
      


           ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
     |
138 | 51, 137 | sylbid 219 |
. . . . . 6
      


       
     
  ![[,] [,]](_icc.gif)   

                   ![[,] [,]](_icc.gif)        |
139 | 138 | rexlimdva 2879 |
. . . . 5
        
      
     
  ![[,] [,]](_icc.gif)   

                   ![[,] [,]](_icc.gif)        |
140 | 43, 139 | mpd 15 |
. . . 4
         ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
    |
141 | 140 | ex 436 |
. . 3
    

  ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)  
     |
142 | 141 | ssrdv 3438 |
. 2
    
  ![[,] [,]](_icc.gif)                      
 ![[,] [,]](_icc.gif)       |
143 | 37, 142 | eqssd 3449 |
1
    
  ![[,] [,]](_icc.gif)                      
 ![[,] [,]](_icc.gif)       |