Step | Hyp | Ref
| Expression |
1 | | hlatl 32938 |
. . . . 5
   |
2 | 1 | adantr 467 |
. . . 4
  
    |
3 | | simpr1 1015 |
. . . 4
  
    |
4 | | cvrat.b |
. . . . . 6
     |
5 | | eqid 2453 |
. . . . . 6
         |
6 | | cvrat.z |
. . . . . 6
     |
7 | | cvrat.a |
. . . . . 6
     |
8 | 4, 5, 6, 7 | atlex 32894 |
. . . . 5
 

        |
9 | 8 | 3expia 1211 |
. . . 4
    
         |
10 | 2, 3, 9 | syl2anc 667 |
. . 3
  
   
         |
11 | 1 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . 17
  

   |
12 | | simp22 1043 |
. . . . . . . . . . . . . . . . 17
  

   |
13 | | simp3 1011 |
. . . . . . . . . . . . . . . . 17
  

   |
14 | 5, 7 | atcmp 32889 |
. . . . . . . . . . . . . . . . 17
 
       
   |
15 | 11, 12, 13, 14 | syl3anc 1269 |
. . . . . . . . . . . . . . . 16
  

       
   |
16 | | breq1 4408 |
. . . . . . . . . . . . . . . . 17
       
         |
17 | 16 | biimprd 227 |
. . . . . . . . . . . . . . . 16
                 |
18 | 15, 17 | syl6bi 232 |
. . . . . . . . . . . . . . 15
  

                         |
19 | 18 | com23 81 |
. . . . . . . . . . . . . 14
  

                         |
20 | | con3 140 |
. . . . . . . . . . . . . 14
                               |
21 | 19, 20 | syl6 34 |
. . . . . . . . . . . . 13
  

              
          |
22 | 21 | impd 433 |
. . . . . . . . . . . 12
  

                         |
23 | | simp1 1009 |
. . . . . . . . . . . . 13
  

   |
24 | 4, 7 | atbase 32867 |
. . . . . . . . . . . . . 14
   |
25 | 24 | 3ad2ant3 1032 |
. . . . . . . . . . . . 13
  

   |
26 | | cvrat.j |
. . . . . . . . . . . . . 14
     |
27 | | eqid 2453 |
. . . . . . . . . . . . . 14
     |
28 | 4, 5, 26, 27, 7 | cvr1 32987 |
. . . . . . . . . . . . 13
 
                 |
29 | 23, 25, 12, 28 | syl3anc 1269 |
. . . . . . . . . . . 12
  

       
         |
30 | 22, 29 | sylibd 218 |
. . . . . . . . . . 11
  

                         |
31 | 30 | imp 431 |
. . . . . . . . . 10
   

               
        |
32 | | hllat 32941 |
. . . . . . . . . . . . 13
   |
33 | 32 | 3ad2ant1 1030 |
. . . . . . . . . . . 12
  

   |
34 | 4, 7 | atbase 32867 |
. . . . . . . . . . . . 13
   |
35 | 12, 34 | syl 17 |
. . . . . . . . . . . 12
  

   |
36 | 4, 26 | latjcom 16317 |
. . . . . . . . . . . 12
 
       |
37 | 33, 35, 25, 36 | syl3anc 1269 |
. . . . . . . . . . 11
  

       |
38 | 37 | adantr 467 |
. . . . . . . . . 10
   

               
      |
39 | 31, 38 | breqtrrd 4432 |
. . . . . . . . 9
   

               
        |
40 | 39 | adantrrl 731 |
. . . . . . . 8
   

        
                   |
41 | 5, 26, 7 | hlatlej1 32952 |
. . . . . . . . . . . . 13
 
           |
42 | 23, 12, 13, 41 | syl3anc 1269 |
. . . . . . . . . . . 12
  

           |
43 | 42 | adantr 467 |
. . . . . . . . . . 11
   

        
                     |
44 | 5, 7 | atcmp 32889 |
. . . . . . . . . . . . . . . . . 18
 
       
   |
45 | 11, 13, 12, 44 | syl3anc 1269 |
. . . . . . . . . . . . . . . . 17
  

       
   |
46 | | breq1 4408 |
. . . . . . . . . . . . . . . . . 18
       
         |
47 | 46 | biimpd 211 |
. . . . . . . . . . . . . . . . 17
                 |
48 | 45, 47 | syl6bi 232 |
. . . . . . . . . . . . . . . 16
  

                         |
49 | 48 | com23 81 |
. . . . . . . . . . . . . . 15
  

                         |
50 | | con3 140 |
. . . . . . . . . . . . . . 15
                               |
51 | 49, 50 | syl6 34 |
. . . . . . . . . . . . . 14
  

              
          |
52 | 51 | imp32 435 |
. . . . . . . . . . . . 13
   

               
        |
53 | 52 | adantrrl 731 |
. . . . . . . . . . . 12
   

        
                   |
54 | | simprl 765 |
. . . . . . . . . . . . . 14
   

                    |
55 | | simp21 1042 |
. . . . . . . . . . . . . . . . 17
  

   |
56 | | simp23 1044 |
. . . . . . . . . . . . . . . . . . 19
  

   |
57 | 4, 7 | atbase 32867 |
. . . . . . . . . . . . . . . . . . 19
   |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  

   |
59 | 4, 26 | latjcl 16309 |
. . . . . . . . . . . . . . . . . 18
 
     |
60 | 33, 35, 58, 59 | syl3anc 1269 |
. . . . . . . . . . . . . . . . 17
  

     |
61 | 23, 55, 60 | 3jca 1189 |
. . . . . . . . . . . . . . . 16
  

 
     |
62 | | cvrat.s |
. . . . . . . . . . . . . . . . . 18
     |
63 | 5, 62 | pltle 16219 |
. . . . . . . . . . . . . . . . 17
 

                |
64 | 63 | imp 431 |
. . . . . . . . . . . . . . . 16
   
               |
65 | 61, 64 | sylan 474 |
. . . . . . . . . . . . . . 15
   

              |
66 | 65 | adantrl 723 |
. . . . . . . . . . . . . 14
   

                      |
67 | | hlpos 32943 |
. . . . . . . . . . . . . . . . 17
   |
68 | 67 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . 16
  

   |
69 | 4, 5 | postr 16211 |
. . . . . . . . . . . . . . . 16
  

                               |
70 | 68, 25, 55, 60, 69 | syl13anc 1271 |
. . . . . . . . . . . . . . 15
  

                 
           |
71 | 70 | adantr 467 |
. . . . . . . . . . . . . 14
   

                                        |
72 | 54, 66, 71 | mp2and 686 |
. . . . . . . . . . . . 13
   

                      |
73 | 72 | adantrrr 732 |
. . . . . . . . . . . 12
   

        
                     |
74 | 4, 5, 26, 7 | hlexch1 32959 |
. . . . . . . . . . . . . . . 16
  

                           |
75 | 74 | 3expia 1211 |
. . . . . . . . . . . . . . 15
  
                              |
76 | 75 | impd 433 |
. . . . . . . . . . . . . 14
  
                              |
77 | 23, 13, 56, 35, 76 | syl13anc 1271 |
. . . . . . . . . . . . 13
  

                             |
78 | 77 | adantr 467 |
. . . . . . . . . . . 12
   

        
                                       |
79 | 53, 73, 78 | mp2and 686 |
. . . . . . . . . . 11
   

        
                     |
80 | 4, 26 | latjcl 16309 |
. . . . . . . . . . . . . 14
 
     |
81 | 33, 35, 25, 80 | syl3anc 1269 |
. . . . . . . . . . . . 13
  

     |
82 | 4, 5, 26 | latjle12 16320 |
. . . . . . . . . . . . 13
  
   
                                |
83 | 33, 35, 58, 81, 82 | syl13anc 1271 |
. . . . . . . . . . . 12
  

                                 |
84 | 83 | adantr 467 |
. . . . . . . . . . 11
   

        
                                           |
85 | 43, 79, 84 | mpbi2and 933 |
. . . . . . . . . 10
   

        
                       |
86 | 5, 26, 7 | hlatlej1 32952 |
. . . . . . . . . . . . 13
 
           |
87 | 23, 12, 56, 86 | syl3anc 1269 |
. . . . . . . . . . . 12
  

           |
88 | 87 | adantr 467 |
. . . . . . . . . . 11
   

        
                     |
89 | 4, 5, 26 | latjle12 16320 |
. . . . . . . . . . . . 13
  
   
                                |
90 | 33, 35, 25, 60, 89 | syl13anc 1271 |
. . . . . . . . . . . 12
  

                                 |
91 | 90 | adantr 467 |
. . . . . . . . . . 11
   

        
                                           |
92 | 88, 73, 91 | mpbi2and 933 |
. . . . . . . . . 10
   

        
                       |
93 | 33, 60, 81 | 3jca 1189 |
. . . . . . . . . . . 12
  

 
       |
94 | 93 | adantr 467 |
. . . . . . . . . . 11
   

        
           
       |
95 | 4, 5 | latasymb 16312 |
. . . . . . . . . . 11
  
                
         
       |
96 | 94, 95 | syl 17 |
. . . . . . . . . 10
   

        
                       
         
       |
97 | 85, 92, 96 | mpbi2and 933 |
. . . . . . . . 9
   

        
                 |
98 | | breq2 4409 |
. . . . . . . . . . . 12
       
     |
99 | 98 | biimpcd 228 |
. . . . . . . . . . 11
  
    
     |
100 | 99 | adantr 467 |
. . . . . . . . . 10
 
             
     |
101 | 100 | ad2antll 736 |
. . . . . . . . 9
   

        
                     |
102 | 97, 101 | mpd 15 |
. . . . . . . 8
   

        
               |
103 | 4, 5, 62, 27 | cvrnbtwn3 32854 |
. . . . . . . . . . . . . . 15
   
                       |
104 | 103 | biimpd 211 |
. . . . . . . . . . . . . 14
   
                       |
105 | 104 | 3expia 1211 |
. . . . . . . . . . . . 13
   
                    
    |
106 | 68, 25, 81, 55, 105 | syl13anc 1271 |
. . . . . . . . . . . 12
  

                       |
107 | 106 | exp4a 611 |
. . . . . . . . . . 11
  

                       |
108 | 107 | com23 81 |
. . . . . . . . . 10
  

                       |
109 | 108 | imp4b 595 |
. . . . . . . . 9
   

                      |
110 | 109 | adantrr 724 |
. . . . . . . 8
   

        
                         |
111 | 40, 102, 110 | mp2and 686 |
. . . . . . 7
   

        
             |
112 | | simpl3 1014 |
. . . . . . 7
   

        
             |
113 | 111, 112 | eqeltrrd 2532 |
. . . . . 6
   

        
             |
114 | 113 | exp45 619 |
. . . . 5
  

                 
     |
115 | 114 | 3expa 1209 |
. . . 4
   
                   
     |
116 | 115 | rexlimdva 2881 |
. . 3
  
   
               
     |
117 | 10, 116 | syld 45 |
. 2
  
     
      
     |
118 | 117 | imp32 435 |
1
   
             
   |