Proof of Theorem hashge2el2dif
Step | Hyp | Ref
| Expression |
1 | | fveq2 5863 |
. . . . . . 7
               |
2 | | hashsng 12546 |
. . . . . . 7
         |
3 | 1, 2 | sylan9eqr 2506 |
. . . . . 6
 
         |
4 | 3 | ralimiaa 2779 |
. . . . 5
 
         |
5 | | 0re 9640 |
. . . . . . . . . . . . . . . 16
 |
6 | | 1re 9639 |
. . . . . . . . . . . . . . . 16
 |
7 | 5, 6 | readdcli 9653 |
. . . . . . . . . . . . . . 15
   |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
  
          |
9 | | 2re 10676 |
. . . . . . . . . . . . . . 15
 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
  
        |
11 | | hashcl 12535 |
. . . . . . . . . . . . . . . 16
       |
12 | 11 | nn0red 10923 |
. . . . . . . . . . . . . . 15
       |
13 | 12 | adantr 467 |
. . . . . . . . . . . . . 14
  
            |
14 | 8, 10, 13 | 3jca 1187 |
. . . . . . . . . . . . 13
  
                |
15 | | 0p1e1 10718 |
. . . . . . . . . . . . . . . . 17
   |
16 | | 1lt2 10773 |
. . . . . . . . . . . . . . . . 17
 |
17 | 15, 16 | eqbrtri 4421 |
. . . . . . . . . . . . . . . 16
   |
18 | 17 | jctl 544 |
. . . . . . . . . . . . . . 15
    
          |
19 | 18 | adantl 468 |
. . . . . . . . . . . . . 14
         
       |
20 | 19 | adantl 468 |
. . . . . . . . . . . . 13
  
                |
21 | | ltleletr 9723 |
. . . . . . . . . . . . 13
   
        
      
       |
22 | 14, 20, 21 | sylc 62 |
. . . . . . . . . . . 12
  
              |
23 | 11 | nn0zd 11035 |
. . . . . . . . . . . . . . 15
       |
24 | | 0z 10945 |
. . . . . . . . . . . . . . 15
 |
25 | 23, 24 | jctil 540 |
. . . . . . . . . . . . . 14
         |
26 | 25 | adantr 467 |
. . . . . . . . . . . . 13
  
              |
27 | | zltp1le 10983 |
. . . . . . . . . . . . 13
           
         |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
  
            
       |
29 | 22, 28 | mpbird 236 |
. . . . . . . . . . 11
  
            |
30 | | 0ltpnf 11421 |
. . . . . . . . . . . 12
 |
31 | | simpl 459 |
. . . . . . . . . . . . . . 15
         |
32 | 31 | anim2i 572 |
. . . . . . . . . . . . . 14
  
          |
33 | 32 | ancomd 453 |
. . . . . . . . . . . . 13
  
          |
34 | | hashinf 12517 |
. . . . . . . . . . . . 13
 
       |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
  
            |
36 | 30, 35 | syl5breqr 4438 |
. . . . . . . . . . 11
  
            |
37 | 29, 36 | pm2.61ian 798 |
. . . . . . . . . 10
             |
38 | | hashgt0n0 12543 |
. . . . . . . . . 10
         |
39 | 37, 38 | syldan 473 |
. . . . . . . . 9
         |
40 | | rspn0 3743 |
. . . . . . . . 9

 
   
       |
41 | 39, 40 | syl 17 |
. . . . . . . 8
        
           |
42 | 41 | imp 431 |
. . . . . . 7
  
                 |
43 | | breq2 4405 |
. . . . . . . . . . 11
     
       |
44 | 6, 9 | ltnlei 9752 |
. . . . . . . . . . . . 13

  |
45 | | pm2.21 112 |
. . . . . . . . . . . . 13



     |
46 | 44, 45 | sylbi 199 |
. . . . . . . . . . . 12
 

     |
47 | 16, 46 | ax-mp 5 |
. . . . . . . . . . 11
      |
48 | 43, 47 | syl6bi 232 |
. . . . . . . . . 10
     
   

     |
49 | 48 | com12 32 |
. . . . . . . . 9
    
    

     |
50 | 49 | adantl 468 |
. . . . . . . 8
                  |
51 | 50 | adantr 467 |
. . . . . . 7
  
                
     |
52 | 42, 51 | mpd 15 |
. . . . . 6
  
           
    |
53 | 52 | expcom 437 |
. . . . 5
 
   
 
           |
54 | 4, 53 | syl 17 |
. . . 4
 
   
     
     |
55 | | ax-1 6 |
. . . 4
 
               |
56 | 54, 55 | pm2.61i 168 |
. . 3
            |
57 | | eqsn 4132 |
. . . . . 6

  

   |
58 | 39, 57 | syl 17 |
. . . . 5
       
  
   |
59 | | equcom 1861 |
. . . . . . 7

  |
60 | 59 | a1i 11 |
. . . . . 6
       
   |
61 | 60 | ralbidv 2826 |
. . . . 5
        

   |
62 | 58, 61 | bitrd 257 |
. . . 4
       
  
   |
63 | 62 | ralbidv 2826 |
. . 3
        
   
   |
64 | 56, 63 | mtbid 302 |
. 2
        
  |
65 | | df-ne 2623 |
. . . . . 6

  |
66 | 65 | rexbii 2888 |
. . . . 5
 

  |
67 | | rexnal 2835 |
. . . . 5
 

  |
68 | 66, 67 | bitri 253 |
. . . 4
 

  |
69 | 68 | rexbii 2888 |
. . 3
  
 
  |
70 | | rexnal 2835 |
. . 3
  


  |
71 | 69, 70 | bitri 253 |
. 2
  


  |
72 | 64, 71 | sylibr 216 |
1
       

  |