Step | Hyp | Ref
| Expression |
1 | | 0lt1 8074 |
. . . 4
 |
2 | | 0re 7948 |
. . . . 5
 |
3 | | 1re 7947 |
. . . . 5
 |
4 | | lttri3 8027 |
. . . . . . . 8
 
  
    |
5 | 4 | adantl 277 |
. . . . . . 7
     
    |
6 | | elrabi 2890 |
. . . . . . . . . . . 12
       
     |
7 | | elpri 3614 |
. . . . . . . . . . . 12
        |
8 | 6, 7 | syl 14 |
. . . . . . . . . . 11
       
    |
9 | | eleq1 2240 |
. . . . . . . . . . . . 13
 
   |
10 | 2, 9 | mpbiri 168 |
. . . . . . . . . . . 12
   |
11 | | eleq1 2240 |
. . . . . . . . . . . . 13
 
   |
12 | 3, 11 | mpbiri 168 |
. . . . . . . . . . . 12
   |
13 | 10, 12 | jaoi 716 |
. . . . . . . . . . 11
     |
14 | 8, 13 | syl 14 |
. . . . . . . . . 10
       
  |
15 | 14 | ssriv 3159 |
. . . . . . . . 9
        |
16 | | eqid 2177 |
. . . . . . . . . . . 12
 |
17 | 16 | orci 731 |
. . . . . . . . . . 11
   |
18 | 2 | elexi 2749 |
. . . . . . . . . . . . 13
 |
19 | 18 | prid1 3697 |
. . . . . . . . . . . 12
    |
20 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
     |
21 | 20 | orbi1d 791 |
. . . . . . . . . . . . 13
   
     |
22 | 21 | elrab3 2894 |
. . . . . . . . . . . 12
           
     |
23 | 19, 22 | ax-mp 5 |
. . . . . . . . . . 11
       
    |
24 | 17, 23 | mpbir 146 |
. . . . . . . . . 10
        |
25 | | elex2 2753 |
. . . . . . . . . 10
       

         |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . 9

        |
27 | | elrabi 2890 |
. . . . . . . . . . . 12
       
     |
28 | | elpri 3614 |
. . . . . . . . . . . . 13
        |
29 | | 0le1 8428 |
. . . . . . . . . . . . . . 15
 |
30 | | breq1 4003 |
. . . . . . . . . . . . . . 15
 
   |
31 | 29, 30 | mpbiri 168 |
. . . . . . . . . . . . . 14
   |
32 | 3 | eqlei2 8042 |
. . . . . . . . . . . . . 14
   |
33 | 31, 32 | jaoi 716 |
. . . . . . . . . . . . 13
     |
34 | 28, 33 | syl 14 |
. . . . . . . . . . . 12
      |
35 | 27, 34 | syl 14 |
. . . . . . . . . . 11
       
  |
36 | 35 | rgen 2530 |
. . . . . . . . . 10
          |
37 | | breq2 4004 |
. . . . . . . . . . . 12
 
   |
38 | 37 | ralbidv 2477 |
. . . . . . . . . . 11
  
       
            |
39 | 38 | rspcev 2841 |
. . . . . . . . . 10
            
           |
40 | 3, 36, 39 | mp2an 426 |
. . . . . . . . 9
           |
41 | | prexg 4208 |
. . . . . . . . . . . 12
 
      |
42 | 2, 3, 41 | mp2an 426 |
. . . . . . . . . . 11
    |
43 | 42 | rabex 4144 |
. . . . . . . . . 10
        |
44 | | sseq1 3178 |
. . . . . . . . . . . 12
       

          |
45 | | eleq2 2241 |
. . . . . . . . . . . . 13
       

          |
46 | 45 | exbidv 1825 |
. . . . . . . . . . . 12
       
             |
47 | | raleq 2672 |
. . . . . . . . . . . . 13
       
 
        
   |
48 | 47 | rexbidv 2478 |
. . . . . . . . . . . 12
       
  
             |
49 | 44, 46, 48 | 3anbi123d 1312 |
. . . . . . . . . . 11
       
 

  
       

      
              |
50 | | raleq 2672 |
. . . . . . . . . . . . 13
       
 
           |
51 | | rexeq 2673 |
. . . . . . . . . . . . . . 15
       
 
            |
52 | 51 | imbi2d 230 |
. . . . . . . . . . . . . 14
       
  


             |
53 | 52 | ralbidv 2477 |
. . . . . . . . . . . . 13
       
 

 
 
             |
54 | 50, 53 | anbi12d 473 |
. . . . . . . . . . . 12
       
  
 
                            |
55 | 54 | rexbidv 2478 |
. . . . . . . . . . 11
       
   
 
   
                         |
56 | 49, 55 | imbi12d 234 |
. . . . . . . . . 10
       
      
  
 

  
         
        
        
                           |
57 | | sup3exmid.ex |
. . . . . . . . . 10
 

   
 
 
     |
58 | 43, 56, 57 | vtocl 2791 |
. . . . . . . . 9
         
        
        
                         |
59 | 15, 26, 40, 58 | mp3an 1337 |
. . . . . . . 8
                        |
60 | 59 | a1i 9 |
. . . . . . 7
                         |
61 | 5, 60 | supclti 6991 |
. . . . . 6
          
  |
62 | 61 | mptru 1362 |
. . . . 5
         
  |
63 | | axltwlin 8015 |
. . . . 5
 
         
  
           
          
    |
64 | 2, 3, 62, 63 | mp3an 1337 |
. . . 4
 
         
          
    |
65 | 1, 64 | ax-mp 5 |
. . 3
           
          
  |
66 | 5, 60 | suplubti 6993 |
. . . . . . . 8
                          |
67 | 66 | mptru 1362 |
. . . . . . 7
            
            |
68 | 2, 67 | mpan 424 |
. . . . . 6
           

          |
69 | | df-rex 2461 |
. . . . . 6
         
             |
70 | 68, 69 | sylib 122 |
. . . . 5
           
             |
71 | | eqeq1 2184 |
. . . . . . . . 9
     |
72 | 71 | orbi1d 791 |
. . . . . . . 8
   
     |
73 | 72 | elrab 2893 |
. . . . . . 7
       
         |
74 | | simpr 110 |
. . . . . . . . . 10
        

  |
75 | 74 | gt0ne0d 8459 |
. . . . . . . . 9
        

  |
76 | 75 | neneqd 2368 |
. . . . . . . 8
        

  |
77 | | simplr 528 |
. . . . . . . 8
        

    |
78 | | orel1 725 |
. . . . . . . 8
       |
79 | 76, 77, 78 | sylc 62 |
. . . . . . 7
        

  |
80 | 73, 79 | sylanb 284 |
. . . . . 6
            |
81 | 80 | exlimiv 1598 |
. . . . 5
           
  |
82 | 70, 81 | syl 14 |
. . . 4
           
  |
83 | 3 | ltnri 8040 |
. . . . . 6
 |
84 | | iba 300 |
. . . . . . . . . . . 12
      
          |
85 | 84 | olcs 736 |
. . . . . . . . . . 11
               |
86 | 73, 85 | bitr4id 199 |
. . . . . . . . . 10
               |
87 | 86 | eqrdv 2175 |
. . . . . . . . 9
       
     |
88 | 87 | supeq1d 6980 |
. . . . . . . 8
           
      
  |
89 | 3 | a1i 9 |
. . . . . . . . . 10
  |
90 | 3 | elexi 2749 |
. . . . . . . . . . . 12
 |
91 | 90 | prid2 3698 |
. . . . . . . . . . 11
    |
92 | 91 | a1i 9 |
. . . . . . . . . 10
     |
93 | | elpri 3614 |
. . . . . . . . . . . 12
        |
94 | 2, 3 | lenlti 8048 |
. . . . . . . . . . . . . . 15

  |
95 | 29, 94 | mpbi 145 |
. . . . . . . . . . . . . 14
 |
96 | | breq2 4004 |
. . . . . . . . . . . . . 14
 
   |
97 | 95, 96 | mtbiri 675 |
. . . . . . . . . . . . 13
   |
98 | | breq2 4004 |
. . . . . . . . . . . . . 14
 
   |
99 | 83, 98 | mtbiri 675 |
. . . . . . . . . . . . 13
   |
100 | 97, 99 | jaoi 716 |
. . . . . . . . . . . 12
  
  |
101 | 93, 100 | syl 14 |
. . . . . . . . . . 11
      |
102 | 101 | adantl 277 |
. . . . . . . . . 10
       |
103 | 5, 89, 92, 102 | supmaxti 6997 |
. . . . . . . . 9
      
  |
104 | 103 | mptru 1362 |
. . . . . . . 8
        |
105 | 88, 104 | eqtrdi 2226 |
. . . . . . 7
           
  |
106 | 105 | breq1d 4010 |
. . . . . 6
            
   |
107 | 83, 106 | mtbiri 675 |
. . . . 5
              |
108 | 107 | con2i 627 |
. . . 4
              |
109 | 82, 108 | orim12i 759 |
. . 3
           
          
      |
110 | 65, 109 | ax-mp 5 |
. 2
   |
111 | | df-dc 835 |
. 2
DECID
    |
112 | 110, 111 | mpbir 146 |
1
DECID  |