let fp be FinSequence of NAT ; :: thesis: ( len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) implies for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) )
defpred S1[ FinSequence of NAT ] means for fr being FinSequence of INT st len fr = len $1 holds
ex fr1 being FinSequence of INT st
( len fr1 = len $1 & ( for b being Nat st b in dom $1 holds
(($1 . b) * (fr1 . b)) + (fr . b) = (($1 . 1) * (fr1 . 1)) + (fr . 1) ) );
defpred S2[ FinSequence of NAT ] means for b, c being Nat st b in dom $1 & c in dom $1 & b <> c holds
($1 . b) gcd ($1 . c) = 1;
defpred S3[ set ] means ex f being FinSequence of NAT st
( f = $1 & ( len f >= 2 & S2[f] implies S1[f] ) );
A1: now :: thesis: for fp being FinSequence of NAT
for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let fp be FinSequence of NAT ; :: thesis: for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let d be Element of NAT ; :: thesis: ( S3[fp] implies S3[fp ^ <*d*>] )
assume A2: S3[fp] ; :: thesis: S3[fp ^ <*d*>]
set k = len fp;
set fp1 = fp ^ <*d*>;
now :: thesis: ( len (fp ^ <*d*>) >= 2 & S2[fp ^ <*d*>] implies S1[fp ^ <*d*>] )
assume that
A3: len (fp ^ <*d*>) >= 2 and
A4: S2[fp ^ <*d*>] ; :: thesis: S1[fp ^ <*d*>]
A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16;
now :: thesis: S1[fp ^ <*d*>]
per cases ( len (fp ^ <*d*>) = 2 or len (fp ^ <*d*>) > 2 ) by A3, XXREAL_0:1;
suppose A6: len (fp ^ <*d*>) = 2 ; :: thesis: S1[fp ^ <*d*>]
now :: thesis: for fr being FinSequence of INT st len fr = len (fp ^ <*d*>) holds
ex fr1 being FinSequence of INT st
( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) )
let fr be FinSequence of INT ; :: thesis: ( len fr = len (fp ^ <*d*>) implies ex fr1 being FinSequence of INT st
( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) ) )
assume len fr = len (fp ^ <*d*>) ; :: thesis: ex fr1 being FinSequence of INT st
( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) )
( 1 in dom (fp ^ <*d*>) & 2 in dom (fp ^ <*d*>) ) by A6, FINSEQ_3:25;
then ((fp ^ <*d*>) . 1) gcd ((fp ^ <*d*>) . 2) = 1 by A4;
then ((fp ^ <*d*>) . 1) gcd ((fp ^ <*d*>) . 2) divides (fr . 1) - (fr . 2) by INT_2:12;
then consider m, n being Integer such that
A7: (((fp ^ <*d*>) . 1) * m) + (((fp ^ <*d*>) . 2) * n) = (fr . 1) - (fr . 2) by Th33;
reconsider x = - m, y = n as Element of INT by INT_1:def 2;
take fr1 = <*x,y*>; :: thesis: ( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) )
thus len fr1 = len (fp ^ <*d*>) by A6, FINSEQ_1:44; :: thesis: for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
let b be Nat; :: thesis: ( b in dom (fp ^ <*d*>) implies (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) )
assume b in dom (fp ^ <*d*>) ; :: thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
then A8: b in Seg (len (fp ^ <*d*>)) by FINSEQ_1:def 3;
now :: thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
per cases ( b = 1 or b = 2 ) by A6, A8, FINSEQ_1:2, TARSKI:def 2;
suppose b = 1 ; :: thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
hence (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ; :: thesis: verum
end;
suppose A9: b = 2 ; :: thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
A10: ( fr1 . 1 = - m & fr1 . 2 = n ) by FINSEQ_1:44;
(((fp ^ <*d*>) . 2) * n) - (((fp ^ <*d*>) . 1) * (- m)) = (fr . 1) - (fr . 2) by A7;
hence (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) by A9, A10, XCMPLX_1:34; :: thesis: verum
end;
end;
end;
hence (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ; :: thesis: verum
end;
hence S1[fp ^ <*d*>] ; :: thesis: verum
end;
suppose A11: len (fp ^ <*d*>) > 2 ; :: thesis: S1[fp ^ <*d*>]
A12: S2[fp]
proof
A13: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26;
let b, c be Nat; :: thesis: ( b in dom fp & c in dom fp & b <> c implies (fp . b) gcd (fp . c) = 1 )
assume that
A14: ( b in dom fp & c in dom fp ) and
A15: b <> c ; :: thesis: (fp . b) gcd (fp . c) = 1
( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A14, FINSEQ_1:def 7;
hence (fp . b) gcd (fp . c) = 1 by A4, A14, A15, A13; :: thesis: verum
end;
A16: (len fp) + 1 > 1 + 1 by A11, FINSEQ_2:16;
then A17: len fp >= 1 + 1 by NAT_1:13;
now :: thesis: for fr2 being FinSequence of INT st len fr2 = len (fp ^ <*d*>) holds
ex fr3 being FinSequence of INT st
( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) )
let fr2 be FinSequence of INT ; :: thesis: ( len fr2 = len (fp ^ <*d*>) implies ex fr3 being FinSequence of INT st
( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) ) )
assume A18: len fr2 = len (fp ^ <*d*>) ; :: thesis: ex fr3 being FinSequence of INT st
( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) )
then consider fr being FinSequence of INT , m being Element of INT such that
A19: fr2 = fr ^ <*m*> by FINSEQ_2:19;
A20: (len fp) + 1 = (len fr) + 1 by A5, A18, A19, FINSEQ_2:16;
then consider fr1 being FinSequence of INT such that
len fr1 = len fp and
A21: for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) by A2, A16, A12, NAT_1:13;
for a being Nat st a in dom fp holds
(fp . a) gcd d = 1
proof
let a be Nat; :: thesis: ( a in dom fp implies (fp . a) gcd d = 1 )
A22: (len fp) + 1 in dom (fp ^ <*d*>) by A5, FINSEQ_5:6;
A23: ( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . ((len fp) + 1) = d ) by FINSEQ_1:26, FINSEQ_1:42;
assume A24: a in dom fp ; :: thesis: (fp . a) gcd d = 1
(len fp) + 1 > len fp by NAT_1:13;
then A25: (len fp) + 1 <> a by A24, FINSEQ_3:25;
(fp ^ <*d*>) . a = fp . a by A24, FINSEQ_1:def 7;
hence (fp . a) gcd d = 1 by A4, A24, A23, A25, A22; :: thesis: verum
end;
then (Product fp) gcd d = 1 by Th36;
then (Product fp) gcd d divides ((fr2 . ((len fp) + 1)) - ((fp . 1) * (fr1 . 1))) - (fr2 . 1) by INT_2:12;
then consider m1, n1 being Integer such that
A26: ((Product fp) * m1) + (d * n1) = ((fr2 . ((len fp) + 1)) - ((fp . 1) * (fr1 . 1))) - (fr2 . 1) by Th33;
reconsider x = - n1 as Element of INT by INT_1:def 2;
deffunc H1( Nat) -> set = ((Product (Del (fp,$1))) * m1) + (fr1 . $1);
consider s2 being FinSequence such that
A27: ( len s2 = len fp & ( for a being Nat st a in dom s2 holds
s2 . a = H1(a) ) ) from FINSEQ_1:sch 2();
A28: for a being Nat st a in dom s2 holds
s2 . a in INT
proof
let a be Nat; :: thesis: ( a in dom s2 implies s2 . a in INT )
assume A29: a in dom s2 ; :: thesis: s2 . a in INT
reconsider a = a as Element of NAT by ORDINAL1:def 12;
s2 . a = ((Product (Del (fp,a))) * m1) + (fr1 . a) by A27, A29;
hence s2 . a in INT by INT_1:def 2; :: thesis: verum
end;
A30: dom s2 = Seg (len fp) by A27, FINSEQ_1:def 3;
reconsider s2 = s2 as FinSequence of INT by A28, FINSEQ_2:12;
take fr3 = s2 ^ <*x*>; :: thesis: ( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) )
thus len fr3 = len (fp ^ <*d*>) by A5, A27, FINSEQ_2:16; :: thesis: for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
let b be Nat; :: thesis: ( b in dom (fp ^ <*d*>) implies (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) )
assume A31: b in dom (fp ^ <*d*>) ; :: thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
thus (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) :: thesis: verum
proof
A32: for c being Nat st c in Seg (len fp) holds
((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c))
proof
let c be Nat; :: thesis: ( c in Seg (len fp) implies ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c)) )
assume A33: c in Seg (len fp) ; :: thesis: ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c))
then c in dom s2 by A27, FINSEQ_1:def 3;
then A34: fr3 . c = s2 . c by FINSEQ_1:def 7
.= ((Product (Del (fp,c))) * m1) + (fr1 . c) by A27, A30, A33 ;
for n being Nat st n in dom fp holds
fp . n in REAL by XREAL_0:def 1;
then A35: fp is FinSequence of REAL by FINSEQ_2:12;
A36: c in dom fp by A33, FINSEQ_1:def 3;
then fp . c = (fp ^ <*d*>) . c by FINSEQ_1:def 7;
hence ((fp ^ <*d*>) . c) * (fr3 . c) = (((fp . c) * (Product (Del (fp,c)))) * m1) + ((fp . c) * (fr1 . c)) by A34
.= ((Product fp) * m1) + ((fp . c) * (fr1 . c)) by A36, Lm16, A35 ;
:: thesis: verum
end;
A37: 1 <= b by A31, FINSEQ_3:25;
A38: b <= (len fp) + 1 by A5, A31, FINSEQ_3:25;
now :: thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
per cases ( b <= len fp or b = (len fp) + 1 ) by A38, NAT_1:8;
suppose A39: b <= len fp ; :: thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
then 1 <= len fp by A37, XXREAL_0:2;
then A40: 1 in Seg (len fp) ;
then 1 in dom fr by A20, FINSEQ_1:def 3;
then A41: fr2 . 1 = fr . 1 by A19, FINSEQ_1:def 7;
A42: b in Seg (len fp) by A37, A39;
then A43: b in dom fp by FINSEQ_1:def 3;
b in dom fr by A20, A42, FINSEQ_1:def 3;
then A44: fr2 . b = fr . b by A19, FINSEQ_1:def 7;
thus (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((Product fp) * m1) + ((fp . b) * (fr1 . b))) + (fr2 . b) by A32, A42
.= ((Product fp) * m1) + (((fp . b) * (fr1 . b)) + (fr . b)) by A44
.= ((Product fp) * m1) + (((fp . 1) * (fr1 . 1)) + (fr . 1)) by A21, A43
.= (((Product fp) * m1) + ((fp . 1) * (fr1 . 1))) + (fr . 1)
.= (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) by A32, A40, A41 ; :: thesis: verum
end;
suppose A45: b = (len fp) + 1 ; :: thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
then A46: (fp ^ <*d*>) . b = d by FINSEQ_1:42;
A47: (fr2 . b) - (((fp . 1) * (fr1 . 1)) + (fr2 . 1)) = (d * n1) + ((Product fp) * m1) by A26, A45;
1 <= len fp by A17, XXREAL_0:2;
then 1 in Seg (len fp) ;
then (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) = (((Product fp) * m1) + ((fp . 1) * (fr1 . 1))) + (fr2 . 1) by A32
.= (fr2 . b) + (d * (- n1)) by A47 ;
hence (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) by A27, A45, A46, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
hence (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ; :: thesis: verum
end;
end;
hence S1[fp ^ <*d*>] ; :: thesis: verum
end;
end;
end;
hence S1[fp ^ <*d*>] ; :: thesis: verum
end;
hence S3[fp ^ <*d*>] ; :: thesis: verum
end;
A48: S3[ <*> NAT]
proof
take <*> NAT ; :: thesis: ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) )
thus ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) ; :: thesis: verum
end;
for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch 2(A48, A1);
 then ex f being FinSequence of NAT st
( f = fp & ( len f >= 2 & S2[f] implies S1[f] ) ) ;
hence ( len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) implies for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) ) ; :: thesis: verum