Step | Hyp | Ref
| Expression |
1 | | po0 4788 |
. . . 4
 |
2 | | res0 5127 |
. . . . . . 7
  |
3 | 2 | ineq2i 3642 |
. . . . . 6
      |
4 | | in0 3771 |
. . . . . 6
   |
5 | 3, 4 | eqtri 2483 |
. . . . 5
    |
6 | | xp0 5273 |
. . . . . . . . . 10
   |
7 | 6 | ineq2i 3642 |
. . . . . . . . 9
       |
8 | 7, 4 | eqtri 2483 |
. . . . . . . 8
     |
9 | 8 | coeq2i 5013 |
. . . . . . 7
      
          |
10 | | co02 5367 |
. . . . . . 7
       |
11 | 9, 10 | eqtri 2483 |
. . . . . 6
      
    |
12 | | 0ss 3774 |
. . . . . 6
 |
13 | 11, 12 | eqsstri 3473 |
. . . . 5
      
  
 |
14 | 5, 13 | pm3.2i 461 |
. . . 4
                |
15 | 1, 14 | 2th 247 |
. . 3
    
      
  
   |
16 | | poeq2 4777 |
. . . 4


   |
17 | | reseq2 5118 |
. . . . . . 7


   |
18 | 17 | ineq2d 3645 |
. . . . . 6

        |
19 | 18 | eqeq1d 2463 |
. . . . 5

          |
20 | | xpeq2 4867 |
. . . . . . . 8

      |
21 | 20 | ineq2d 3645 |
. . . . . . 7

          |
22 | 21 | coeq2d 5015 |
. . . . . 6

      
     
         |
23 | 22 | sseq1d 3470 |
. . . . 5

       
     
          |
24 | 19, 23 | anbi12d 722 |
. . . 4

    
      
   
   
      
  
    |
25 | 16, 24 | bibi12d 327 |
. . 3

 
          
    
    
      
  
     |
26 | 15, 25 | mpbiri 241 |
. 2


          
       |
27 | | r19.28zv 3875 |
. . . . . . 7

 
                 
              |
28 | 27 | ralbidv 2838 |
. . . . . 6

 

              

                 |
29 | | r19.28zv 3875 |
. . . . . 6

 
          
   
   

      
       |
30 | 28, 29 | bitrd 261 |
. . . . 5

 

                 

              |
31 | 30 | ralbidv 2838 |
. . . 4

 


              

                  |
32 | | r19.26 2928 |
. . . 4
 
    
      
   
 
  


      
      |
33 | 31, 32 | syl6bb 269 |
. . 3

 


                  


              |
34 | | df-po 4773 |
. . 3




         
      |
35 | | disj 3816 |
. . . . 5
    
   |
36 | | df-ral 2753 |
. . . . 5
 

  
    |
37 | | opex 4677 |
. . . . . . . . . 10
  
 |
38 | | eleq1 2527 |
. . . . . . . . . . . 12
           |
39 | | df-br 4416 |
. . . . . . . . . . . 12
  
  
  |
40 | 38, 39 | syl6bbr 271 |
. . . . . . . . . . 11
          |
41 | | eleq1 2527 |
. . . . . . . . . . . . 13
             |
42 | | vex 3059 |
. . . . . . . . . . . . . . . 16
 |
43 | | ididg 5006 |
. . . . . . . . . . . . . . . 16
   |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 |
45 | 42 | brres 5129 |
. . . . . . . . . . . . . . 15
        |
46 | 44, 45 | mpbiran 934 |
. . . . . . . . . . . . . 14
   
  |
47 | | df-br 4416 |
. . . . . . . . . . . . . 14
          |
48 | 46, 47 | bitr3i 259 |
. . . . . . . . . . . . 13

  
   |
49 | 41, 48 | syl6bbr 271 |
. . . . . . . . . . . 12
         |
50 | 49 | notbid 300 |
. . . . . . . . . . 11
    

   |
51 | 40, 50 | imbi12d 326 |
. . . . . . . . . 10
     
 
  
    |
52 | 37, 51 | spcv 3151 |
. . . . . . . . 9
   
 
  
   |
53 | 52 | con2d 120 |
. . . . . . . 8
   
 

     |
54 | 53 | alrimiv 1783 |
. . . . . . 7
   
 
        |
55 | | relres 5150 |
. . . . . . . . . . . 12
  |
56 | | elrel 4955 |
. . . . . . . . . . . 12
  
 
  
     |
57 | 55, 56 | mpan 681 |
. . . . . . . . . . 11
    
     |
58 | 57 | ancri 559 |
. . . . . . . . . 10
     
  
    |
59 | | eleq1 2527 |
. . . . . . . . . . . . . . . 16
 
   |
60 | | breq12 4420 |
. . . . . . . . . . . . . . . . . 18
 
         |
61 | 60 | anidms 655 |
. . . . . . . . . . . . . . . . 17
   
     |
62 | 61 | notbid 300 |
. . . . . . . . . . . . . . . 16
   
     |
63 | 59, 62 | imbi12d 326 |
. . . . . . . . . . . . . . 15
      
      |
64 | 63 | spv 2114 |
. . . . . . . . . . . . . 14
   
         |
65 | | breq2 4419 |
. . . . . . . . . . . . . . . . . 18
   
     |
66 | 65 | notbid 300 |
. . . . . . . . . . . . . . . . 17
   
     |
67 | 66 | imbi2d 322 |
. . . . . . . . . . . . . . . 16
      
      |
68 | 67 | biimpcd 232 |
. . . . . . . . . . . . . . 15
     

      |
69 | 68 | impd 437 |
. . . . . . . . . . . . . 14
             |
70 | 64, 69 | syl 17 |
. . . . . . . . . . . . 13
   
           |
71 | | eleq1 2527 |
. . . . . . . . . . . . . . 15
        
    |
72 | | vex 3059 |
. . . . . . . . . . . . . . . . 17
 |
73 | 72 | brres 5129 |
. . . . . . . . . . . . . . . 16
        |
74 | | df-br 4416 |
. . . . . . . . . . . . . . . 16
          |
75 | 72 | ideq 5005 |
. . . . . . . . . . . . . . . . 17

  |
76 | 75 | anbi1i 706 |
. . . . . . . . . . . . . . . 16
 
 
   |
77 | 73, 74, 76 | 3bitr3ri 284 |
. . . . . . . . . . . . . . 15
 
   
   |
78 | 71, 77 | syl6bbr 271 |
. . . . . . . . . . . . . 14
           |
79 | | eleq1 2527 |
. . . . . . . . . . . . . . . 16
           |
80 | | df-br 4416 |
. . . . . . . . . . . . . . . 16
  
  
  |
81 | 79, 80 | syl6bbr 271 |
. . . . . . . . . . . . . . 15
          |
82 | 81 | notbid 300 |
. . . . . . . . . . . . . 14
    
     |
83 | 78, 82 | imbi12d 326 |
. . . . . . . . . . . . 13
      

 
       |
84 | 70, 83 | syl5ibrcom 230 |
. . . . . . . . . . . 12
   
        
    |
85 | 84 | exlimdvv 1790 |
. . . . . . . . . . 11
   
           
    |
86 | 85 | impd 437 |
. . . . . . . . . 10
   
       
  
 
   |
87 | 58, 86 | syl5 33 |
. . . . . . . . 9
   
   
    |
88 | 87 | con2d 120 |
. . . . . . . 8
   
   
    |
89 | 88 | alrimiv 1783 |
. . . . . . 7
   
     
    |
90 | 54, 89 | impbii 192 |
. . . . . 6
   
          |
91 | | df-ral 2753 |
. . . . . 6
 
 
        |
92 | 90, 91 | bitr4i 260 |
. . . . 5
   
       |
93 | 35, 36, 92 | 3bitri 279 |
. . . 4
         |
94 | | ralcom 2962 |
. . . . . . 7
 

      
  


            |
95 | | r19.23v 2878 |
. . . . . . . 8
 
      
  
 
           |
96 | 95 | ralbii 2830 |
. . . . . . 7
 

      
  

 
           |
97 | 94, 96 | bitri 257 |
. . . . . 6
 

      
  

 
           |
98 | 97 | ralbii 2830 |
. . . . 5
 


      
  


 
           |
99 | | brin 4465 |
. . . . . . . . . . . 12
                 |
100 | | brin 4465 |
. . . . . . . . . . . 12
                 |
101 | 99, 100 | anbi12i 708 |
. . . . . . . . . . 11
    
     
                        |
102 | | an4 838 |
. . . . . . . . . . . 12
                                       |
103 | | ancom 456 |
. . . . . . . . . . . 12
                                       |
104 | | ancom 456 |
. . . . . . . . . . . . . . 15
 
 
   |
105 | 104 | anbi1i 706 |
. . . . . . . . . . . . . 14
  


 
 
 
    |
106 | | brxp 4883 |
. . . . . . . . . . . . . . 15
    

   |
107 | | brxp 4883 |
. . . . . . . . . . . . . . 15
    

   |
108 | 106, 107 | anbi12i 708 |
. . . . . . . . . . . . . 14
              
    |
109 | | anandi 842 |
. . . . . . . . . . . . . 14
  
 
 
 
    |
110 | 105, 108,
109 | 3bitr4i 285 |
. . . . . . . . . . . . 13
            
    |
111 | 110 | anbi1i 706 |
. . . . . . . . . . . 12
                                 |
112 | 102, 103,
111 | 3bitri 279 |
. . . . . . . . . . 11
                                 |
113 | | anass 659 |
. . . . . . . . . . 11
   
                       |
114 | 101, 112,
113 | 3bitri 279 |
. . . . . . . . . 10
    
     
                  |
115 | 114 | exbii 1728 |
. . . . . . . . 9
                
                |
116 | 42, 72 | brco 5023 |
. . . . . . . . . 10
    
                          |
117 | | df-br 4416 |
. . . . . . . . . 10
    
                       |
118 | 116, 117 | bitr3i 259 |
. . . . . . . . 9
                
  
      
     |
119 | | df-rex 2754 |
. . . . . . . . . 10
   

           
           |
120 | | r19.42v 2956 |
. . . . . . . . . 10
   

          
         |
121 | 119, 120 | bitr3i 259 |
. . . . . . . . 9
     
        
 
           |
122 | 115, 118,
121 | 3bitr3ri 284 |
. . . . . . . 8
  


            
         |
123 | | df-br 4416 |
. . . . . . . 8
  
  
  |
124 | 122, 123 | imbi12i 332 |
. . . . . . 7
     
                    
         |
125 | 124 | 2albii 1702 |
. . . . . 6
       


                           
  
   |
126 | | r2al 2777 |
. . . . . . 7
 

 
     
  
        
     
      |
127 | | impexp 452 |
. . . . . . . 8
     
              
     
      |
128 | 127 | 2albii 1702 |
. . . . . . 7
       


                  
     
      |
129 | 126, 128 | bitr4i 260 |
. . . . . 6
 

 
     
  
      
              |
130 | | relco 5351 |
. . . . . . 7
      
    |
131 | | ssrel 4941 |
. . . . . . 7
   
              
                    
  
    |
132 | 130, 131 | ax-mp 5 |
. . . . . 6
       
                    
  
   |
133 | 125, 129,
132 | 3bitr4i 285 |
. . . . 5
 

 
     
  
         
  |
134 | 98, 133 | bitr2i 258 |
. . . 4
       
    

            |
135 | 93, 134 | anbi12i 708 |
. . 3
    
      
   
 
  


      
      |
136 | 33, 34, 135 | 3bitr4g 296 |
. 2


          
       |
137 | 26, 136 | pm2.61ine 2718 |
1

          
      |