Proof of Theorem 4atlem11
Step | Hyp | Ref
| Expression |
1 | | 3anass 969 |
. . . 4
 
   
    
      
  
          
      
      |
2 | | simpl11 1063 |
. . . . . . 7
     
 
             |
3 | | hllat 33327 |
. . . . . . 7
   |
4 | 2, 3 | syl 16 |
. . . . . 6
     
 
             |
5 | | simpl2l 1041 |
. . . . . . 7
     
 
             |
6 | | eqid 2452 |
. . . . . . . 8
         |
7 | | 4at.a |
. . . . . . . 8
     |
8 | 6, 7 | atbase 33253 |
. . . . . . 7
       |
9 | 5, 8 | syl 16 |
. . . . . 6
     
 
                 |
10 | | simpl2r 1042 |
. . . . . . 7
     
 
             |
11 | 6, 7 | atbase 33253 |
. . . . . . 7
       |
12 | 10, 11 | syl 16 |
. . . . . 6
     
 
                 |
13 | | simpl12 1064 |
. . . . . . . 8
     
 
             |
14 | | simpl31 1069 |
. . . . . . . 8
     
 
             |
15 | | 4at.j |
. . . . . . . . 9
     |
16 | 6, 15, 7 | hlatjcl 33330 |
. . . . . . . 8
 
         |
17 | 2, 13, 14, 16 | syl3anc 1219 |
. . . . . . 7
     
 
                   |
18 | | simpl32 1070 |
. . . . . . . 8
     
 
             |
19 | | simpl33 1071 |
. . . . . . . 8
     
 
             |
20 | 6, 15, 7 | hlatjcl 33330 |
. . . . . . . 8
 
         |
21 | 2, 18, 19, 20 | syl3anc 1219 |
. . . . . . 7
     
 
                   |
22 | 6, 15 | latjcl 15335 |
. . . . . . 7
  
    
      
   
        |
23 | 4, 17, 21, 22 | syl3anc 1219 |
. . . . . 6
     
 
             
         |
24 | | 4at.l |
. . . . . . 7
     |
25 | 6, 24, 15 | latjle12 15346 |
. . . . . 6
  
   
      
             
      
  
           |
26 | 4, 9, 12, 23, 25 | syl13anc 1221 |
. . . . 5
     
 
                           
   
     |
27 | 26 | anbi2d 703 |
. . . 4
     
 
                       
    
        
   
           |
28 | 1, 27 | syl5bb 257 |
. . 3
     
 
                               
        
   
      |
29 | | simpl13 1065 |
. . . . 5
     
 
             |
30 | 6, 7 | atbase 33253 |
. . . . 5
       |
31 | 29, 30 | syl 16 |
. . . 4
     
 
                 |
32 | 6, 15, 7 | hlatjcl 33330 |
. . . . 5
 
         |
33 | 2, 5, 10, 32 | syl3anc 1219 |
. . . 4
     
 
                   |
34 | 6, 24, 15 | latjle12 15346 |
. . . 4
  
    
    
   
                 
   
  
             |
35 | 4, 31, 33, 23, 34 | syl13anc 1221 |
. . 3
     
 
                             
 
   
     |
36 | 28, 35 | bitrd 253 |
. 2
     
 
                               
             |
37 | | simpl1 991 |
. . . 4
     
 
           
   |
38 | | simpl2 992 |
. . . 4
     
 
           
   |
39 | 18, 19 | jca 532 |
. . . 4
     
 
           
   |
40 | | simpr 461 |
. . . 4
     
 
                     |
41 | 24, 15, 7 | 4atlem3a 33560 |
. . . 4
     
 
           
               |
42 | 37, 38, 39, 40, 41 | syl31anc 1222 |
. . 3
     
 
           
               |
43 | | simp1l 1012 |
. . . . . 6
    
 
 
                                     
 


    |
44 | | simp1r 1013 |
. . . . . 6
    
 
 
                                              |
45 | | simp2 989 |
. . . . . 6
    
 
 
                                          |
46 | | simp3 990 |
. . . . . 6
    
 
 
                                        
    
      
     |
47 | 24, 15, 7 | 4atlem11b 33571 |
. . . . . 6
     
 
     
       
 
                       
           |
48 | 43, 44, 45, 46, 47 | syl121anc 1224 |
. . . . 5
    
 
 
                                      
           |
49 | 48 | 3exp 1187 |
. . . 4
     
 
           
        
      
    
       
            |
50 | 2 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                      |
51 | 13 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                      |
52 | 29 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                      |
53 | 5 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                      |
54 | 10 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                      |
55 | 15, 7 | hlatj4 33337 |
. . . . . . 7
  


           
    |
56 | 50, 51, 52, 53, 54, 55 | syl122anc 1228 |
. . . . . 6
    
 
 
                                      
           |
57 | 50, 51, 53 | 3jca 1168 |
. . . . . . 7
    
 
 
                                    
   |
58 | 52, 54 | jca 532 |
. . . . . . 7
    
 
 
                                    
   |
59 | | simp1l3 1083 |
. . . . . . 7
    
 
 
                                    
   |
60 | | simp1r2 1085 |
. . . . . . . . 9
    
 
 
                                        |
61 | 24, 15, 7 | 4atlem0be 33558 |
. . . . . . . . 9
  

     |
62 | 50, 51, 52, 53, 60, 61 | syl131anc 1232 |
. . . . . . . 8
    
 
 
                                      |
63 | | simp1r1 1084 |
. . . . . . . . 9
    
 
 
                                      |
64 | 24, 15, 7 | 4atlem0ae 33557 |
. . . . . . . . 9
  

    
    |
65 | 50, 51, 52, 53, 63, 60, 64 | syl132anc 1237 |
. . . . . . . 8
    
 
 
                                        |
66 | | simp1r3 1086 |
. . . . . . . . 9
    
 
 
                                          |
67 | 15, 7 | hlatj32 33335 |
. . . . . . . . . . 11
  
    
       |
68 | 50, 51, 52, 53, 67 | syl13anc 1221 |
. . . . . . . . . 10
    
 
 
                                      
       |
69 | 68 | breq2d 4407 |
. . . . . . . . 9
    
 
 
                                        
       |
70 | 66, 69 | mtbid 300 |
. . . . . . . 8
    
 
 
                                          |
71 | 62, 65, 70 | 3jca 1168 |
. . . . . . 7
    
 
 
                                              |
72 | | simp2 989 |
. . . . . . 7
    
 
 
                                          |
73 | | simp32 1025 |
. . . . . . 7
    
 
 
                                            |
74 | | simp31 1024 |
. . . . . . 7
    
 
 
                                            |
75 | | simp33 1026 |
. . . . . . 7
    
 
 
                                            |
76 | 24, 15, 7 | 4atlem11b 33571 |
. . . . . . 7
     
 
     
       
 
                       
           |
77 | 57, 58, 59, 71, 72, 73, 74, 75, 76 | syl323anc 1249 |
. . . . . 6
    
 
 
                                      
           |
78 | 56, 77 | eqtrd 2493 |
. . . . 5
    
 
 
                                      
           |
79 | 78 | 3exp 1187 |
. . . 4
     
 
           
        
      
    
       
            |
80 | 6, 7 | atbase 33253 |
. . . . . . . . . 10
       |
81 | 13, 80 | syl 16 |
. . . . . . . . 9
     
 
                 |
82 | 6, 15 | latj4rot 15386 |
. . . . . . . . 9
  
   
     
   
         
          |
83 | 4, 81, 31, 9, 12, 82 | syl122anc 1228 |
. . . . . . . 8
     
 
             
           |
84 | 15, 7 | hlatjcom 33331 |
. . . . . . . . . 10
 
       |
85 | 2, 10, 13, 84 | syl3anc 1219 |
. . . . . . . . 9
     
 
                 |
86 | 85 | oveq1d 6210 |
. . . . . . . 8
     
 
             
           |
87 | 83, 86 | eqtrd 2493 |
. . . . . . 7
     
 
             
           |
88 | 87 | 3ad2ant1 1009 |
. . . . . 6
    
 
 
                                      
           |
89 | 2, 13, 10 | 3jca 1168 |
. . . . . . . . 9
     
 
           
   |
90 | 29, 5 | jca 532 |
. . . . . . . . 9
     
 
           
   |
91 | | simpl3 993 |
. . . . . . . . 9
     
 
           
   |
92 | 89, 90, 91 | 3jca 1168 |
. . . . . . . 8
     
 
            
 


    |
93 | 92 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                     
 


    |
94 | 24, 15, 7 | 4noncolr1 33418 |
. . . . . . . . . 10
  
 

  
                |
95 | 37, 38, 40, 94 | syl3anc 1219 |
. . . . . . . . 9
     
 
                     |
96 | | necom 2718 |
. . . . . . . . . . 11

  |
97 | 96 | a1i 11 |
. . . . . . . . . 10
     
 
           
   |
98 | 85 | breq2d 4407 |
. . . . . . . . . . 11
     
 
             
     |
99 | 98 | notbid 294 |
. . . . . . . . . 10
     
 
           
 
     |
100 | 85 | oveq1d 6210 |
. . . . . . . . . . . 12
     
 
             
       |
101 | 100 | breq2d 4407 |
. . . . . . . . . . 11
     
 
               
       |
102 | 101 | notbid 294 |
. . . . . . . . . 10
     
 
           
   
       |
103 | 97, 99, 102 | 3anbi123d 1290 |
. . . . . . . . 9
     
 
              
       
        |
104 | 95, 103 | mpbid 210 |
. . . . . . . 8
     
 
                     |
105 | 104 | 3ad2ant1 1009 |
. . . . . . 7
    
 
 
                                              |
106 | | simp2 989 |
. . . . . . 7
    
 
 
                                          |
107 | | simpr3 996 |
. . . . . . . . 9
    
 
 
               
    
      
       
    |
108 | | simpr1 994 |
. . . . . . . . 9
    
 
 
               
    
      
       
    |
109 | | simpr2 995 |
. . . . . . . . 9
    
 
 
               
    
      
       
    |
110 | 107, 108,
109 | 3jca 1168 |
. . . . . . . 8
    
 
 
               
    
      
                          |
111 | 110 | 3adant2 1007 |
. . . . . . 7
    
 
 
                                        
    
      
     |
112 | 24, 15, 7 | 4atlem11b 33571 |
. . . . . . 7
     
 
     
       
 
                       
           |
113 | 93, 105, 106, 111, 112 | syl121anc 1224 |
. . . . . 6
    
 
 
                                      
           |
114 | 88, 113 | eqtrd 2493 |
. . . . 5
    
 
 
                                      
           |
115 | 114 | 3exp 1187 |
. . . 4
     
 
           
        
      
    
       
            |
116 | 49, 79, 115 | 3jaod 1283 |
. . 3
     
 
               
                              
   
            |
117 | 42, 116 | mpd 15 |
. 2
     
 
                                         
     |
118 | 36, 117 | sylbird 235 |
1
     
 
                         
           |