Step | Hyp | Ref
| Expression |
1 | | elpri 3615 |
. . . . . . . . . 10
      
         

      |
2 | | exmidonfinlem.a |
. . . . . . . . . 10
     
      |
3 | 1, 2 | eleq2s 2272 |
. . . . . . . . 9
     

      |
4 | | eleq2 2241 |
. . . . . . . . . . . 12
             |
5 | 4 | biimpcd 159 |
. . . . . . . . . . 11
             |
6 | | elrabi 2890 |
. . . . . . . . . . . . . 14
         |
7 | | velsn 3609 |
. . . . . . . . . . . . . 14
  
  |
8 | 6, 7 | sylib 122 |
. . . . . . . . . . . . 13
       |
9 | | biidd 172 |
. . . . . . . . . . . . . . . . . 18
     |
10 | 9 | elrab 2893 |
. . . . . . . . . . . . . . . . 17
       
   |
11 | 10 | simprbi 275 |
. . . . . . . . . . . . . . . 16
       |
12 | 11 | notnotd 630 |
. . . . . . . . . . . . . . 15
    
  |
13 | | 0ex 4130 |
. . . . . . . . . . . . . . . . 17
 |
14 | 13 | snm 3712 |
. . . . . . . . . . . . . . . 16

   |
15 | | r19.3rmv 3513 |
. . . . . . . . . . . . . . . 16
   
       |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . 15

     |
17 | 12, 16 | sylib 122 |
. . . . . . . . . . . . . 14
          |
18 | | rabeq0 3452 |
. . . . . . . . . . . . . 14
          |
19 | 17, 18 | sylibr 134 |
. . . . . . . . . . . . 13
           |
20 | 8, 19 | eqtr4d 2213 |
. . . . . . . . . . . 12
           |
21 | | p0ex 4188 |
. . . . . . . . . . . . . . 15
   |
22 | 21 | rabex 4147 |
. . . . . . . . . . . . . 14
     |
23 | 22 | prid2 3699 |
. . . . . . . . . . . . 13
          
     |
24 | 23, 2 | eleqtrri 2253 |
. . . . . . . . . . . 12
     |
25 | 20, 24 | eqeltrdi 2268 |
. . . . . . . . . . 11
       |
26 | 5, 25 | syl6 33 |
. . . . . . . . . 10
         |
27 | | eleq2 2241 |
. . . . . . . . . . . 12
    

       |
28 | 27 | biimpcd 159 |
. . . . . . . . . . 11
     
       |
29 | | elrabi 2890 |
. . . . . . . . . . . . . 14
    
    |
30 | 29, 7 | sylib 122 |
. . . . . . . . . . . . 13
    
  |
31 | | biidd 172 |
. . . . . . . . . . . . . . . . 17
 
   |
32 | 31 | elrab 2893 |
. . . . . . . . . . . . . . . 16
           |
33 | 32 | simprbi 275 |
. . . . . . . . . . . . . . 15
    
  |
34 | | r19.3rmv 3513 |
. . . . . . . . . . . . . . . 16
   
       |
35 | 14, 34 | ax-mp 5 |
. . . . . . . . . . . . . . 15
      |
36 | 33, 35 | sylib 122 |
. . . . . . . . . . . . . 14
    
     |
37 | | rabeq0 3452 |
. . . . . . . . . . . . . 14
          |
38 | 36, 37 | sylibr 134 |
. . . . . . . . . . . . 13
    
   
  |
39 | 30, 38 | eqtr4d 2213 |
. . . . . . . . . . . 12
    

     |
40 | 21 | rabex 4147 |
. . . . . . . . . . . . . 14
   
 |
41 | 40 | prid1 3698 |
. . . . . . . . . . . . 13
   
     
      |
42 | 41, 2 | eleqtrri 2253 |
. . . . . . . . . . . 12
   
 |
43 | 39, 42 | eqeltrdi 2268 |
. . . . . . . . . . 11
    
  |
44 | 28, 43 | syl6 33 |
. . . . . . . . . 10
     
   |
45 | 26, 44 | jaod 717 |
. . . . . . . . 9
      
        |
46 | 3, 45 | mpan9 281 |
. . . . . . . 8
 
   |
47 | 46 | rgen2 2563 |
. . . . . . 7


 |
48 | | dftr5 4104 |
. . . . . . 7
  
  |
49 | 47, 48 | mpbir 146 |
. . . . . 6
 |
50 | | elpri 3615 |
. . . . . . . . 9
      
         

      |
51 | 50, 2 | eleq2s 2272 |
. . . . . . . 8
     

      |
52 | | ordtriexmidlem 4518 |
. . . . . . . . . . 11
   
 |
53 | 52 | ontrci 4427 |
. . . . . . . . . 10
     |
54 | | treq 4107 |
. . . . . . . . . 10
             |
55 | 53, 54 | mpbiri 168 |
. . . . . . . . 9
    
  |
56 | | ordtriexmidlem 4518 |
. . . . . . . . . . 11
     |
57 | 56 | ontrci 4427 |
. . . . . . . . . 10
     |
58 | | treq 4107 |
. . . . . . . . . 10
    
        |
59 | 57, 58 | mpbiri 168 |
. . . . . . . . 9
    
  |
60 | 55, 59 | jaoi 716 |
. . . . . . . 8
     

   
  |
61 | 51, 60 | syl 14 |
. . . . . . 7
   |
62 | 61 | rgen 2530 |
. . . . . 6

 |
63 | | dford3 4367 |
. . . . . 6
      |
64 | 49, 62, 63 | mpbir2an 942 |
. . . . 5
 |
65 | | prexg 4211 |
. . . . . . . 8
                
       |
66 | 40, 22, 65 | mp2an 426 |
. . . . . . 7
      
   
 |
67 | 2, 66 | eqeltri 2250 |
. . . . . 6
 |
68 | 67 | elon 4374 |
. . . . 5

  |
69 | 64, 68 | mpbir 146 |
. . . 4
 |
70 | | 2onn 6521 |
. . . . . 6
 |
71 | | nnfi 6871 |
. . . . . 6
   |
72 | 70, 71 | ax-mp 5 |
. . . . 5
 |
73 | | pm5.19 706 |
. . . . . . . . . 10
   |
74 | 13 | snm 3712 |
. . . . . . . . . . 11
    |
75 | | r19.3rmv 3513 |
. . . . . . . . . . 11
   
  
        |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . 10
  
       |
77 | 73, 76 | mtbi 670 |
. . . . . . . . 9

     |
78 | | rabbi 2654 |
. . . . . . . . 9
 
   
   
      |
79 | 77, 78 | mtbi 670 |
. . . . . . . 8
    
    |
80 | 79 | neir 2350 |
. . . . . . 7
         |
81 | | pr2ne 7190 |
. . . . . . . 8
                 
                |
82 | 40, 22, 81 | mp2an 426 |
. . . . . . 7
           
          |
83 | 80, 82 | mpbir 146 |
. . . . . 6
      
     |
84 | 2, 83 | eqbrtri 4024 |
. . . . 5
 |
85 | | enfii 6873 |
. . . . 5
  
  |
86 | 72, 84, 85 | mp2an 426 |
. . . 4
 |
87 | 69, 86 | elini 3319 |
. . 3
   |
88 | | eleq2 2241 |
. . 3
  

     |
89 | 87, 88 | mpbiri 168 |
. 2
  
  |
90 | | df1o2 6429 |
. . . . 5
   |
91 | | 1lt2o 6442 |
. . . . 5
 |
92 | 90, 91 | eqeltrri 2251 |
. . . 4
   |
93 | | nneneq 6856 |
. . . . . 6
       |
94 | 70, 93 | mpan2 425 |
. . . . 5
 
   |
95 | 84, 94 | mpbii 148 |
. . . 4
   |
96 | 92, 95 | eleqtrrid 2267 |
. . 3
     |
97 | | elpri 3615 |
. . . 4
  
      
          
  
      |
98 | 97, 2 | eleq2s 2272 |
. . 3
  
   
    
       |
99 | 96, 98 | syl 14 |
. 2
         
       |
100 | 13 | snid 3623 |
. . . . . . 7
   |
101 | | eleq2 2241 |
. . . . . . 7
  
    
 
       |
102 | 100, 101 | mpbii 148 |
. . . . . 6
  
          |
103 | | biidd 172 |
. . . . . . 7

    |
104 | 103 | elrab 2893 |
. . . . . 6
     
     |
105 | 102, 104 | sylib 122 |
. . . . 5
  
    
     |
106 | 105 | simprd 114 |
. . . 4
  
      |
107 | | eleq2 2241 |
. . . . . . 7
  
    
         |
108 | 100, 107 | mpbii 148 |
. . . . . 6
  
   
      |
109 | | biidd 172 |
. . . . . . 7

    |
110 | 109 | elrab 2893 |
. . . . . 6
     
     |
111 | 108, 110 | sylib 122 |
. . . . 5
  
    
     |
112 | 111 | simprd 114 |
. . . 4
  
      |
113 | 106, 112 | orim12i 759 |
. . 3
         
    
    |
114 | | df-dc 835 |
. . 3
DECID
    |
115 | 113, 114 | sylibr 134 |
. 2
         
    
DECID   |
116 | 89, 99, 115 | 3syl 17 |
1
  
DECID   |