Step | Hyp | Ref
| Expression |
1 | | 0nn0 10891 |
. . . . . 6
 |
2 | 1 | a1i 11 |
. . . . 5

  |
3 | | breq1 4408 |
. . . . . . . 8
 
   |
4 | 3 | imbi1d 319 |
. . . . . . 7
         |
5 | 4 | ralbidv 2829 |
. . . . . 6
  
  
     |
6 | 5 | adantl 468 |
. . . . 5
     

 
    |
7 | | nnel 2735 |
. . . . . . . . 9

  |
8 | | n0i 3738 |
. . . . . . . . 9

  |
9 | 7, 8 | sylbi 199 |
. . . . . . . 8

  |
10 | 9 | con4i 134 |
. . . . . . 7

  |
11 | 10 | a1d 26 |
. . . . . 6

    |
12 | 11 | ralrimivw 2805 |
. . . . 5

 
   |
13 | 2, 6, 12 | rspcedvd 3157 |
. . . 4

  
   |
14 | 13 | 2a1d 27 |
. . 3


   
     |
15 | | ltso 9719 |
. . . . . . 7
 |
16 | | id 22 |
. . . . . . . . 9

  |
17 | | nn0ssre 10880 |
. . . . . . . . 9
 |
18 | 16, 17 | syl6ss 3446 |
. . . . . . . 8

  |
19 | 18 | 3anim3i 1197 |
. . . . . . 7
  
    |
20 | | fisup2g 7989 |
. . . . . . 7
 
  
 
 
     |
21 | 15, 19, 20 | sylancr 670 |
. . . . . 6
  

 


     |
22 | | simp3 1011 |
. . . . . . 7
  
  |
23 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
24 | 23 | notbid 296 |
. . . . . . . . . . . . . . . . . . 19
 
   |
25 | 24 | rspcva 3150 |
. . . . . . . . . . . . . . . . . 18
   
  |
26 | 25 | 2a1d 27 |
. . . . . . . . . . . . . . . . 17
              |
27 | 26 | expcom 437 |
. . . . . . . . . . . . . . . 16
 
            |
28 | 27 | com24 90 |
. . . . . . . . . . . . . . 15
 
  




     |
29 | 28 | imp31 434 |
. . . . . . . . . . . . . 14
   
 
  
     |
30 | 7, 29 | syl5bi 221 |
. . . . . . . . . . . . 13
   
 
  
 
   |
31 | 30 | con4d 109 |
. . . . . . . . . . . 12
   
 
  
     |
32 | 31 | ralrimiva 2804 |
. . . . . . . . . . 11
  
 

   
   |
33 | 32 | ex 436 |
. . . . . . . . . 10
 
  


 
    |
34 | 33 | adantr 467 |
. . . . . . . . 9
  
 
         
    |
35 | 34 | com12 32 |
. . . . . . . 8
       
 

   
    |
36 | 35 | reximdva 2864 |
. . . . . . 7
  
 
 
 
    
     |
37 | | ssrexv 3496 |
. . . . . . 7

  
    
    |
38 | 22, 36, 37 | sylsyld 58 |
. . . . . 6
  
 
 
 
     
    |
39 | 21, 38 | mpd 15 |
. . . . 5
  
  
   |
40 | 39 | 3exp 1208 |
. . . 4
 
   
     |
41 | 40 | com3l 84 |
. . 3

    
     |
42 | 14, 41 | pm2.61ine 2709 |
. 2

   
    |
43 | | fzfi 12192 |
. . . . 5
     |
44 | | elfz2nn0 11892 |
. . . . . . . . . . 11
    

   |
45 | 44 | notbii 298 |
. . . . . . . . . 10
    

   |
46 | | 3ianor 1003 |
. . . . . . . . . 10
  

   |
47 | | 3orass 989 |
. . . . . . . . . 10
    
    |
48 | 45, 46, 47 | 3bitri 275 |
. . . . . . . . 9
    


    |
49 | | ssel 3428 |
. . . . . . . . . . . . 13

    |
50 | 49 | adantr 467 |
. . . . . . . . . . . 12
 
     |
51 | 50 | adantr 467 |
. . . . . . . . . . 11
  
  
  
   |
52 | 51 | con3rr3 142 |
. . . . . . . . . 10
      
 
   |
53 | | notnot 293 |
. . . . . . . . . . . 12

  |
54 | | pm2.24 113 |
. . . . . . . . . . . . . . . . 17

    |
55 | 54 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
 
   |
56 | 55 | adantr 467 |
. . . . . . . . . . . . . . 15
  
  
  
   |
57 | 56 | com12 32 |
. . . . . . . . . . . . . 14
      
 
   |
58 | 57 | a1d 26 |
. . . . . . . . . . . . 13
       
 
    |
59 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
60 | | neleq1 2731 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
61 | 59, 60 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . 19
         |
62 | 61 | rspcva 3150 |
. . . . . . . . . . . . . . . . . 18
   
  
   |
63 | | nn0re 10885 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
64 | | nn0re 10885 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
65 | | ltnle 9718 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 
   |
66 | 63, 64, 65 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 
   |
67 | | df-nel 2627 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
69 | 66, 68 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  


    |
70 | 69 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
 
    |
71 | 70 | ex 436 |
. . . . . . . . . . . . . . . . . . . . 21


 
 
     |
72 | 71 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
     
     |
73 | 72 | com12 32 |
. . . . . . . . . . . . . . . . . . 19

 
    
     |
74 | 73 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
   
    
     |
75 | 62, 74 | mpid 42 |
. . . . . . . . . . . . . . . . 17
   
   
 
    |
76 | 75 | ex 436 |
. . . . . . . . . . . . . . . 16

 
   
 
     |
77 | 76 | com13 83 |
. . . . . . . . . . . . . . 15
 
  
   
     |
78 | 77 | imp 431 |
. . . . . . . . . . . . . 14
  
  
   
    |
79 | 78 | com13 83 |
. . . . . . . . . . . . 13

      
 
    |
80 | 58, 79 | jaoi 381 |
. . . . . . . . . . . 12
  

  
  
 
    |
81 | 53, 80 | syl5bir 222 |
. . . . . . . . . . 11
  

  
 
  
    |
82 | 81 | impcom 432 |
. . . . . . . . . 10
 

    
 
  
   |
83 | 52, 82 | jaoi3 982 |
. . . . . . . . 9
  
    
 
  
   |
84 | 48, 83 | sylbi 199 |
. . . . . . . 8
       
 
  
   |
85 | 84 | com12 32 |
. . . . . . 7
  
  
      
   |
86 | 85 | con4d 109 |
. . . . . 6
  
  
  
       |
87 | 86 | ssrdv 3440 |
. . . . 5
  
  
        |
88 | | ssfi 7797 |
. . . . 5
          
  |
89 | 43, 87, 88 | sylancr 670 |
. . . 4
  
  
    |
90 | 89 | ex 436 |
. . 3
 
  
     |
91 | 90 | rexlimdva 2881 |
. 2

   
    |
92 | 42, 91 | impbid 194 |
1


  
    |