Step | Hyp | Ref
| Expression |
1 | | eldif 3426 |
. . 3
    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)     |
2 | | rexr 9717 |
. . . . . . . . . 10
   |
3 | | rexr 9717 |
. . . . . . . . . 10
   |
4 | | elicc1 11714 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
     |
5 | 2, 3, 4 | syl2an 484 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif)  
    |
6 | 5 | adantr 471 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)  
    |
7 | 6 | notbid 300 |
. . . . . . 7
        ![[,] [,]](_icc.gif) 
     |
8 | | 3anass 995 |
. . . . . . . . 9
  
      |
9 | 8 | notbii 302 |
. . . . . . . 8
 

      |
10 | | ianor 495 |
. . . . . . . . 9
  
        |
11 | | rexr 9717 |
. . . . . . . . . . . 12
   |
12 | 11 | pm2.24d 139 |
. . . . . . . . . . 11
 
           |
13 | 12 | adantl 472 |
. . . . . . . . . 10
     

          |
14 | | ianor 495 |
. . . . . . . . . . 11
 
 
   |
15 | 11 | ad2antlr 738 |
. . . . . . . . . . . . . 14
      
  |
16 | | mnflt 11459 |
. . . . . . . . . . . . . . 15
   |
17 | 16 | ad2antlr 738 |
. . . . . . . . . . . . . 14
         |
18 | | simpr 467 |
. . . . . . . . . . . . . . . 16
       |
19 | | simpll 765 |
. . . . . . . . . . . . . . . 16
       |
20 | | ltnle 9744 |
. . . . . . . . . . . . . . . . 17
 
 
   |
21 | 20 | bicomd 206 |
. . . . . . . . . . . . . . . 16
 
     |
22 | 18, 19, 21 | syl2anc 671 |
. . . . . . . . . . . . . . 15
     
   |
23 | 22 | biimpa 491 |
. . . . . . . . . . . . . 14
         |
24 | | mnfxr 11448 |
. . . . . . . . . . . . . . 15
 |
25 | 2 | ad3antrrr 741 |
. . . . . . . . . . . . . . 15
      
  |
26 | | elioo1 11710 |
. . . . . . . . . . . . . . 15
     
     |
27 | 24, 25, 26 | sylancr 674 |
. . . . . . . . . . . . . 14
                |
28 | 15, 17, 23, 27 | mpbir3and 1197 |
. . . . . . . . . . . . 13
      
     |
29 | 28 | ex 440 |
. . . . . . . . . . . 12
     
      |
30 | | ltnle 9744 |
. . . . . . . . . . . . . 14
 
 
   |
31 | 30 | adantll 725 |
. . . . . . . . . . . . 13
     
   |
32 | 11 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
         |
33 | | simpr 467 |
. . . . . . . . . . . . . . 15
         |
34 | | ltpnf 11456 |
. . . . . . . . . . . . . . . 16
   |
35 | 34 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
         |
36 | 3 | ad3antlr 742 |
. . . . . . . . . . . . . . . 16
         |
37 | | pnfxr 11446 |
. . . . . . . . . . . . . . . 16
 |
38 | | elioo1 11710 |
. . . . . . . . . . . . . . . 16
      

    |
39 | 36, 37, 38 | sylancl 673 |
. . . . . . . . . . . . . . 15
          

    |
40 | 32, 33, 35, 39 | mpbir3and 1197 |
. . . . . . . . . . . . . 14
            |
41 | 40 | ex 440 |
. . . . . . . . . . . . 13
     
      |
42 | 31, 41 | sylbird 243 |
. . . . . . . . . . . 12
     
      |
43 | 29, 42 | orim12d 854 |
. . . . . . . . . . 11
      
            |
44 | 14, 43 | syl5bi 225 |
. . . . . . . . . 10
                   |
45 | 13, 44 | jaod 386 |
. . . . . . . . 9
       
 

          |
46 | 10, 45 | syl5bi 225 |
. . . . . . . 8
                     |
47 | 9, 46 | syl5bi 225 |
. . . . . . 7
                   |
48 | 7, 47 | sylbid 223 |
. . . . . 6
        ![[,] [,]](_icc.gif) 

          |
49 | 48 | expimpd 612 |
. . . . 5
 
     ![[,] [,]](_icc.gif)              |
50 | | elun 3586 |
. . . . 5
                   |
51 | 49, 50 | syl6ibr 235 |
. . . 4
 
     ![[,] [,]](_icc.gif)              |
52 | | ioossre 11730 |
. . . . . . . . 9
    |
53 | | ioossre 11730 |
. . . . . . . . 9
    |
54 | 52, 53 | unssi 3621 |
. . . . . . . 8
         |
55 | 54 | sseli 3440 |
. . . . . . 7
           |
56 | 55 | adantl 472 |
. . . . . 6
            
  |
57 | | elioo2 11711 |
. . . . . . . . . . . . . . . 16
     
     |
58 | 24, 2, 57 | sylancr 674 |
. . . . . . . . . . . . . . 15
    
     |
59 | 58 | adantr 471 |
. . . . . . . . . . . . . 14
 
          |
60 | 20 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
 
     |
61 | 60 | ex 440 |
. . . . . . . . . . . . . . . . . 18
 

    |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . 17



     |
63 | 62 | com13 83 |
. . . . . . . . . . . . . . . 16
 

     |
64 | 63 | adantr 471 |
. . . . . . . . . . . . . . 15
 
        |
65 | 64 | 3impd 1231 |
. . . . . . . . . . . . . 14
 
   
   |
66 | 59, 65 | sylbid 223 |
. . . . . . . . . . . . 13
 
    
   |
67 | 3 | adantl 472 |
. . . . . . . . . . . . . . 15
 
   |
68 | 67, 37, 38 | sylancl 673 |
. . . . . . . . . . . . . 14
 
          |
69 | | xrltnle 9732 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   |
70 | 69 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . 21
       |
71 | 70 | ex 440 |
. . . . . . . . . . . . . . . . . . . 20


     |
72 | 71 | com3l 84 |
. . . . . . . . . . . . . . . . . . 19

 
    |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . 18


 
     |
74 | 73 | com14 91 |
. . . . . . . . . . . . . . . . 17


 
     |
75 | 3, 74 | syl 17 |
. . . . . . . . . . . . . . . 16
         |
76 | 75 | adantl 472 |
. . . . . . . . . . . . . . 15
 
         |
77 | 76 | 3impd 1231 |
. . . . . . . . . . . . . 14
 
  

   |
78 | 68, 77 | sylbid 223 |
. . . . . . . . . . . . 13
 
        |
79 | 66, 78 | orim12d 854 |
. . . . . . . . . . . 12
 
          
    |
80 | 50, 79 | syl5bi 225 |
. . . . . . . . . . 11
 
               |
81 | 80 | imp 435 |
. . . . . . . . . 10
            
    |
82 | 81, 14 | sylibr 217 |
. . . . . . . . 9
            
    |
83 | 82 | intnand 932 |
. . . . . . . 8
            
      |
84 | 83, 8 | sylnibr 311 |
. . . . . . 7
            
    |
85 | 2, 3 | anim12i 574 |
. . . . . . . . 9
 
     |
86 | 85 | adantr 471 |
. . . . . . . 8
            
    |
87 | 4 | notbid 300 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif) 
     |
88 | 86, 87 | syl 17 |
. . . . . . 7
            

  ![[,] [,]](_icc.gif) 
     |
89 | 84, 88 | mpbird 240 |
. . . . . 6
            
  ![[,] [,]](_icc.gif)    |
90 | 56, 89 | jca 539 |
. . . . 5
            
   ![[,] [,]](_icc.gif)     |
91 | 90 | ex 440 |
. . . 4
 
             ![[,] [,]](_icc.gif)      |
92 | 51, 91 | impbid 195 |
. . 3
 
     ![[,] [,]](_icc.gif)  
           |
93 | 1, 92 | syl5bb 265 |
. 2
 
     ![[,] [,]](_icc.gif)              |
94 | 93 | eqrdv 2460 |
1
 
    ![[,] [,]](_icc.gif)             |