Step | Hyp | Ref
| Expression |
1 | | xrofsup.5 |
. . 3
          |
2 | | xrofsup.1 |
. . . . . . . . . 10

  |
3 | 2 | sseld 3417 |
. . . . . . . . 9
     |
4 | | xrofsup.2 |
. . . . . . . . . 10

  |
5 | 4 | sseld 3417 |
. . . . . . . . 9
     |
6 | 3, 5 | anim12d 572 |
. . . . . . . 8
         |
7 | 6 | imp 436 |
. . . . . . 7
 

      |
8 | | xaddcl 11554 |
. . . . . . 7
          |
9 | 7, 8 | syl 17 |
. . . . . 6
 

         |
10 | 9 | ralrimivva 2814 |
. . . . 5
  
       |
11 | | fveq2 5879 |
. . . . . . . 8
                   |
12 | | df-ov 6311 |
. . . . . . . 8
              |
13 | 11, 12 | syl6eqr 2523 |
. . . . . . 7
                |
14 | 13 | eleq1d 2533 |
. . . . . 6
         
        |
15 | 14 | ralxp 4981 |
. . . . 5
 
       
 
       |
16 | 10, 15 | sylibr 217 |
. . . 4
            |
17 | | xaddf 11540 |
. . . . . 6
        |
18 | | ffun 5742 |
. . . . . 6
           |
19 | 17, 18 | ax-mp 5 |
. . . . 5
  |
20 | | xpss12 4945 |
. . . . . . 7
 
       |
21 | 2, 4, 20 | syl2anc 673 |
. . . . . 6
  
    |
22 | 17 | fdmi 5746 |
. . . . . 6

   |
23 | 21, 22 | syl6sseqr 3465 |
. . . . 5
  
   |
24 | | funimass4 5930 |
. . . . 5
   

 
                    |
25 | 19, 23, 24 | sylancr 676 |
. . . 4
                     |
26 | 16, 25 | mpbird 240 |
. . 3
          |
27 | 1, 26 | eqsstrd 3452 |
. 2

  |
28 | | supxrcl 11625 |
. . . 4

  
   |
29 | 2, 28 | syl 17 |
. . 3
       |
30 | | supxrcl 11625 |
. . . 4

  
   |
31 | 4, 30 | syl 17 |
. . 3
       |
32 | 29, 31 | xaddcld 11612 |
. 2
           
    |
33 | 1 | eleq2d 2534 |
. . . . 5
            |
34 | 33 | pm5.32i 649 |
. . . 4
 

           |
35 | | nfvd 1770 |
. . . . 5
 
       
    
      
    |
36 | | nfvd 1770 |
. . . . 5
 
       

          
    |
37 | 2 | ad2antrr 740 |
. . . . . . . . . . 11
           
    |
38 | | simprl 772 |
. . . . . . . . . . 11
           
    |
39 | | supxrub 11635 |
. . . . . . . . . . 11
 
       |
40 | 37, 38, 39 | syl2anc 673 |
. . . . . . . . . 10
           
        |
41 | 4 | ad2antrr 740 |
. . . . . . . . . . 11
           
    |
42 | | simprr 774 |
. . . . . . . . . . 11
           
    |
43 | | supxrub 11635 |
. . . . . . . . . . 11
 
       |
44 | 41, 42, 43 | syl2anc 673 |
. . . . . . . . . 10
           
        |
45 | 37, 38 | sseldd 3419 |
. . . . . . . . . . 11
           
    |
46 | 41, 42 | sseldd 3419 |
. . . . . . . . . . 11
           
    |
47 | 37, 28 | syl 17 |
. . . . . . . . . . 11
           
        |
48 | 41, 30 | syl 17 |
. . . . . . . . . . 11
           
        |
49 | | xle2add 11570 |
. . . . . . . . . . 11
           
                             
     |
50 | 45, 46, 47, 48, 49 | syl22anc 1293 |
. . . . . . . . . 10
           
            
        
      
     |
51 | 40, 44, 50 | mp2and 693 |
. . . . . . . . 9
           
      
          
    |
52 | 51 | ralrimivva 2814 |
. . . . . . . 8
 
       


        
      
    |
53 | | fvelima 5931 |
. . . . . . . . . . 11
  
                   |
54 | 19, 53 | mpan 684 |
. . . . . . . . . 10
        
          |
55 | 54 | adantl 473 |
. . . . . . . . 9
 
       
           |
56 | 13 | eqeq1d 2473 |
. . . . . . . . . 10
         
        |
57 | 56 | rexxp 4982 |
. . . . . . . . 9
         


       |
58 | 55, 57 | sylib 201 |
. . . . . . . 8
 
       


       |
59 | 52, 58 | r19.29d2r 2919 |
. . . . . . 7
 
       


     
          
          |
60 | | ancom 457 |
. . . . . . . 8
                                    
          
     |
61 | 60 | 2rexbii 2882 |
. . . . . . 7
  
                          
              
      
     |
62 | 59, 61 | sylib 201 |
. . . . . 6
 
       


                           |
63 | | breq1 4398 |
. . . . . . . . 9
                      
                  |
64 | 63 | biimpa 492 |
. . . . . . . 8
                      
             
    |
65 | 64 | reximi 2852 |
. . . . . . 7
                       
   
               |
66 | 65 | reximi 2852 |
. . . . . 6
  
                     
   

               |
67 | 62, 66 | syl 17 |
. . . . 5
 
       


               |
68 | 35, 36, 67 | 19.9d2r 28194 |
. . . 4
 
       
               |
69 | 34, 68 | sylbi 200 |
. . 3
 
           
    |
70 | 69 | ralrimiva 2809 |
. 2
     
      
    |
71 | 2 | ad2antrr 740 |
. . . . . 6
              
     |
72 | 4 | ad2antrr 740 |
. . . . . 6
              
     |
73 | | simplr 770 |
. . . . . . 7
              
     |
74 | 29 | ad2antrr 740 |
. . . . . . 7
              
         |
75 | 31 | ad2antrr 740 |
. . . . . . 7
              
         |
76 | | xrofsup.3 |
. . . . . . . 8
       |
77 | 76 | ad2antrr 740 |
. . . . . . 7
              
         |
78 | | xrofsup.4 |
. . . . . . . 8
       |
79 | 78 | ad2antrr 740 |
. . . . . . 7
              
         |
80 | | simpr 468 |
. . . . . . 7
              
             
    |
81 | 73, 74, 75, 77, 79, 80 | xlt2addrd 28413 |
. . . . . 6
              
                      |
82 | | nfv 1769 |
. . . . . . . 8
     |
83 | | nfcv 2612 |
. . . . . . . . 9
   |
84 | | nfre1 2846 |
. . . . . . . . 9
                   |
85 | 83, 84 | nfrex 2848 |
. . . . . . . 8
                    |
86 | 82, 85 | nfan 2031 |
. . . . . . 7
                        |
87 | | nfvd 1770 |
. . . . . . 7
    
                
  

       |
88 | | nfvd 1770 |
. . . . . . 7
    
                
  

       |
89 | | id 22 |
. . . . . . . . . . . 12
 
 
   |
90 | 89 | ralrimivw 2810 |
. . . . . . . . . . 11
 
      |
91 | 90 | ralrimivw 2810 |
. . . . . . . . . 10
 
       |
92 | 91 | adantr 472 |
. . . . . . . . 9
    
                
      |
93 | | simpr 468 |
. . . . . . . . 9
    
                
                   |
94 | 92, 93 | r19.29d2r 2919 |
. . . . . . . 8
    
                
                       |
95 | | simplrr 779 |
. . . . . . . . . . . . . . 15
   
  
                  

                    |
96 | 95 | 3anassrs 1256 |
. . . . . . . . . . . . . 14
                          


                    |
97 | 96 | simp1d 1042 |
. . . . . . . . . . . . 13
                          


          |
98 | | simp-4l 784 |
. . . . . . . . . . . . . 14
                          


       |
99 | | simplrl 778 |
. . . . . . . . . . . . . . . . 17
   
  
                  

   
   |
100 | 99 | 3anassrs 1256 |
. . . . . . . . . . . . . . . 16
                          


       |
101 | 100 | simpld 466 |
. . . . . . . . . . . . . . 15
                          


     |
102 | | simpllr 777 |
. . . . . . . . . . . . . . 15
                          


     |
103 | 101, 102 | sseldd 3419 |
. . . . . . . . . . . . . 14
                          


     |
104 | 100 | simprd 470 |
. . . . . . . . . . . . . . 15
                          


     |
105 | | simplr 770 |
. . . . . . . . . . . . . . 15
                          


  
  |
106 | 104, 105 | sseldd 3419 |
. . . . . . . . . . . . . 14
                          


  
  |
107 | 98, 103, 106 | jca32 544 |
. . . . . . . . . . . . 13
                          


    
 
    |
108 | | simpr 468 |
. . . . . . . . . . . . 13
                          


   
   |
109 | | xlt2add 11571 |
. . . . . . . . . . . . . . 15
      
 
              |
110 | 109 | imp 436 |
. . . . . . . . . . . . . 14
   
 
  
 
            |
111 | | breq1 4398 |
. . . . . . . . . . . . . . 15
                         |
112 | 111 | biimpar 493 |
. . . . . . . . . . . . . 14
                 
       |
113 | 110, 112 | sylan2 482 |
. . . . . . . . . . . . 13
              
          |
114 | 97, 107, 108, 113 | syl12anc 1290 |
. . . . . . . . . . . 12
                          


  
       |
115 | | simplll 776 |
. . . . . . . . . . . . . . 15
                     
    |
116 | | simprl 772 |
. . . . . . . . . . . . . . 15
                     
    |
117 | | simplr2 1073 |
. . . . . . . . . . . . . . 15
                     
 
  
   |
118 | | supxrlub 11636 |
. . . . . . . . . . . . . . . 16
 
 
  
 
   |
119 | 118 | biimpa 492 |
. . . . . . . . . . . . . . 15
            |
120 | 115, 116,
117, 119 | syl21anc 1291 |
. . . . . . . . . . . . . 14
                     
  
  |
121 | | simpllr 777 |
. . . . . . . . . . . . . . 15
                     
    |
122 | | simprr 774 |
. . . . . . . . . . . . . . 15
                     
    |
123 | | simplr3 1074 |
. . . . . . . . . . . . . . 15
                     
 
  
   |
124 | | supxrlub 11636 |
. . . . . . . . . . . . . . . 16
 
 
  
 
   |
125 | 124 | biimpa 492 |
. . . . . . . . . . . . . . 15
            |
126 | 121, 122,
123, 125 | syl21anc 1291 |
. . . . . . . . . . . . . 14
                     
  
  |
127 | | reeanv 2944 |
. . . . . . . . . . . . . 14
  


 

   |
128 | 120, 126,
127 | sylanbrc 677 |
. . . . . . . . . . . . 13
                     
  


   |
129 | 128 | ancoms 460 |
. . . . . . . . . . . 12
                        

    |
130 | 114, 129 | reximddv2 2860 |
. . . . . . . . . . 11
                        

       |
131 | 130 | ex 441 |
. . . . . . . . . 10
                      


        |
132 | 131 | reximdva 2858 |
. . . . . . . . 9

                                |
133 | 132 | reximia 2850 |
. . . . . . . 8
                     
   
       |
134 | 94, 133 | syl 17 |
. . . . . . 7
    
                
   
       |
135 | 86, 87, 88, 134 | 19.9d2rf 28193 |
. . . . . 6
    
                


       |
136 | 71, 72, 81, 135 | syl21anc 1291 |
. . . . 5
              
   

       |
137 | | simprl 772 |
. . . . . . . . . 10
 

    |
138 | | simprr 774 |
. . . . . . . . . 10
 

 
  |
139 | 19 | a1i 11 |
. . . . . . . . . 10
 

     |
140 | 23 | adantr 472 |
. . . . . . . . . 10
 

   
   |
141 | 137, 138,
139, 140 | elovimad 6348 |
. . . . . . . . 9
 

                |
142 | 1 | eleq2d 2534 |
. . . . . . . . . 10
                      |
143 | 142 | adantr 472 |
. . . . . . . . 9
 

                       |
144 | 141, 143 | mpbird 240 |
. . . . . . . 8
 

         |
145 | | simpr 468 |
. . . . . . . . 9
   
 
             |
146 | 145 | breq2d 4407 |
. . . . . . . 8
   
 
               |
147 | 144, 146 | rspcedv 3140 |
. . . . . . 7
 

       

   |
148 | 147 | rexlimdvva 2878 |
. . . . . 6
        

   |
149 | 148 | ad2antrr 740 |
. . . . 5
              
    

     
   |
150 | 136, 149 | mpd 15 |
. . . 4
              
   
  |
151 | 150 | ex 441 |
. . 3
 

    
      
 

   |
152 | 151 | ralrimiva 2809 |
. 2
                
   |
153 | | supxr2 11624 |
. 2
                  
   
      
              
 

                      |
154 | 27, 32, 70, 152, 153 | syl22anc 1293 |
1
               
    |