Step | Hyp | Ref
| Expression |
1 | | prop 7474 |
. . . . . . 7
              |
2 | | prnmaddl 7489 |
. . . . . . 7
                  
        |
3 | 1, 2 | sylan 283 |
. . . . . 6
 
     
        |
4 | 3 | 3ad2antl2 1160 |
. . . . 5
  

              |
5 | 4 | adantlr 477 |
. . . 4
   
          
         |
6 | | simprl 529 |
. . . . . 6
                           |
7 | | halfnqq 7409 |
. . . . . 6
      |
8 | 6, 7 | syl 14 |
. . . . 5
                              |
9 | | simplll 533 |
. . . . . . . . . 10
                         
   |
10 | 9 | adantr 276 |
. . . . . . . . 9
     
                    
    
   |
11 | 10 | simp1d 1009 |
. . . . . . . 8
     
                    
      |
12 | | prop 7474 |
. . . . . . . 8
              |
13 | 11, 12 | syl 14 |
. . . . . . 7
     
                    
                 |
14 | | simprl 529 |
. . . . . . 7
     
                    
      |
15 | | prarloc2 7503 |
. . . . . . 7
                            |
16 | 13, 14, 15 | syl2anc 411 |
. . . . . 6
     
                    
                  |
17 | 9 | ad2antrr 488 |
. . . . . . . . . . . 12
      
                             
        
   |
18 | 17 | simp1d 1009 |
. . . . . . . . . . 11
      
                             
          |
19 | 17 | simp2d 1010 |
. . . . . . . . . . 11
      
                             
          |
20 | | addclpr 7536 |
. . . . . . . . . . 11
 
     |
21 | 18, 19, 20 | syl2anc 411 |
. . . . . . . . . 10
      
                             
            |
22 | | prop 7474 |
. . . . . . . . . 10
                    |
23 | 21, 22 | syl 14 |
. . . . . . . . 9
      
                             
                         |
24 | 18, 12 | syl 14 |
. . . . . . . . . . 11
      
                             
                     |
25 | | simprl 529 |
. . . . . . . . . . 11
      
                             
              |
26 | | elprnql 7480 |
. . . . . . . . . . 11
                 
  |
27 | 24, 25, 26 | syl2anc 411 |
. . . . . . . . . 10
      
                             
          |
28 | 19, 1 | syl 14 |
. . . . . . . . . . . 12
      
                             
                     |
29 | | simplr 528 |
. . . . . . . . . . . . 13
                               |
30 | 29 | ad2antrr 488 |
. . . . . . . . . . . 12
      
                             
              |
31 | | elprnql 7480 |
. . . . . . . . . . . 12
                    |
32 | 28, 30, 31 | syl2anc 411 |
. . . . . . . . . . 11
      
                             
          |
33 | | simplrl 535 |
. . . . . . . . . . . 12
     
                    
      |
34 | 33 | adantr 276 |
. . . . . . . . . . 11
      
                             
          |
35 | | addclnq 7374 |
. . . . . . . . . . 11
 
     |
36 | 32, 34, 35 | syl2anc 411 |
. . . . . . . . . 10
      
                             
            |
37 | | addclnq 7374 |
. . . . . . . . . 10
           |
38 | 27, 36, 37 | syl2anc 411 |
. . . . . . . . 9
      
                             
              |
39 | | prdisj 7491 |
. . . . . . . . 9
                                              |
40 | 23, 38, 39 | syl2anc 411 |
. . . . . . . 8
      
                             
                                |
41 | 18 | adantr 276 |
. . . . . . . . . 10
       
                             
                 |
42 | 19 | adantr 276 |
. . . . . . . . . 10
       
                             
                 |
43 | | simplrl 535 |
. . . . . . . . . 10
       
                             
                     |
44 | | simplrr 536 |
. . . . . . . . . . 11
     
                    
            |
45 | 44 | ad2antrr 488 |
. . . . . . . . . 10
       
                             
                       |
46 | | df-iplp 7467 |
. . . . . . . . . . . 12
 
            
                
       |
47 | | addclnq 7374 |
. . . . . . . . . . . 12
 
     |
48 | 46, 47 | genpprecll 7513 |
. . . . . . . . . . 11
 
      
      
             |
49 | 48 | imp 124 |
. . . . . . . . . 10
                             |
50 | 41, 42, 43, 45, 49 | syl22anc 1239 |
. . . . . . . . 9
       
                             
                           |
51 | 27 | adantr 276 |
. . . . . . . . . . . . 13
       
                             
                 |
52 | 14 | ad2antrr 488 |
. . . . . . . . . . . . 13
       
                             
                 |
53 | 32 | adantr 276 |
. . . . . . . . . . . . 13
       
                             
                 |
54 | | addcomnqg 7380 |
. . . . . . . . . . . . . 14
 
       |
55 | 54 | adantl 277 |
. . . . . . . . . . . . 13
                             
                          
      |
56 | | addassnqg 7381 |
. . . . . . . . . . . . . 14
 
           |
57 | 56 | adantl 277 |
. . . . . . . . . . . . 13
                             
                        
 
          |
58 | | addclnq 7374 |
. . . . . . . . . . . . . 14
 
     |
59 | 58 | adantl 277 |
. . . . . . . . . . . . 13
                             
                          
    |
60 | 51, 52, 53, 55, 57, 52, 59 | caov4d 6059 |
. . . . . . . . . . . 12
       
                             
                             |
61 | | simprr 531 |
. . . . . . . . . . . . . 14
     
                    
        |
62 | 61 | ad2antrr 488 |
. . . . . . . . . . . . 13
       
                             
                   |
63 | 62 | oveq2d 5891 |
. . . . . . . . . . . 12
       
                             
                           |
64 | 33 | ad2antrr 488 |
. . . . . . . . . . . . 13
       
                             
                 |
65 | | addassnqg 7381 |
. . . . . . . . . . . . 13
 
           |
66 | 51, 53, 64, 65 | syl3anc 1238 |
. . . . . . . . . . . 12
       
                             
                         |
67 | 60, 63, 66 | 3eqtrd 2214 |
. . . . . . . . . . 11
       
                             
                           |
68 | | simplrr 536 |
. . . . . . . . . . . 12
       
                             
                       |
69 | | simpr 110 |
. . . . . . . . . . . 12
       
                             
                       |
70 | 17 | simp3d 1011 |
. . . . . . . . . . . . . 14
      
                             
          |
71 | 70 | adantr 276 |
. . . . . . . . . . . . 13
       
                             
                 |
72 | 46, 47 | genppreclu 7514 |
. . . . . . . . . . . . 13
 
        
      
               |
73 | 41, 71, 72 | syl2anc 411 |
. . . . . . . . . . . 12
       
                             
                             
               |
74 | 68, 69, 73 | mp2and 433 |
. . . . . . . . . . 11
       
                             
                             |
75 | 67, 74 | eqeltrrd 2255 |
. . . . . . . . . 10
       
                             
                           |
76 | | simpr 110 |
. . . . . . . . . . . . 13
  
            |
77 | 76 | ad3antrrr 492 |
. . . . . . . . . . . 12
     
                    
          |
78 | 77 | ad2antrr 488 |
. . . . . . . . . . 11
       
                             
                     |
79 | | fveq2 5516 |
. . . . . . . . . . . 12
    
              |
80 | 79 | eleq2d 2247 |
. . . . . . . . . . 11
    
                        |
81 | 78, 80 | syl 14 |
. . . . . . . . . 10
       
                             
                         
             |
82 | 75, 81 | mpbird 167 |
. . . . . . . . 9
       
                             
                           |
83 | 50, 82 | jca 306 |
. . . . . . . 8
       
                             
                                       |
84 | 40, 83 | mtand 665 |
. . . . . . 7
      
                             
                |
85 | | prop 7474 |
. . . . . . . . 9
              |
86 | 70, 85 | syl 14 |
. . . . . . . 8
      
                             
                     |
87 | | simplrl 535 |
. . . . . . . . 9
      
                             
          |
88 | | ltaddnq 7406 |
. . . . . . . . 9
 

    |
89 | 32, 87, 88 | syl2anc 411 |
. . . . . . . 8
      
                             
            |
90 | | prloc 7490 |
. . . . . . . 8
            
                 |
91 | 86, 89, 90 | syl2anc 411 |
. . . . . . 7
      
                             
                      |
92 | 84, 91 | ecased 1349 |
. . . . . 6
      
                             
              |
93 | 16, 92 | rexlimddv 2599 |
. . . . 5
     
                    
          |
94 | 8, 93 | rexlimddv 2599 |
. . . 4
                               |
95 | 5, 94 | rexlimddv 2599 |
. . 3
   
          
      |
96 | 95 | ex 115 |
. 2
  
          
       |
97 | 96 | ssrdv 3162 |
1
  
         
      |