Proof of Theorem cdlemk12
Step | Hyp | Ref
| Expression |
1 | | simp11l 1120 |
. 2
    
  


                                           
  |
2 | | simp22l 1128 |
. 2
    
  


                                           
  |
3 | | simp11 1039 |
. . 3
    
  


                                                |
4 | | simp13 1041 |
. . 3
    
  


                                           
  |
5 | | cdlemk.l |
. . . 4
     |
6 | | cdlemk.a |
. . . 4
     |
7 | | cdlemk.h |
. . . 4
     |
8 | | cdlemk.t |
. . . 4
         |
9 | 5, 6, 7, 8 | ltrnat 33717 |
. . 3
   

      |
10 | 3, 4, 2, 9 | syl3anc 1269 |
. 2
    
  


                                                  |
11 | | simp12 1040 |
. . . 4
    
  


                                           
  |
12 | | simp21r 1127 |
. . . 4
    
  


                                           
  |
13 | 3, 11, 12 | 3jca 1189 |
. . 3
    
  


                                              
   |
14 | | simp21l 1126 |
. . . 4
    
  


                                           
  |
15 | | simp22 1043 |
. . . 4
    
  


                                                |
16 | | simp23 1044 |
. . . 4
    
  


                                                      |
17 | 14, 15, 16 | 3jca 1189 |
. . 3
    
  


                                                          |
18 | | simp311 1156 |
. . 3
    
  


                                               |
19 | | simp313 1158 |
. . 3
    
  


                                               |
20 | | simp32r 1135 |
. . 3
    
  


                                                      |
21 | | cdlemk.b |
. . . 4
     |
22 | | cdlemk.j |
. . . 4
     |
23 | | cdlemk.r |
. . . 4
         |
24 | | cdlemk.m |
. . . 4
     |
25 | | cdlemk.s |
. . . 4
                               |
26 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 34425 |
. . 3
    
 

                                 |
27 | 13, 17, 18, 19, 20, 26 | syl113anc 1281 |
. 2
    
  


                                                      |
28 | | simp33 1047 |
. . . 4
    
  


                                                      |
29 | 28 | necomd 2681 |
. . 3
    
  


                                                      |
30 | 6, 7, 8, 23 | trlcocnvat 34303 |
. . 3
                        |
31 | 3, 12, 4, 29, 30 | syl121anc 1274 |
. 2
    
  


                                               
     |
32 | | simp1 1009 |
. . 3
    
  


                                              
   |
33 | | simp312 1157 |
. . 3
    
  


                                               |
34 | | simp32l 1134 |
. . 3
    
  


                                                      |
35 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 34425 |
. . 3
    
 

                                 |
36 | 32, 17, 18, 33, 34, 35 | syl113anc 1281 |
. 2
    
  


                                                      |
37 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksv2 34426 |
. . . . 5
    
 

                                     
        
       |
38 | 32, 17, 18, 33, 34, 37 | syl113anc 1281 |
. . . 4
    
  


                                                                           |
39 | | hllat 32941 |
. . . . . 6
   |
40 | 1, 39 | syl 17 |
. . . . 5
    
  


                                           
  |
41 | 21, 6, 7, 8, 23 | trlnidat 33751 |
. . . . . . 7
   
        |
42 | 3, 4, 33, 41 | syl3anc 1269 |
. . . . . 6
    
  


                                                  |
43 | 21, 22, 6 | hlatjcl 32944 |
. . . . . 6
 
             |
44 | 1, 2, 42, 43 | syl3anc 1269 |
. . . . 5
    
  


                                                    |
45 | 5, 6, 7, 8 | ltrnat 33717 |
. . . . . . 7
   

      |
46 | 3, 14, 2, 45 | syl3anc 1269 |
. . . . . 6
    
  


                                                  |
47 | 6, 7, 8, 23 | trlcocnvat 34303 |
. . . . . . 7
                        |
48 | 3, 4, 11, 34, 47 | syl121anc 1274 |
. . . . . 6
    
  


                                               
     |
49 | 21, 22, 6 | hlatjcl 32944 |
. . . . . 6
                  
          |
50 | 1, 46, 48, 49 | syl3anc 1269 |
. . . . 5
    
  


                                                           |
51 | 21, 5, 24 | latmle1 16334 |
. . . . 5
  
         
               
        
             |
52 | 40, 44, 50, 51 | syl3anc 1269 |
. . . 4
    
  


                                                  
        
             |
53 | 38, 52 | eqbrtrd 4426 |
. . 3
    
  


                                                            |
54 | 5, 22, 6, 7, 8, 23 | trljat1 33744 |
. . . 4
      
              |
55 | 3, 4, 15, 54 | syl3anc 1269 |
. . 3
    
  


                                                          |
56 | 53, 55 | breqtrd 4430 |
. 2
    
  


                                                            |
57 | | simp2 1010 |
. . 3
    
  


                                               
            |
58 | | simp31 1045 |
. . 3
    
  


                                                   |
59 | | eqid 2453 |
. . . 4
     
         
                      
                  |
60 | 21, 5, 22, 6, 7, 8,
23, 24, 25, 59 | cdlemk11 34428 |
. . 3
    
  


                       
                                     |
61 | 32, 57, 58, 34, 20, 60 | syl113anc 1281 |
. 2
    
  


                                                                       |
62 | 5, 22, 6 | hlatlej2 32953 |
. . . . 5
 
                 |
63 | 1, 2, 42, 62 | syl3anc 1269 |
. . . 4
    
  


                                                        |
64 | 63, 55 | breqtrd 4430 |
. . 3
    
  


                                                        |
65 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksel 34424 |
. . . . . 6
    
 

                             |
66 | 13, 17, 18, 19, 20, 65 | syl113anc 1281 |
. . . . 5
    
  


                                                  |
67 | 5, 6, 7, 8 | ltrnel 33716 |
. . . . 5
          
        
           |
68 | 3, 66, 15, 67 | syl3anc 1269 |
. . . 4
    
  


                                                                |
69 | 7, 8 | ltrncnv 33723 |
. . . . . . . 8
    
   |
70 | 3, 4, 69 | syl2anc 667 |
. . . . . . 7
    
  


                                            
  |
71 | 7, 8, 23 | trlcnv 33743 |
. . . . . . . . 9
    
           |
72 | 3, 4, 71 | syl2anc 667 |
. . . . . . . 8
    
  


                                                       |
73 | 72, 28 | eqnetrd 2693 |
. . . . . . 7
    
  


                                                       |
74 | 21, 7, 8, 23 | trlcone 34307 |
. . . . . . 7
     
          
  
         
    |
75 | 3, 70, 12, 73, 19, 74 | syl122anc 1278 |
. . . . . 6
    
  


                                                     
    |
76 | 75 | necomd 2681 |
. . . . 5
    
  


                                                
         |
77 | 7, 8 | ltrncom 34317 |
. . . . . . 7
       
      |
78 | 3, 70, 12, 77 | syl3anc 1269 |
. . . . . 6
    
  


                                                    |
79 | 78 | fveq2d 5874 |
. . . . 5
    
  


                                                
           |
80 | 76, 79, 72 | 3netr3d 2702 |
. . . 4
    
  


                                               
         |
81 | 7, 8 | ltrnco 34298 |
. . . . . 6
    

     |
82 | 3, 12, 70, 81 | syl3anc 1269 |
. . . . 5
    
  


                                                 |
83 | 5, 7, 8, 23 | trlle 33762 |
. . . . 5
       
         |
84 | 3, 82, 83 | syl2anc 667 |
. . . 4
    
  


                                               
     |
85 | 5, 7, 8, 23 | trlle 33762 |
. . . . 5
    
      |
86 | 3, 4, 85 | syl2anc 667 |
. . . 4
    
  


                                                  |
87 | 5, 22, 6, 7 | lhp2atnle 33610 |
. . . 4
                                                                                     |
88 | 3, 68, 80, 31, 84, 42, 86, 87 | syl322anc 1297 |
. . 3
    
  


                                                                   |
89 | | nbrne1 4423 |
. . 3
                                 
              
          |
90 | 64, 88, 89 | syl2anc 667 |
. 2
    
  


                                                              
      |
91 | 5, 22, 24, 6 | 2atm 33104 |
. 2
                    
                     
                         
    
                                      
            
       |
92 | 1, 2, 10, 27, 31, 36, 56, 61, 90, 91 | syl333anc 1301 |
1
    
  


                                                                               |