let n be Nat; :: thesis: ex p, q being Polynomial of INT.Ring st
( degree p > 0 & degree q > 0 & ( for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i ) )
( rng (primesFinS (n + 1)) c= INT & INT = the carrier of INT.Ring ) by VALUED_0:def 5;
then reconsider z = primesFinS (n + 1) as FinSequence of INT.Ring by FINSEQ_1:def 4;
take p = (1_. INT.Ring) + (~ (Product (rpoly (((len z) |-> 1),z)))); :: thesis: ex q being Polynomial of INT.Ring st
( degree p > 0 & degree q > 0 & ( for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i ) )
take q = <%(0. INT.Ring),(1. INT.Ring)%>; :: thesis: ( degree p > 0 & degree q > 0 & ( for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i ) )
A1: len z = n + 1 by NUMBER13:def 1;
A2: Sum ((len z) |-> 1) = 1 * (len z) by RVSUM_1:80;
deg (~ (Product (rpoly (((len z) |-> 1),z)))) = n + 1 by A1, A2, Th49;
then A3: (len (~ (Product (rpoly (((len z) |-> 1),z))))) - 1 = n + 1 by HURWITZ:def 2;
A4: len (1_. INT.Ring) = 1 by POLYNOM4:4;
len (1_. INT.Ring) <> len (~ (Product (rpoly (((len z) |-> 1),z)))) by A3, A4;
then len p = max ((len (1_. INT.Ring)),(len (~ (Product (rpoly (((len z) |-> 1),z)))))) by POLYNOM4:7;
then deg p = ((n + 1) + 1) - 1 by A3, A4, HURWITZ:def 2;
hence degree p > 0 ; :: thesis: ( degree q > 0 & ( for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i ) )
len q = 2 by POLYNOM5:40;
then degree q = 2 - 1 by HURWITZ:def 2;
hence degree q > 0 ; :: thesis: for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i
let i be Nat; :: thesis: ( i <= n implies eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i )
assume A5: i <= n ; :: thesis: eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i
A6: eval (q,(In ((primenumber i),INT.Ring))) = (0. INT.Ring) + ((1. INT.Ring) * (In ((primenumber i),INT.Ring))) by POLYNOM5:44
.= In ((primenumber i),INT.Ring) ;
A7: eval ((1_. INT.Ring),(In ((primenumber i),INT.Ring))) = 1. INT.Ring by POLYNOM4:18;
A8: i < n + 1 by A5, NAT_1:13;
then A9: In ((primenumber i),INT.Ring) = z . (i + 1) by NUMBER13:def 1;
A10: len ((len z) |-> 1) = len z ;
( 1 <= i + 1 & i + 1 <= n + 1 ) by A8, NAT_1:11, NAT_1:13;
then A11: ( i + 1 in dom z & dom z = dom ((len z) |-> 1) & i + 1 in Seg (len z) ) by A1, A10, FINSEQ_3:25, FINSEQ_3:29;
then ( ((len z) |-> 1) . (i + 1) = 1 & z /. (i + 1) = z . (i + 1) ) by FINSEQ_2:57, PARTFUN1:def 6;
then 0. INT.Ring = eval ((~ (Product (rpoly (((len z) |-> 1),z)))),(In ((primenumber i),INT.Ring))) by A11, Th51, A9, POLYNOM5:def 7;
then eval (p,(In ((primenumber i),INT.Ring))) = (1. INT.Ring) + (0. INT.Ring) by A7, POLYNOM4:19
.= 1. INT.Ring ;
hence eval ((p *' q),(In ((primenumber i),INT.Ring))) = (1. INT.Ring) * (In ((primenumber i),INT.Ring)) by A6, POLYNOM4:24
.= primenumber i ;
:: thesis: verum