Step | Hyp | Ref
| Expression |
1 | | fveq2 5879 |
. . . . . . . . 9
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
2 | 1 | sseq1d 3445 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      |
3 | 2 | elrab 3184 |
. . . . . . 7
 
 ![[,] [,]](_icc.gif)   

 ![[,] [,]](_icc.gif)      |
4 | | simprr 774 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)  
 
 ![[,] [,]](_icc.gif)     |
5 | | fvex 5889 |
. . . . . . . . 9
 ![[,] [,]](_icc.gif)    |
6 | 5 | elpw 3948 |
. . . . . . . 8
  ![[,] [,]](_icc.gif)   
 ![[,] [,]](_icc.gif)     |
7 | 4, 6 | sylibr 217 |
. . . . . . 7
        ![[,] [,]](_icc.gif)  
 
 ![[,] [,]](_icc.gif)      |
8 | 3, 7 | sylan2b 483 |
. . . . . 6
        ![[,] [,]](_icc.gif)  
 
 ![[,] [,]](_icc.gif)      |
9 | 8 | ralrimiva 2809 |
. . . . 5
    
   ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)      |
10 | | iccf 11758 |
. . . . . . 7
![[,] [,]](_icc.gif)  
     |
11 | | ffun 5742 |
. . . . . . 7
 ![[,] [,]](_icc.gif)      
![[,] [,]](_icc.gif)  |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
![[,] [,]](_icc.gif) |
13 | | ssrab2 3500 |
. . . . . . . 8
  ![[,] [,]](_icc.gif)  
  |
14 | | dyadmbl.1 |
. . . . . . . . . . 11
 
                   |
15 | 14 | dyadf 22628 |
. . . . . . . . . 10
     
    |
16 | | frn 5747 |
. . . . . . . . . 10
       
  
    |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
    |
18 | | inss2 3644 |
. . . . . . . . . 10
      |
19 | | rexpssxrxp 9703 |
. . . . . . . . . 10
     |
20 | 18, 19 | sstri 3427 |
. . . . . . . . 9
      |
21 | 17, 20 | sstri 3427 |
. . . . . . . 8

  |
22 | 13, 21 | sstri 3427 |
. . . . . . 7
  ![[,] [,]](_icc.gif)  
 
  |
23 | 10 | fdmi 5746 |
. . . . . . 7
   |
24 | 22, 23 | sseqtr4i 3451 |
. . . . . 6
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif) |
25 | | funimass4 5930 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
 
    ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)       |
26 | 12, 24, 25 | mp2an 686 |
. . . . 5
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
 
    ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)      |
27 | 9, 26 | sylibr 217 |
. . . 4
    
 ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
 
   |
28 | | sspwuni 4360 |
. . . 4
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
 
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
 
  |
29 | 27, 28 | sylib 201 |
. . 3
    
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)       |
30 | | eqid 2471 |
. . . . . . . 8
           |
31 | 30 | rexmet 21887 |
. . . . . . 7
           |
32 | | eqid 2471 |
. . . . . . . . 9
    
        
     |
33 | 30, 32 | tgioo 21892 |
. . . . . . . 8
        
     |
34 | 33 | mopni2 21586 |
. . . . . . 7
   
           

        
    
  |
35 | 31, 34 | mp3an1 1377 |
. . . . . 6
               
    
  |
36 | | elssuni 4219 |
. . . . . . . . . . . 12
    
   
   |
37 | | uniretop 21861 |
. . . . . . . . . . . 12
      |
38 | 36, 37 | syl6sseqr 3465 |
. . . . . . . . . . 11
    
  |
39 | 38 | sselda 3418 |
. . . . . . . . . 10
         |
40 | | rpre 11331 |
. . . . . . . . . 10

  |
41 | 30 | bl2ioo 21888 |
. . . . . . . . . 10
 
       
                |
42 | 39, 40, 41 | syl2an 485 |
. . . . . . . . 9
      


       
               |
43 | 42 | sseq1d 3445 |
. . . . . . . 8
      


       
     
           |
44 | | 2re 10701 |
. . . . . . . . . . . 12
 |
45 | | 1lt2 10799 |
. . . . . . . . . . . 12
 |
46 | | expnlbnd 12440 |
. . . . . . . . . . . 12
            |
47 | 44, 45, 46 | mp3an23 1382 |
. . . . . . . . . . 11

         |
48 | 47 | ad2antrl 742 |
. . . . . . . . . 10
      

           
        |
49 | 39 | ad2antrr 740 |
. . . . . . . . . . . . 13
       

           
       
  |
50 | | 2nn 10790 |
. . . . . . . . . . . . . . . . . . 19
 |
51 | | nnnn0 10900 |
. . . . . . . . . . . . . . . . . . . 20
   |
52 | 51 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
  |
53 | | nnexpcl 12323 |
. . . . . . . . . . . . . . . . . . 19
 
       |
54 | 50, 52, 53 | sylancr 676 |
. . . . . . . . . . . . . . . . . 18
       

           
       
      |
55 | 54 | nnred 10646 |
. . . . . . . . . . . . . . . . 17
       

           
       
      |
56 | 49, 55 | remulcld 9689 |
. . . . . . . . . . . . . . . 16
       

           
       
        |
57 | | fllelt 12066 |
. . . . . . . . . . . . . . . 16
                 
                           |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . 15
       

           
       
                           
          |
59 | 58 | simpld 466 |
. . . . . . . . . . . . . 14
       

           
       
                  |
60 | | reflcl 12065 |
. . . . . . . . . . . . . . . 16
                   |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . . . 15
       

           
       
            |
62 | 54 | nngt0d 10675 |
. . . . . . . . . . . . . . 15
       

           
       
      |
63 | | ledivmul2 10506 |
. . . . . . . . . . . . . . 15
           
                                     
         |
64 | 61, 49, 55, 62, 63 | syl112anc 1296 |
. . . . . . . . . . . . . 14
       

           
       
                
                   |
65 | 59, 64 | mpbird 240 |
. . . . . . . . . . . . 13
       

           
       
                  |
66 | | peano2re 9824 |
. . . . . . . . . . . . . . . 16
                         |
67 | 61, 66 | syl 17 |
. . . . . . . . . . . . . . 15
       

           
       
              |
68 | 67, 54 | nndivred 10680 |
. . . . . . . . . . . . . 14
       

           
       
                    |
69 | 58 | simprd 470 |
. . . . . . . . . . . . . . 15
       

           
       
                    |
70 | | ltmuldiv 10500 |
. . . . . . . . . . . . . . . 16
      
                 
                  
     
               |
71 | 49, 67, 55, 62, 70 | syl112anc 1296 |
. . . . . . . . . . . . . . 15
       

           
       
                  
     
               |
72 | 69, 71 | mpbid 215 |
. . . . . . . . . . . . . 14
       

           
       
     
              |
73 | 49, 68, 72 | ltled 9800 |
. . . . . . . . . . . . 13
       

           
       
     
              |
74 | 61, 54 | nndivred 10680 |
. . . . . . . . . . . . . 14
       

           
       
                  |
75 | | elicc2 11724 |
. . . . . . . . . . . . . 14
      
                                                 ![[,] [,]](_icc.gif)      
                                   
                |
76 | 74, 68, 75 | syl2anc 673 |
. . . . . . . . . . . . 13
       

           
       
                   ![[,] [,]](_icc.gif)      
                                   
                |
77 | 49, 65, 73, 76 | mpbir3and 1213 |
. . . . . . . . . . . 12
       

           
       
                  ![[,] [,]](_icc.gif)      
               |
78 | 56 | flcld 12067 |
. . . . . . . . . . . . . . 15
       

           
       
            |
79 | 14 | dyadval 22629 |
. . . . . . . . . . . . . . 15
           
     
                                                |
80 | 78, 52, 79 | syl2anc 673 |
. . . . . . . . . . . . . 14
       

           
       
                                                     |
81 | 80 | fveq2d 5883 |
. . . . . . . . . . . . 13
       

           
       
 ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)                                          |
82 | | df-ov 6311 |
. . . . . . . . . . . . 13
                  ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                                         |
83 | 81, 82 | syl6eqr 2523 |
. . . . . . . . . . . 12
       

           
       
 ![[,] [,]](_icc.gif)      
               
            ![[,] [,]](_icc.gif)                      |
84 | 77, 83 | eleqtrrd 2552 |
. . . . . . . . . . 11
       

           
       
 ![[,] [,]](_icc.gif)                   |
85 | | ffn 5739 |
. . . . . . . . . . . . . . . 16
       
      |
86 | 15, 85 | ax-mp 5 |
. . . . . . . . . . . . . . 15

  |
87 | | fnovrn 6463 |
. . . . . . . . . . . . . . 15
                               |
88 | 86, 87 | mp3an1 1377 |
. . . . . . . . . . . . . 14
           
     
           |
89 | 78, 52, 88 | syl2anc 673 |
. . . . . . . . . . . . 13
       

           
       
                |
90 | | simplrl 778 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
  |
91 | 90 | rpred 11364 |
. . . . . . . . . . . . . . . . . 18
       

           
       
  |
92 | 49, 91 | resubcld 10068 |
. . . . . . . . . . . . . . . . 17
       

           
       
    |
93 | 92 | rexrd 9708 |
. . . . . . . . . . . . . . . 16
       

           
       
    |
94 | 49, 91 | readdcld 9688 |
. . . . . . . . . . . . . . . . 17
       

           
       
    |
95 | 94 | rexrd 9708 |
. . . . . . . . . . . . . . . 16
       

           
       
    |
96 | 74, 91 | readdcld 9688 |
. . . . . . . . . . . . . . . . . 18
       

           
       
                    |
97 | 61 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
       

           
       
            |
98 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . . . 20
       

           
       
  |
99 | 55 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
       

           
       
      |
100 | 54 | nnne0d 10676 |
. . . . . . . . . . . . . . . . . . . 20
       

           
       
      |
101 | 97, 98, 99, 100 | divdird 10443 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
                                            |
102 | 54 | nnrecred 10677 |
. . . . . . . . . . . . . . . . . . . 20
       

           
       
        |
103 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . 20
       

           
       
        |
104 | 102, 91, 74, 103 | ltadd2dd 9811 |
. . . . . . . . . . . . . . . . . . 19
       

           
       
                                            |
105 | 101, 104 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . 18
       

           
       
                                      |
106 | 49, 68, 96, 72, 105 | lttrd 9813 |
. . . . . . . . . . . . . . . . 17
       

           
       
     
              |
107 | 49, 91, 74 | ltsubaddd 10230 |
. . . . . . . . . . . . . . . . 17
       

           
       
                  
     
               |
108 | 106, 107 | mpbird 240 |
. . . . . . . . . . . . . . . 16
       

           
       
      
             |
109 | 49, 102 | readdcld 9688 |
. . . . . . . . . . . . . . . . 17
       

           
       
          |
110 | 74, 49, 102, 65 | leadd1dd 10248 |
. . . . . . . . . . . . . . . . . 18
       

           
       
                                  |
111 | 101, 110 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . 17
       

           
       
                            |
112 | 102, 91, 49, 103 | ltadd2dd 9811 |
. . . . . . . . . . . . . . . . 17
       

           
       
            |
113 | 68, 109, 94, 111, 112 | lelttrd 9810 |
. . . . . . . . . . . . . . . 16
       

           
       
                      |
114 | | iccssioo 11728 |
. . . . . . . . . . . . . . . 16
                                                      
            ![[,] [,]](_icc.gif)                              |
115 | 93, 95, 108, 113, 114 | syl22anc 1293 |
. . . . . . . . . . . . . . 15
       

           
       
                  ![[,] [,]](_icc.gif)                              |
116 | 83, 115 | eqsstrd 3452 |
. . . . . . . . . . . . . 14
       

           
       
 ![[,] [,]](_icc.gif)      
                    |
117 | | simplrr 779 |
. . . . . . . . . . . . . 14
       

           
       
          |
118 | 116, 117 | sstrd 3428 |
. . . . . . . . . . . . 13
       

           
       
 ![[,] [,]](_icc.gif)      
            |
119 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
                ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                   |
120 | 119 | sseq1d 3445 |
. . . . . . . . . . . . . 14
                 ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      
             |
121 | 120 | elrab 3184 |
. . . . . . . . . . . . 13
               
 ![[,] [,]](_icc.gif)   
              
 ![[,] [,]](_icc.gif)                    |
122 | 89, 118, 121 | sylanbrc 677 |
. . . . . . . . . . . 12
       

           
       
                ![[,] [,]](_icc.gif)  
   |
123 | | funfvima2 6158 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     |
124 | 12, 24, 123 | mp2an 686 |
. . . . . . . . . . . 12
               
 ![[,] [,]](_icc.gif)   
 ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
    |
125 | 122, 124 | syl 17 |
. . . . . . . . . . 11
       

           
       
 ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
    |
126 | | elunii 4195 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
    |
127 | 84, 125, 126 | syl2anc 673 |
. . . . . . . . . 10
       

           
       
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
    |
128 | 48, 127 | rexlimddv 2875 |
. . . . . . . . 9
      

          
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)       |
129 | 128 | expr 626 |
. . . . . . . 8
      


           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     |
130 | 43, 129 | sylbid 223 |
. . . . . . 7
      


       
     
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     |
131 | 130 | rexlimdva 2871 |
. . . . . 6
        
      
     
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     |
132 | 35, 131 | mpd 15 |
. . . . 5
         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
    |
133 | 132 | ex 441 |
. . . 4
    

  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     |
134 | 133 | ssrdv 3424 |
. . 3
    
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)       |
135 | 29, 134 | eqssd 3435 |
. 2
    
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)       |
136 | | fveq2 5879 |
. . . . . . 7
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
137 | 136 | sseq1d 3445 |
. . . . . 6
   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
138 | | equequ1 1875 |
. . . . . 6
 
   |
139 | 137, 138 | imbi12d 327 |
. . . . 5
    ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       |
140 | 139 | ralbidv 2829 |
. . . 4
  
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)       |
141 | 140 | cbvrabv 3030 |
. . 3
 
 ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)      |
142 | 13 | a1i 11 |
. . 3
    
  ![[,] [,]](_icc.gif)      |
143 | 14, 141, 142 | dyadmbl 22637 |
. 2
    
  ![[,] [,]](_icc.gif)  
 ![[,] [,]](_icc.gif)       |
144 | 135, 143 | eqeltrrd 2550 |
1
    
  |