Step | Hyp | Ref
| Expression |
1 | | simplr 770 |
. . . 4
      
  |
2 | | eqid 2471 |
. . . . . 6
         |
3 | | eqid 2471 |
. . . . . 6
     |
4 | | eqid 2471 |
. . . . . 6
         |
5 | | lvolnle3at.v |
. . . . . 6
     |
6 | 2, 3, 4, 5 | islvol 33209 |
. . . . 5
 
    
              |
7 | 6 | ad2antrr 740 |
. . . 4
             
             |
8 | 1, 7 | mpbid 215 |
. . 3
                         |
9 | 8 | simprd 470 |
. 2
       
           |
10 | | oveq1 6315 |
. . . . . . . . 9
       |
11 | 10 | oveq1d 6323 |
. . . . . . . 8
   
       |
12 | 11 | breq2d 4407 |
. . . . . . 7
     
       |
13 | 12 | notbid 301 |
. . . . . 6
 
   
       |
14 | | simp1l 1054 |
. . . . . . . . . . . 12
                
  |
15 | | simp3l 1058 |
. . . . . . . . . . . 12
                       |
16 | | simp21 1063 |
. . . . . . . . . . . 12
                
  |
17 | | simp22 1064 |
. . . . . . . . . . . 12
                
  |
18 | | lvolnle3at.l |
. . . . . . . . . . . . 13
     |
19 | | lvolnle3at.j |
. . . . . . . . . . . . 13
     |
20 | | lvolnle3at.a |
. . . . . . . . . . . . 13
     |
21 | 18, 19, 20, 4 | lplnnle2at 33177 |
. . . . . . . . . . . 12
      
 
    |
22 | 14, 15, 16, 17, 21 | syl13anc 1294 |
. . . . . . . . . . 11
                
    |
23 | 2, 4 | lplnbase 33170 |
. . . . . . . . . . . . . . 15
    
      |
24 | 15, 23 | syl 17 |
. . . . . . . . . . . . . 14
                       |
25 | | simp1r 1055 |
. . . . . . . . . . . . . . 15
                
  |
26 | 2, 5 | lvolbase 33214 |
. . . . . . . . . . . . . . 15
       |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
                
      |
28 | | simp3r 1059 |
. . . . . . . . . . . . . 14
                       |
29 | | eqid 2471 |
. . . . . . . . . . . . . . 15
         |
30 | 2, 29, 3 | cvrlt 32907 |
. . . . . . . . . . . . . 14
                         |
31 | 14, 24, 27, 28, 30 | syl31anc 1295 |
. . . . . . . . . . . . 13
                         |
32 | | hlpos 33002 |
. . . . . . . . . . . . . . 15
   |
33 | 14, 32 | syl 17 |
. . . . . . . . . . . . . 14
                
  |
34 | 2, 19, 20 | hlatjcl 33003 |
. . . . . . . . . . . . . . 15
 
         |
35 | 14, 16, 17, 34 | syl3anc 1292 |
. . . . . . . . . . . . . 14
                         |
36 | 2, 18, 29 | pltletr 16295 |
. . . . . . . . . . . . . 14
          
                              |
37 | 33, 24, 27, 35, 36 | syl13anc 1294 |
. . . . . . . . . . . . 13
                           
           |
38 | 31, 37 | mpand 689 |
. . . . . . . . . . . 12
                               |
39 | 18, 29 | pltle 16285 |
. . . . . . . . . . . . 13
 
                         |
40 | 14, 15, 35, 39 | syl3anc 1292 |
. . . . . . . . . . . 12
                               |
41 | 38, 40 | syld 44 |
. . . . . . . . . . 11
                         |
42 | 22, 41 | mtod 182 |
. . . . . . . . . 10
                
    |
43 | 42 | adantr 472 |
. . . . . . . . 9
     
            
        |
44 | | simprr 774 |
. . . . . . . . . . 11
     
            
        |
45 | | hllat 33000 |
. . . . . . . . . . . . . 14
   |
46 | 14, 45 | syl 17 |
. . . . . . . . . . . . 13
                
  |
47 | | simp23 1065 |
. . . . . . . . . . . . . 14
                
  |
48 | 2, 20 | atbase 32926 |
. . . . . . . . . . . . . 14
       |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . 13
                
      |
50 | 2, 18, 19 | latleeqj2 16388 |
. . . . . . . . . . . . 13
 
                       |
51 | 46, 49, 35, 50 | syl3anc 1292 |
. . . . . . . . . . . 12
                   
         |
52 | 51 | adantr 472 |
. . . . . . . . . . 11
     
            
                |
53 | 44, 52 | mpbid 215 |
. . . . . . . . . 10
     
            
      
     |
54 | 53 | breq2d 4407 |
. . . . . . . . 9
     
            
        
     |
55 | 43, 54 | mtbird 308 |
. . . . . . . 8
     
            
          |
56 | 55 | anassrs 660 |
. . . . . . 7
      
            
  
      |
57 | | simpl1l 1081 |
. . . . . . . . . 10
     
            
   
  |
58 | | simpl3l 1085 |
. . . . . . . . . 10
     
            
          |
59 | | simpl2 1034 |
. . . . . . . . . . 11
     
            
    
   |
60 | | simpr 468 |
. . . . . . . . . . 11
     
            
          |
61 | 18, 19, 20, 4 | lplni2 33173 |
. . . . . . . . . . 11
  

               |
62 | 57, 59, 60, 61 | syl3anc 1292 |
. . . . . . . . . 10
     
            
              |
63 | 29, 4 | lplnnlt 33201 |
. . . . . . . . . 10
 
      
     
            |
64 | 57, 58, 62, 63 | syl3anc 1292 |
. . . . . . . . 9
     
            
                |
65 | 2, 19 | latjcl 16375 |
. . . . . . . . . . . . 13
  
    
    
          |
66 | 46, 35, 49, 65 | syl3anc 1292 |
. . . . . . . . . . . 12
                           |
67 | 2, 18, 29 | pltletr 16295 |
. . . . . . . . . . . 12
          
                      
        
    |
68 | 33, 24, 27, 66, 67 | syl13anc 1294 |
. . . . . . . . . . 11
                           
 
        
    |
69 | 31, 68 | mpand 689 |
. . . . . . . . . 10
                                   |
70 | 69 | adantr 472 |
. . . . . . . . 9
     
            
                      |
71 | 64, 70 | mtod 182 |
. . . . . . . 8
     
            
   
      |
72 | 71 | anassrs 660 |
. . . . . . 7
      
            
         |
73 | 56, 72 | pm2.61dan 808 |
. . . . . 6
     
            
      |
74 | | eqid 2471 |
. . . . . . . . . 10
         |
75 | 74, 19, 20, 4 | lplnnle2at 33177 |
. . . . . . . . 9
      
 
          |
76 | 14, 15, 17, 47, 75 | syl13anc 1294 |
. . . . . . . 8
                           |
77 | 2, 19, 20 | hlatjcl 33003 |
. . . . . . . . . . . 12
 
         |
78 | 14, 17, 47, 77 | syl3anc 1292 |
. . . . . . . . . . 11
                         |
79 | 2, 18, 29 | pltletr 16295 |
. . . . . . . . . . 11
          
                              |
80 | 33, 24, 27, 78, 79 | syl13anc 1294 |
. . . . . . . . . 10
                           
           |
81 | 31, 80 | mpand 689 |
. . . . . . . . 9
                               |
82 | 74, 29 | pltle 16285 |
. . . . . . . . . 10
 
                               |
83 | 14, 15, 78, 82 | syl3anc 1292 |
. . . . . . . . 9
                                     |
84 | 81, 83 | syld 44 |
. . . . . . . 8
                               |
85 | 76, 84 | mtod 182 |
. . . . . . 7
                
    |
86 | 19, 20 | hlatjidm 33005 |
. . . . . . . . . 10
 
     |
87 | 14, 17, 86 | syl2anc 673 |
. . . . . . . . 9
                     |
88 | 87 | oveq1d 6323 |
. . . . . . . 8
                         |
89 | 88 | breq2d 4407 |
. . . . . . 7
                     
     |
90 | 85, 89 | mtbird 308 |
. . . . . 6
                
      |
91 | 13, 73, 90 | pm2.61ne 2728 |
. . . . 5
                
      |
92 | 91 | 3expia 1233 |
. . . 4
                 
       |
93 | 92 | expd 443 |
. . 3
                
        |
94 | 93 | rexlimdv 2870 |
. 2
                         |
95 | 9, 94 | mpd 15 |
1
      
      |