Proof of Theorem osumcllem9N
Step | Hyp | Ref
| Expression |
1 | | inass 3658 |
. . . . . . 7
 
    
      |
2 | | simp11 1018 |
. . . . . . . . 9
  
    
  
  |
3 | | simp13 1020 |
. . . . . . . . 9
  
    
  
  |
4 | | simp21 1021 |
. . . . . . . . 9
  
    
       |
5 | | osumcllem.l |
. . . . . . . . . 10
     |
6 | | osumcllem.j |
. . . . . . . . . 10
     |
7 | | osumcllem.a |
. . . . . . . . . 10
     |
8 | | osumcllem.p |
. . . . . . . . . 10
      |
9 | | osumcllem.o |
. . . . . . . . . 10
      |
10 | | osumcllem.c |
. . . . . . . . . 10
     |
11 | | osumcllem.m |
. . . . . . . . . 10
     |
12 | | osumcllem.u |
. . . . . . . . . 10
       |
13 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem3N 33908 |
. . . . . . . . 9
 
         |
14 | 2, 3, 4, 13 | syl3anc 1219 |
. . . . . . . 8
  
    
     
   |
15 | 14 | ineq1d 3649 |
. . . . . . 7
  
    
       
     |
16 | 1, 15 | syl5eqr 2506 |
. . . . . 6
  
    
     
       |
17 | | simp12 1019 |
. . . . . . . 8
  
    
  
  |
18 | 7, 10 | psubclssatN 33891 |
. . . . . . . 8
 

  |
19 | 2, 17, 18 | syl2anc 661 |
. . . . . . 7
  
    
     |
20 | 7, 10 | psubclssatN 33891 |
. . . . . . . 8
 

  |
21 | 2, 3, 20 | syl2anc 661 |
. . . . . . 7
  
    
     |
22 | | simp22 1022 |
. . . . . . 7
  
    
     |
23 | 7, 8 | paddssat 33764 |
. . . . . . . . . . . 12
       |
24 | 2, 19, 21, 23 | syl3anc 1219 |
. . . . . . . . . . 11
  
    
    
  |
25 | 7, 9 | polssatN 33858 |
. . . . . . . . . . 11
  
        |
26 | 2, 24, 25 | syl2anc 661 |
. . . . . . . . . 10
  
    
         |
27 | 7, 9 | polssatN 33858 |
. . . . . . . . . 10
            
  |
28 | 2, 26, 27 | syl2anc 661 |
. . . . . . . . 9
  
    
           |
29 | 12, 28 | syl5eqss 3498 |
. . . . . . . 8
  
    
     |
30 | | simp23 1023 |
. . . . . . . 8
  
    
  
  |
31 | 29, 30 | sseldd 3455 |
. . . . . . 7
  
    
  
  |
32 | | simp3 990 |
. . . . . . 7
  
    
  
    |
33 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem8N 33913 |
. . . . . . 7
  
 
  
       |
34 | 2, 19, 21, 4, 22, 31, 32, 33 | syl331anc 1244 |
. . . . . 6
  
    
       |
35 | 16, 34 | eqtrd 2492 |
. . . . 5
  
    
     
     |
36 | 35 | fveq2d 5793 |
. . . 4
  
    
          
    |
37 | 7, 9 | pol0N 33859 |
. . . . 5
     |
38 | 2, 37 | syl 16 |
. . . 4
  
    
       |
39 | 36, 38 | eqtrd 2492 |
. . 3
  
    
             |
40 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem1N 33906 |
. . . 4
  

     |
41 | 2, 19, 21, 30, 40 | syl31anc 1222 |
. . 3
  
    
       |
42 | 39, 41 | ineq12d 3651 |
. 2
  
    
                   |
43 | 7, 9, 10 | polsubclN 33902 |
. . . . . 6
               |
44 | 2, 26, 43 | syl2anc 661 |
. . . . 5
  
    
           |
45 | 12, 44 | syl5eqel 2543 |
. . . 4
  
    
  
  |
46 | 7, 8, 10 | paddatclN 33899 |
. . . . . 6
 
       |
47 | 2, 17, 31, 46 | syl3anc 1219 |
. . . . 5
  
    
         |
48 | 11, 47 | syl5eqel 2543 |
. . . 4
  
    
  
  |
49 | 10 | psubclinN 33898 |
. . . 4
 
     |
50 | 2, 45, 48, 49 | syl3anc 1219 |
. . 3
  
    
       |
51 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem2N 33907 |
. . . 4
  


    |
52 | 2, 19, 21, 30, 51 | syl31anc 1222 |
. . 3
  
    
       |
53 | 10, 9 | poml6N 33905 |
. . 3
   
                   |
54 | 2, 17, 50, 52, 53 | syl31anc 1222 |
. 2
  
    
                 |
55 | 31 | snssd 4116 |
. . . . 5
  
    
       |
56 | 7, 8 | paddssat 33764 |
. . . . 5
    
      |
57 | 2, 19, 55, 56 | syl3anc 1219 |
. . . 4
  
    
         |
58 | 11, 57 | syl5eqss 3498 |
. . 3
  
    
     |
59 | | sseqin2 3667 |
. . 3

    |
60 | 58, 59 | sylib 196 |
. 2
  
    
       |
61 | 42, 54, 60 | 3eqtr3rd 2501 |
1
  
    
  
  |