Step | Hyp | Ref
| Expression |
1 | | cply1mul.p |
. . . . . . . . . 10
Poly1   |
2 | | cply1mul.m |
. . . . . . . . . 10
     |
3 | | eqid 2450 |
. . . . . . . . . 10
         |
4 | | cply1mul.b |
. . . . . . . . . 10
     |
5 | 1, 2, 3, 4 | coe1mul 18856 |
. . . . . . . . 9
 
 coe1 
  
 g        coe1            coe1             |
6 | 5 | 3expb 1208 |
. . . . . . . 8
  
 
coe1      g        coe1            coe1             |
7 | 6 | adantr 467 |
. . . . . . 7
   
  
  coe1      coe1      coe1     
g        coe1            coe1             |
8 | 7 | adantr 467 |
. . . . . 6
          coe1      coe1     
 coe1     
g        coe1            coe1             |
9 | | oveq2 6296 |
. . . . . . . . 9
           |
10 | | oveq1 6295 |
. . . . . . . . . . 11
       |
11 | 10 | fveq2d 5867 |
. . . . . . . . . 10
  coe1        coe1    
    |
12 | 11 | oveq2d 6304 |
. . . . . . . . 9
   coe1            coe1          coe1            coe1          |
13 | 9, 12 | mpteq12dv 4480 |
. . . . . . . 8
        coe1            coe1                coe1            coe1           |
14 | 13 | oveq2d 6304 |
. . . . . . 7
  g        coe1            coe1           g        coe1            coe1            |
15 | 14 | adantl 468 |
. . . . . 6
    

 
   coe1      coe1         g        coe1            coe1           g        coe1            coe1            |
16 | | nnnn0 10873 |
. . . . . . 7
   |
17 | 16 | adantl 468 |
. . . . . 6
          coe1      coe1     
   |
18 | | ovex 6316 |
. . . . . . 7
 g        coe1            coe1           |
19 | 18 | a1i 11 |
. . . . . 6
          coe1      coe1     
  g        coe1            coe1            |
20 | 8, 15, 17, 19 | fvmptd 5952 |
. . . . 5
          coe1      coe1     
  coe1        g        coe1            coe1            |
21 | | r19.26 2916 |
. . . . . . . . . 10
 
  coe1      coe1    
 
 coe1       coe1       |
22 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . 20
       |
23 | | nncn 10614 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
24 | 23 | subid1d 9972 |
. . . . . . . . . . . . . . . . . . . . 21
     |
25 | 24 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
26 | 22, 25 | sylan9eqr 2506 |
. . . . . . . . . . . . . . . . . . 19
        
    |
27 | | simpll 759 |
. . . . . . . . . . . . . . . . . . 19
        
  |
28 | 26, 27 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . 18
        
    |
29 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
    coe1      coe1    
    |
30 | 29 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . 19
     coe1      coe1    
    |
31 | 30 | rspcv 3145 |
. . . . . . . . . . . . . . . . . 18
    
 coe1      coe1    
    |
32 | 28, 31 | syl 17 |
. . . . . . . . . . . . . . . . 17
        
 
 coe1      coe1    
    |
33 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . 21
  coe1    
    coe1            coe1          coe1            |
34 | | simpll 759 |
. . . . . . . . . . . . . . . . . . . . . 22
   
             |
35 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
36 | 35 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 
  |
37 | | elfznn0 11884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
38 | 37 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
39 | 38 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
  |
40 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1  coe1   |
41 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
42 | 40, 4, 1, 41 | coe1fvalcl 18798 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  coe1           |
43 | 36, 39, 42 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . 22
   
            coe1           |
44 | | cply1mul.0 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
45 | 41, 3, 44 | ringrz 17811 |
. . . . . . . . . . . . . . . . . . . . . 22
   coe1         
  coe1           |
46 | 34, 43, 45 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
   
             coe1           |
47 | 33, 46 | sylan9eqr 2506 |
. . . . . . . . . . . . . . . . . . . 20
                 coe1         coe1            coe1         |
48 | 47 | ex 436 |
. . . . . . . . . . . . . . . . . . 19
   
             coe1    
    coe1            coe1          |
49 | 48 | expcom 437 |
. . . . . . . . . . . . . . . . . 18
        
 

 
  coe1    
    coe1            coe1           |
50 | 49 | com23 81 |
. . . . . . . . . . . . . . . . 17
        
  coe1    
         coe1            coe1           |
51 | 32, 50 | syld 45 |
. . . . . . . . . . . . . . . 16
        
 
 coe1            coe1            coe1           |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . 15
 
 coe1                     coe1            coe1           |
53 | 52 | expd 438 |
. . . . . . . . . . . . . 14
 
 coe1                    coe1            coe1            |
54 | 53 | com24 90 |
. . . . . . . . . . . . 13
 
 coe1                    coe1            coe1    
       |
55 | 54 | adantl 468 |
. . . . . . . . . . . 12
    coe1       coe1    
 

 
          coe1            coe1            |
56 | 55 | com13 83 |
. . . . . . . . . . 11
   
      coe1       coe1              coe1            coe1            |
57 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
58 | 57 | biimpri 210 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
59 | 58, 37 | anim12ci 570 |
. . . . . . . . . . . . . . . . . . . . 21
      
    |
60 | | elnnne0 10880 |
. . . . . . . . . . . . . . . . . . . . 21

    |
61 | 59, 60 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . 20
      
  |
62 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . 22
  coe1      coe1       |
63 | 62 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . . . 21
   coe1      coe1       |
64 | 63 | rspcv 3145 |
. . . . . . . . . . . . . . . . . . . 20
  
 coe1      coe1       |
65 | 61, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      
 
 coe1      coe1       |
66 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  coe1       coe1            coe1              coe1          |
67 | | simpll 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
         |
68 | 4 | eleq2i 2520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

      |
69 | 68 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
70 | 69 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
71 | 70 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
 
      |
72 | | fznn0sub 11828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
73 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
coe1  coe1   |
74 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
75 | 73, 74, 1, 41 | coe1fvalcl 18798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          coe1    
        |
76 | 71, 72, 75 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
        coe1    
        |
77 | 41, 3, 44 | ringlz 17810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   coe1    
      
      coe1    
    |
78 | 67, 76, 77 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
             coe1         |
79 | 66, 78 | sylan9eqr 2506 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
      coe1       coe1            coe1    
    |
80 | 79 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
         coe1       coe1            coe1          |
81 | 80 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 
    
  coe1       coe1            coe1           |
82 | 81 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 
  coe1            coe1            coe1           |
83 | 82 | a1dd 47 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
  coe1             coe1            coe1            |
84 | 83 | com14 91 |
. . . . . . . . . . . . . . . . . . . 20
       coe1             coe1            coe1            |
85 | 84 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
      
  coe1             coe1            coe1            |
86 | 65, 85 | syld 45 |
. . . . . . . . . . . . . . . . . 18
      
 
 coe1             coe1            coe1            |
87 | 86 | com24 90 |
. . . . . . . . . . . . . . . . 17
      
 

 

 
 coe1       coe1            coe1            |
88 | 87 | ex 436 |
. . . . . . . . . . . . . . . 16
       

 

 
 coe1       coe1            coe1             |
89 | 88 | com14 91 |
. . . . . . . . . . . . . . 15
           
 
 coe1       coe1            coe1             |
90 | 89 | imp 431 |
. . . . . . . . . . . . . 14
 
      

 

   coe1       coe1            coe1            |
91 | 90 | com14 91 |
. . . . . . . . . . . . 13
 
 coe1          
 
       coe1            coe1            |
92 | 91 | adantr 467 |
. . . . . . . . . . . 12
    coe1       coe1    
 

 

         coe1            coe1            |
93 | 92 | com13 83 |
. . . . . . . . . . 11
          coe1       coe1              coe1            coe1            |
94 | 56, 93 | pm2.61i 168 |
. . . . . . . . . 10
  
 
  
 coe1       coe1    
 
       coe1            coe1           |
95 | 21, 94 | syl5bi 221 |
. . . . . . . . 9
  
 
 
  coe1      coe1              coe1            coe1           |
96 | 95 | imp 431 |
. . . . . . . 8
   
  
  coe1      coe1               coe1            coe1    
     |
97 | 96 | impl 625 |
. . . . . . 7
    

 
   coe1      coe1              coe1            coe1    
    |
98 | 97 | mpteq2dva 4488 |
. . . . . 6
          coe1      coe1     
        coe1            coe1                |
99 | 98 | oveq2d 6304 |
. . . . 5
          coe1      coe1     
  g        coe1            coe1           g         |
100 | | ringmnd 17782 |
. . . . . . . . 9

  |
101 | | ovex 6316 |
. . . . . . . . . 10
     |
102 | 101 | a1i 11 |
. . . . . . . . 9

      |
103 | 44 | gsumz 16614 |
. . . . . . . . 9
        g        |
104 | 100, 102,
103 | syl2anc 666 |
. . . . . . . 8

 g        |
105 | 104 | adantr 467 |
. . . . . . 7
  
 
 g        |
106 | 105 | adantr 467 |
. . . . . 6
   
  
  coe1      coe1       g        |
107 | 106 | adantr 467 |
. . . . 5
          coe1      coe1     
  g        |
108 | 20, 99, 107 | 3eqtrd 2488 |
. . . 4
          coe1      coe1     
  coe1        |
109 | 108 | ralrimiva 2801 |
. . 3
   
  
  coe1      coe1      
 coe1        |
110 | | fveq2 5863 |
. . . . 5
  coe1        coe1         |
111 | 110 | eqeq1d 2452 |
. . . 4
   coe1        coe1         |
112 | 111 | cbvralv 3018 |
. . 3
 
 coe1         coe1        |
113 | 109, 112 | sylibr 216 |
. 2
   
  
  coe1      coe1      
 coe1        |
114 | 113 | ex 436 |
1
  
 
 
  coe1      coe1       coe1         |