Proof of Theorem 4atlem11
Step | Hyp | Ref
| Expression |
1 | | 3anass 990 |
. . . 4
 
   
    
      
  
          
      
      |
2 | | simpl11 1084 |
. . . . . . 7
     
 
             |
3 | | hllat 32931 |
. . . . . . 7
   |
4 | 2, 3 | syl 17 |
. . . . . 6
     
 
             |
5 | | simpl2l 1062 |
. . . . . . 7
     
 
             |
6 | | eqid 2452 |
. . . . . . . 8
         |
7 | | 4at.a |
. . . . . . . 8
     |
8 | 6, 7 | atbase 32857 |
. . . . . . 7
       |
9 | 5, 8 | syl 17 |
. . . . . 6
     
 
                 |
10 | | simpl2r 1063 |
. . . . . . 7
     
 
             |
11 | 6, 7 | atbase 32857 |
. . . . . . 7
       |
12 | 10, 11 | syl 17 |
. . . . . 6
     
 
                 |
13 | | simpl12 1085 |
. . . . . . . 8
     
 
             |
14 | | simpl31 1090 |
. . . . . . . 8
     
 
             |
15 | | 4at.j |
. . . . . . . . 9
     |
16 | 6, 15, 7 | hlatjcl 32934 |
. . . . . . . 8
 
         |
17 | 2, 13, 14, 16 | syl3anc 1271 |
. . . . . . 7
     
 
                   |
18 | | simpl32 1091 |
. . . . . . . 8
     
 
             |
19 | | simpl33 1092 |
. . . . . . . 8
     
 
             |
20 | 6, 15, 7 | hlatjcl 32934 |
. . . . . . . 8
 
         |
21 | 2, 18, 19, 20 | syl3anc 1271 |
. . . . . . 7
     
 
                   |
22 | 6, 15 | latjcl 16308 |
. . . . . . 7
  
    
      
   
        |
23 | 4, 17, 21, 22 | syl3anc 1271 |
. . . . . 6
     
 
             
         |
24 | | 4at.l |
. . . . . . 7
     |
25 | 6, 24, 15 | latjle12 16319 |
. . . . . 6
  
   
      
             
      
  
           |
26 | 4, 9, 12, 23, 25 | syl13anc 1273 |
. . . . 5
     
 
                           
   
     |
27 | 26 | anbi2d 715 |
. . . 4
     
 
                       
    
        
   
           |
28 | 1, 27 | syl5bb 265 |
. . 3
     
 
                               
        
   
      |
29 | | simpl13 1086 |
. . . . 5
     
 
             |
30 | 6, 7 | atbase 32857 |
. . . . 5
       |
31 | 29, 30 | syl 17 |
. . . 4
     
 
                 |
32 | 6, 15, 7 | hlatjcl 32934 |
. . . . 5
 
         |
33 | 2, 5, 10, 32 | syl3anc 1271 |
. . . 4
     
 
                   |
34 | 6, 24, 15 | latjle12 16319 |
. . . 4
  
    
    
   
                 
   
  
             |
35 | 4, 31, 33, 23, 34 | syl13anc 1273 |
. . 3
     
 
                             
 
   
     |
36 | 28, 35 | bitrd 261 |
. 2
     
 
                               
             |
37 | | simpl1 1012 |
. . . 4
     
 
           
   |
38 | | simpl2 1013 |
. . . 4
     
 
           
   |
39 | 18, 19 | jca 539 |
. . . 4
     
 
           
   |
40 | | simpr 467 |
. . . 4
     
 
                     |
41 | 24, 15, 7 | 4atlem3a 33164 |
. . . 4
     
 
           
               |
42 | 37, 38, 39, 40, 41 | syl31anc 1274 |
. . 3
     
 
           
               |
43 | | simp1l 1033 |
. . . . . 6
    
 
 
                                     
 


    |
44 | | simp1r 1034 |
. . . . . 6
    
 
 
                                              |
45 | | simp2 1010 |
. . . . . 6
    
 
 
                                          |
46 | | simp3 1011 |
. . . . . 6
    
 
 
                                        
    
      
     |
47 | 24, 15, 7 | 4atlem11b 33175 |
. . . . . 6
     
 
     
       
 
                       
           |
48 | 43, 44, 45, 46, 47 | syl121anc 1276 |
. . . . 5
    
 
 
                                      
           |
49 | 48 | 3exp 1209 |
. . . 4
     
 
           
        
      
    
       
            |
50 | 2 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                      |
51 | 13 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                      |
52 | 29 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                      |
53 | 5 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                      |
54 | 10 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                      |
55 | 15, 7 | hlatj4 32941 |
. . . . . . 7
  


           
    |
56 | 50, 51, 52, 53, 54, 55 | syl122anc 1280 |
. . . . . 6
    
 
 
                                      
           |
57 | 50, 51, 53 | 3jca 1189 |
. . . . . . 7
    
 
 
                                    
   |
58 | 52, 54 | jca 539 |
. . . . . . 7
    
 
 
                                    
   |
59 | | simp1l3 1104 |
. . . . . . 7
    
 
 
                                    
   |
60 | | simp1r2 1106 |
. . . . . . . . 9
    
 
 
                                        |
61 | 24, 15, 7 | 4atlem0be 33162 |
. . . . . . . . 9
  

     |
62 | 50, 51, 52, 53, 60, 61 | syl131anc 1284 |
. . . . . . . 8
    
 
 
                                      |
63 | | simp1r1 1105 |
. . . . . . . . 9
    
 
 
                                      |
64 | 24, 15, 7 | 4atlem0ae 33161 |
. . . . . . . . 9
  

    
    |
65 | 50, 51, 52, 53, 63, 60, 64 | syl132anc 1289 |
. . . . . . . 8
    
 
 
                                        |
66 | | simp1r3 1107 |
. . . . . . . . 9
    
 
 
                                          |
67 | 15, 7 | hlatj32 32939 |
. . . . . . . . . . 11
  
    
       |
68 | 50, 51, 52, 53, 67 | syl13anc 1273 |
. . . . . . . . . 10
    
 
 
                                      
       |
69 | 68 | breq2d 4386 |
. . . . . . . . 9
    
 
 
                                        
       |
70 | 66, 69 | mtbid 306 |
. . . . . . . 8
    
 
 
                                          |
71 | 62, 65, 70 | 3jca 1189 |
. . . . . . 7
    
 
 
                                              |
72 | | simp2 1010 |
. . . . . . 7
    
 
 
                                          |
73 | | simp32 1046 |
. . . . . . 7
    
 
 
                                            |
74 | | simp31 1045 |
. . . . . . 7
    
 
 
                                            |
75 | | simp33 1047 |
. . . . . . 7
    
 
 
                                            |
76 | 24, 15, 7 | 4atlem11b 33175 |
. . . . . . 7
     
 
     
       
 
                       
           |
77 | 57, 58, 59, 71, 72, 73, 74, 75, 76 | syl323anc 1301 |
. . . . . 6
    
 
 
                                      
           |
78 | 56, 77 | eqtrd 2486 |
. . . . 5
    
 
 
                                      
           |
79 | 78 | 3exp 1209 |
. . . 4
     
 
           
        
      
    
       
            |
80 | 6, 7 | atbase 32857 |
. . . . . . . . . 10
       |
81 | 13, 80 | syl 17 |
. . . . . . . . 9
     
 
                 |
82 | 6, 15 | latj4rot 16359 |
. . . . . . . . 9
  
   
     
   
         
          |
83 | 4, 81, 31, 9, 12, 82 | syl122anc 1280 |
. . . . . . . 8
     
 
             
           |
84 | 15, 7 | hlatjcom 32935 |
. . . . . . . . . 10
 
       |
85 | 2, 10, 13, 84 | syl3anc 1271 |
. . . . . . . . 9
     
 
                 |
86 | 85 | oveq1d 6291 |
. . . . . . . 8
     
 
             
           |
87 | 83, 86 | eqtrd 2486 |
. . . . . . 7
     
 
             
           |
88 | 87 | 3ad2ant1 1030 |
. . . . . 6
    
 
 
                                      
           |
89 | 2, 13, 10 | 3jca 1189 |
. . . . . . . . 9
     
 
           
   |
90 | 29, 5 | jca 539 |
. . . . . . . . 9
     
 
           
   |
91 | | simpl3 1014 |
. . . . . . . . 9
     
 
           
   |
92 | 89, 90, 91 | 3jca 1189 |
. . . . . . . 8
     
 
            
 


    |
93 | 92 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                     
 


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

  
                |
95 | 37, 38, 40, 94 | syl3anc 1271 |
. . . . . . . . 9
     
 
                     |
96 | | necom 2677 |
. . . . . . . . . . 11

  |
97 | 96 | a1i 11 |
. . . . . . . . . 10
     
 
           
   |
98 | 85 | breq2d 4386 |
. . . . . . . . . . 11
     
 
             
     |
99 | 98 | notbid 300 |
. . . . . . . . . 10
     
 
           
 
     |
100 | 85 | oveq1d 6291 |
. . . . . . . . . . . 12
     
 
             
       |
101 | 100 | breq2d 4386 |
. . . . . . . . . . 11
     
 
               
       |
102 | 101 | notbid 300 |
. . . . . . . . . 10
     
 
           
   
       |
103 | 97, 99, 102 | 3anbi123d 1343 |
. . . . . . . . 9
     
 
              
       
        |
104 | 95, 103 | mpbid 215 |
. . . . . . . 8
     
 
                     |
105 | 104 | 3ad2ant1 1030 |
. . . . . . 7
    
 
 
                                              |
106 | | simp2 1010 |
. . . . . . 7
    
 
 
                                          |
107 | | simpr3 1017 |
. . . . . . . . 9
    
 
 
               
    
      
       
    |
108 | | simpr1 1015 |
. . . . . . . . 9
    
 
 
               
    
      
       
    |
109 | | simpr2 1016 |
. . . . . . . . 9
    
 
 
               
    
      
       
    |
110 | 107, 108,
109 | 3jca 1189 |
. . . . . . . 8
    
 
 
               
    
      
                          |
111 | 110 | 3adant2 1028 |
. . . . . . 7
    
 
 
                                        
    
      
     |
112 | 24, 15, 7 | 4atlem11b 33175 |
. . . . . . 7
     
 
     
       
 
                       
           |
113 | 93, 105, 106, 111, 112 | syl121anc 1276 |
. . . . . 6
    
 
 
                                      
           |
114 | 88, 113 | eqtrd 2486 |
. . . . 5
    
 
 
                                      
           |
115 | 114 | 3exp 1209 |
. . . 4
     
 
           
        
      
    
       
            |
116 | 49, 79, 115 | 3jaod 1336 |
. . 3
     
 
               
                              
   
            |
117 | 42, 116 | mpd 15 |
. 2
     
 
                                         
     |
118 | 36, 117 | sylbird 243 |
1
     
 
                         
           |