:: The Chinese Remainder Theorem
:: by Andrzej Kondracki
::
:: Received December 30, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, INT_1, RAT_1, NEWTON, RELAT_1, ARYTM_1, ARYTM_3,
XXREAL_0, CARD_1, PREPOWER, INT_2, COMPLEX1, SUBSET_1, FINSEQ_1, FUNCT_1,
XBOOLE_0, ORDINAL4, TARSKI, CARD_3, FINSEQ_3, REAL_1, SQUARE_1, ORDINAL1,
XCMPLX_0, VALUED_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, NUMBERS, XCMPLX_0,
XREAL_0, INT_1, REAL_1, NAT_1, NAT_D, RAT_1, INT_2, XXREAL_0, VALUED_0,
PREPOWER, SQUARE_1, FUNCT_1, FINSEQ_1, FINSEQ_3, RVSUM_1, FINSEQ_4,
NEWTON, TREES_4;
constructors REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2, FINSEQ_3, FINSEQ_4,
FINSOP_1, RVSUM_1, NEWTON, PREPOWER, TREES_4, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0,
XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1, FINSEQ_1, NEWTON, VALUED_0,
CARD_1, RVSUM_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FINSEQ_1, TARSKI;
equalities FINSEQ_1, SQUARE_1, RVSUM_1;
expansions FINSEQ_1, TARSKI, INT_1;
theorems TARSKI, ABSVALUE, INT_1, NAT_1, INT_2, RAT_1, NEWTON, PREPOWER,
SQUARE_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_1, RVSUM_1, PRE_FF, CARD_4,
FINSEQ_3, FINSEQ_5, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, CARD_1,
XXREAL_0, ORDINAL1, FINSOP_1, NAT_D, XREAL_0, RELAT_1, VALUED_0;
schemes NAT_1, FINSEQ_1, FINSEQ_2;
begin :: PRELIMINARIES
reserve x,y,z for Real,
a,b,c,d,e,f,g,h for Nat,
k,l,m,n,m1,n1,m2,n2 for Integer,
q for Rational;
theorem Th1:
for x being Complex holds x|^2=x*x & (-x)|^2=x|^2
proof
let x be Complex;
A1: (-x)|^1=-x;
A2: x=x|^1;
then x|^(1+1)=x*x by NEWTON:8;
then x|^2=(-x)*(-x) .=(-x)|^(1+1) by A1,NEWTON:8;
hence thesis by A2,NEWTON:8;
end;
theorem Th2:
for a being Nat holds (-x)|^(2*a)=x|^(2*a) & (-x)|^(2*a+1)=-(x|^( 2*a+1))
proof
let a be Nat;
A1: (-x)|^(2*a)=((-x)|^2)|^a by NEWTON:9
.=(x|^2)|^a by Th1
.=x|^(2*a) by NEWTON:9;
(-x)|^(2*a+1)=((-x)|^(2*a))*(-x) by NEWTON:6
.=-(x|^(2*a))*x by A1
.=-(x|^(2*a+1)) by NEWTON:6;
hence thesis by A1;
end;
theorem Th3:
x>=0 & y>=0 & d>0 & x|^d=y|^d implies x=y
proof
assume that
A1: x>=0 and
A2: y>=0 and
A3: d>0 and
A4: x|^d=y|^d;
A5: d>=1 by A3,NAT_1:14;
then x = d -Root (x |^ d) by A1,PREPOWER:19
.= y by A2,A4,A5,PREPOWER:19;
hence thesis;
end;
Lm1: (x>=0 iff x+y>=y) & (x>0 iff x+y>y) & (x>=0 iff y>=y-x) & (x>0 iff y>y-x)
proof
A1: x>=0 iff x+y>=0 qua Nat+y by XREAL_1:6;
hence x>=0 iff x+y>=y;
A2: x>0 iff x+y>0 qua Nat+y by XREAL_1:6;
hence x>0 iff x+y>y;
thus x>=0 iff y>=y-x by A1,XREAL_1:20;
thus thesis by A2,XREAL_1:19;
end;
Lm2: x>=0 & y>=z implies x+y>=z & y>=z-x
proof
assume x>=0 & y>=z;
then x+y>=z+(0 qua Nat) by XREAL_1:7;
hence thesis by XREAL_1:20;
end;
Lm3: (x>=0 & y>z or x>0 & y>=z) implies x+y>z & y>z-x
proof
assume x>=0 & y>z or x>0 & y>=z;
then x+y>z+(0 qua Nat) by XREAL_1:8;
hence thesis by XREAL_1:19;
end;
registration
let k be Integer, a be natural Number;
cluster k |^ a -> integer;
coherence
proof
A1: a is Nat by TARSKI:1;
defpred Q[Nat] means k|^$1 is Integer;
A2: for a st Q[a] holds Q[a+1]
proof
let a;
assume k|^a is Integer;
then reconsider b=k|^a as Integer;
k|^(a+1)=k*b by NEWTON:6;
hence thesis;
end;
A3: Q[0] by NEWTON:4;
for a holds Q[a] from NAT_1:sch 2(A3,A2);
hence thesis by A1;
end;
end;
Lm4: for a ex b st a=2*b or a=2*b+1
proof
let a;
set b=a div 2, d=a mod 2;
a=2*b+d by NAT_D:2;
then a=2*b+(0 qua Nat) or a=2*b+1 by NAT_1:23,NAT_D:1;
hence thesis;
end;
theorem Th4:
k divides m & k divides n implies k divides m+n
proof
assume that
A1: k divides m and
A2: k divides n;
consider m1 such that
A3: m=k*m1 by A1;
consider n1 such that
A4: n=k*n1 by A2;
m+n=k*(m1+n1) by A3,A4;
hence thesis;
end;
theorem Th5:
k divides m & k divides n implies k divides m*m1+n*n1
proof
assume k divides m & k divides n;
then k divides m*m1 & k divides n*n1 by INT_2:2;
hence thesis by Th4;
end;
theorem Th6:
m gcd n = 1 & k gcd n = 1 implies m*k gcd n = 1
proof
assume (m gcd n)=1 & (k gcd n)=1;
then m,n are_coprime & k,n are_coprime by INT_2:def 3;
then m*k,n are_coprime by INT_2:26;
hence thesis by INT_2:def 3;
end;
theorem
a gcd b=1 & c gcd b=1 implies a*c gcd b=1 by Th6;
theorem Th8:
0 gcd m = |.m.| & 1 gcd m = 1
proof
A1: m gcd 1=|.m.| gcd |.1.| by INT_2:34
.=|.m.| gcd 1 by ABSVALUE:def 1
.=1 by NEWTON:51;
m gcd 0=|.m.| gcd |.0 qua Nat.| by INT_2:34
.=|.m.| gcd 0 by ABSVALUE:2
.=|.m.| by NEWTON:52;
hence thesis by A1;
end;
theorem Th9:
1,k are_coprime
proof
1 gcd k = 1 by Th8;
hence thesis by INT_2:def 3;
end;
theorem Th10:
k,l are_coprime implies k|^a,l are_coprime
proof
defpred P[Nat] means k|^$1,l are_coprime;
assume
A1: k,l are_coprime;
A2: for a st P[a] holds P[a+1]
proof
let a;
assume k|^a,l are_coprime;
then k*(k|^a),l are_coprime by A1,INT_2:26;
hence thesis by NEWTON:6;
end;
k|^0=1 by NEWTON:4;
then
A3: P[0] by Th9;
for a holds P[a] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem Th11:
k,l are_coprime implies k|^a,l|^b are_coprime
proof
assume k,l are_coprime;
then k|^a,l are_coprime by Th10;
hence thesis by Th10;
end;
theorem Th12:
k gcd l = 1 implies k gcd l|^b = 1 & k|^a gcd l|^b = 1
proof
assume k gcd l=1;
then k,l are_coprime by INT_2:def 3;
then k,l|^b are_coprime & k|^a,l|^b are_coprime by Th10,Th11;
hence thesis by INT_2:def 3;
end;
theorem
|.m.| divides k iff m divides k
proof
A1: now
assume m divides k;
then consider l such that
A2: m*l=k;
now
per cases;
suppose
m>=0;
then |.m.|*l=k by A2,ABSVALUE:def 1;
hence (|.m.|) divides k;
end;
suppose
m<0;
then |.m.|*(-l)=(-m)*(-l) by ABSVALUE:def 1
.=k by A2;
hence |.m.| divides k;
end;
end;
hence |.m.| divides k;
end;
now
assume |.m.| divides k;
then consider l such that
A3: |.m.|*l=k;
now
per cases;
suppose
m>=0;
then m*l=k by A3,ABSVALUE:def 1;
hence m divides k;
end;
suppose
m<0;
then k=(-m)*l by A3,ABSVALUE:def 1
.=m*(-l);
hence m divides k;
end;
end;
hence m divides k;
end;
hence thesis by A1;
end;
theorem Th14:
a divides b implies (a|^c) divides (b|^c)
proof
assume a divides b;
then consider d be Nat such that
A1: a*d=b by NAT_D:def 3;
b|^c =(a|^c)*(d|^c) by A1,NEWTON:7;
hence thesis;
end;
theorem Th15:
a divides 1 implies a=1
proof
assume
A1: a divides 1;
then a divides 1+1 by NAT_D:8;
hence thesis by A1,NEWTON:39;
end;
theorem
d divides a & a gcd b = 1 implies d gcd b = 1 by Th15,NEWTON:57;
Lm5: a<>0 implies (a divides b iff b/a is Element of NAT)
proof
assume
A1: a<>0;
A2: now
assume a divides b;
then consider d be Nat such that
A3: b=a*d by NAT_D:def 3;
reconsider d as Element of NAT by ORDINAL1:def 12;
b=a*d by A3;
hence b/a is Element of NAT by A1,XCMPLX_1:89;
end;
now
assume b/a is Element of NAT;
then reconsider d=b/a as Element of NAT;
b=a*d by A1,XCMPLX_1:87;
hence a divides b;
end;
hence thesis by A2;
end;
theorem Th17:
k<>0 implies (k divides l iff l/k is Integer)
proof
assume
A1: k<>0;
hence k divides l implies l/k is Integer by XCMPLX_1:89;
assume l/k is Integer;
then reconsider m=l/k as Integer;
l=k*m by A1,XCMPLX_1:87;
hence k divides l;
end;
Lm6: b<>0 & a*k=b implies k is Element of NAT
proof
assume that
A1: b<>0 and
A2: a*k=b;
A3: a divides (b qua Integer) by A2;
A4: a<>0 by A1,A2;
then k=b/a by A2,XCMPLX_1:89;
hence thesis by A3,A4,Lm5;
end;
Lm7: a+b<=c implies a<=c & b<=c
proof
A1: a<=a+b & b<=a+b by NAT_1:11;
assume a+b<=c;
hence thesis by A1,XXREAL_0:2;
end;
theorem
a<=b-c implies a<=b & c <=b
proof
assume a<=b-c;
then a+c <=b by XREAL_1:19;
hence thesis by Lm7;
end;
Lm8: k<m iff k<=m-1
proof
A1: now
assume k<=m-1;
then
A2: k+1<=m by XREAL_1:19;
k<k+1 by XREAL_1:29;
hence k<m by A2,XXREAL_0:2;
end;
now
assume k<m;
then k+1<=m by INT_1:7;
hence k<=m-1 by XREAL_1:19;
end;
hence thesis by A1;
end;
Lm9: k<m+1 iff k<=m
proof
k<m+1 iff k-1<m by XREAL_1:19;
hence thesis by Lm8;
end;
reserve fs,fs1,fs2,fs3 for FinSequence;
reserve D for non empty set,
v,v1,v2,v3 for object,
fp for FinSequence of NAT,
fr,fr1,fr2 for FinSequence of INT,
ft for FinSequence of REAL;
registration
let fr be integer-valued FinSequence;
cluster Product fr -> integer;
coherence
proof
A0: fr is FinSequence of INT by FINSEQ_1:102;
defpred P[FinSequence of INT] means Product $1 is Integer;
A1: now
let s be (FinSequence of INT),m be Element of INT;
reconsider k=m as Integer;
assume P[s];
then reconsider pis=Product s as Integer;
Product(s^<*m*>)=pis*k by RVSUM_1:96;
hence P[s^<*m*>];
end;
A2: P[<*>INT] by RVSUM_1:94;
for fr1 holds P[fr1] from FINSEQ_2:sch 2(A2,A1);
hence thesis by A0;
end;
end;
definition
let fp;
redefine func Sum(fp) -> Element of NAT; :: redefines Sum (RVSUM_1, definition)
coherence
proof
defpred P[FinSequence of NAT] means Sum $1 is Element of NAT;
A1: now
let fp;
let a be Element of NAT;
assume P[fp];
then reconsider sp=Sum(fp) as Element of NAT;
Sum(fp^<*a*>)=sp+a by RVSUM_1:74;
hence P[fp^<*a*>];
end;
A2: P[<*>NAT] by RVSUM_1:72;
for fp holds P[fp] from FINSEQ_2:sch 2(A2,A1);
hence thesis;
end;
end;
registration
let fp be natural-valued FinSequence;
cluster Sum fp -> natural;
coherence
proof
rng fp c= NAT by VALUED_0:def 6;
then reconsider fp as FinSequence of NAT by FINSEQ_1:def 4;
Sum fp in NAT;
hence thesis;
end;
end;
definition
let fp;
redefine func Product fp -> Element of NAT; :: redefines Product (RVSUM_1, definition)
coherence
proof
defpred P[FinSequence of NAT] means Product $1 is Element of NAT;
A1: now
let fp;
let a be Element of NAT;
assume P[fp];
then reconsider sp=Product(fp) as Element of NAT;
Product(fp^<*a*>)=sp*a by RVSUM_1:96;
hence P[fp^<*a*>];
end;
A2: P[<*>NAT] by RVSUM_1:94;
for fp holds P[fp] from FINSEQ_2:sch 2(A2,A1);
hence thesis;
end;
end;
registration
let fp be natural-valued FinSequence;
cluster Product fp -> natural;
coherence
proof
rng fp c= NAT by VALUED_0:def 6;
then reconsider fp as FinSequence of NAT by FINSEQ_1:def 4;
Product fp in NAT;
hence thesis;
end;
end;
Lm10: a in dom fs implies ex fs1,fs2 st fs=fs1^<*fs.a*>^fs2 & len fs1=a-1 &
len fs2=len fs -a
proof
assume
A1: a in dom fs;
then a>=1 & a<=len fs by FINSEQ_3:25;
then reconsider b=len fs-a, d=a-1 as Element of NAT by INT_1:5;
len fs=a+b;
then consider fs3,fs2 such that
A2: len fs3=a and
A3: len fs2=b and
A4: fs=fs3^fs2 by FINSEQ_2:22;
a=d+1;
then consider fs1,v such that
A5: fs3=fs1^<*v*> by A2,FINSEQ_2:18;
A6: len fs1 + 1=d+1 by A2,A5,FINSEQ_2:16;
a<>0 by A1,FINSEQ_3:25;
then a in dom fs3 by A2,CARD_1:27,FINSEQ_5:6;
then fs3.a=fs.a by A4,FINSEQ_1:def 7;
then fs.a=v by A5,A6,FINSEQ_1:42;
hence thesis by A3,A4,A5,A6;
end;
definition
let a be Nat,fs;
redefine func Del (fs,a) means :: redefines Del (FINSEQ_3, definition)
:Def1:
it = fs if not a in dom fs otherwise
len it + 1 = len fs &
for b holds (b<a implies it.b = fs.b) & (b>=a implies it.b = fs.(b+1));
compatibility
proof
let IT be FinSequence;
thus not a in dom fs implies (IT = Del(fs,a) iff IT = fs) by FINSEQ_3:104;
assume
A1: a in dom fs;
hereby
assume
A2: IT = Del(fs,a);
then
A3: ex m be Nat st len fs = m + 1 & len IT = m by A1,FINSEQ_3:104;
hence len IT + 1 = len fs;
let b;
thus b<a implies IT.b=fs.b by A2,FINSEQ_3:110;
assume
A4: b>=a;
per cases;
suppose
b<=len IT;
hence IT.b=fs.(b+1) by A1,A2,A3,A4,FINSEQ_3:111;
end;
suppose
A5: b > len IT;
then not b in dom IT by FINSEQ_3:25;
then
A6: IT.b = {} by FUNCT_1:def 2;
b+1 > len IT + 1 by A5,XREAL_1:6;
then not b+1 in dom fs by A3,FINSEQ_3:25;
hence IT.b=fs.(b+1) by A6,FUNCT_1:def 2;
end;
end;
assume that
A7: len IT + 1 = len fs and
A8: for b holds (b<a implies IT.b=fs.b) & (b>=a implies IT.b=fs.(b+1) );
A9: for k be Nat st 1 <= k & k <= len IT holds IT.k=(Del(fs,a)).k
proof
let k be Nat;
assume that
1 <= k and
A10: k <= len IT;
reconsider k as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A11: k < a;
then IT.k=fs.k by A8;
hence thesis by A11,FINSEQ_3:110;
end;
suppose
A12: k >= a;
then IT.k=fs.(k+1) by A8;
hence thesis by A1,A7,A10,A12,FINSEQ_3:111;
end;
end;
ex m be Nat st len fs = m + 1 & len Del(fs,a) = m by A1,FINSEQ_3:104;
hence thesis by A7,A9;
end;
correctness;
end;
Lm11: a in dom fs & fs=fs1^<*v*>^fs2 & len fs1=a-1 implies Del(fs,a)=fs1^fs2
proof
assume that
A1: a in dom fs and
A2: fs=fs1^<*v*>^fs2 and
A3: len fs1=a-1;
A4: len(Del(fs,a))+1=len fs by A1,Def1;
len fs=len(fs1^<*v*>)+len fs2 by A2,FINSEQ_1:22
.=len fs1 +1 +len fs2 by FINSEQ_2:16
.=a +len fs2 by A3;
then len(Del(fs,a))=len fs2 +len fs1 by A3,A4;
then
A5: len(fs1^fs2)=len(Del(fs,a)) by FINSEQ_1:22;
A6: len<*v*>=1 by FINSEQ_1:39;
A7: fs=fs1^(<*v*>^fs2) by A2,FINSEQ_1:32;
then len fs=(a-1) + len(<*v*>^fs2) by A3,FINSEQ_1:22;
then
A8: len(<*v*>^fs2)=len fs -(a-1);
now
let e be Nat;
assume that
A9: 1<=e and
A10: e<=len Del(fs,a);
now
per cases;
suppose
A11: e<a;
then e<=a-1 by Lm8;
then
A12: e in dom fs1 by A3,A9,FINSEQ_3:25;
hence (fs1^fs2).e=fs1.e by FINSEQ_1:def 7
.=fs.e by A7,A12,FINSEQ_1:def 7
.=(Del(fs,a)).e by A1,A11,Def1;
end;
suppose
A13: e>=a;
then
A14: e>a-1 by Lm8;
then
A15: e+1>a by XREAL_1:19;
then e+1-a>0 by XREAL_1:50;
then
A16: e+1-a+1>0 qua Nat+1 by XREAL_1:6;
A17: e+1>a-1 by A15,XREAL_1:146,XXREAL_0:2;
then e+1-(a-1)>0 by XREAL_1:50;
then reconsider f=e+1-(a-1) as Element of NAT by INT_1:3;
A18: e+1<=len fs by A4,A10,XREAL_1:6;
then
A19: e+1-(a-1)<=len(<*v*>^fs2) by A8,XREAL_1:9;
thus (fs1^fs2).e=fs2.(e-len fs1) by A3,A5,A10,A14,FINSEQ_1:24
.=fs2.(f-1) by A3
.=(<*v*>^fs2).f by A6,A16,A19,FINSEQ_1:24
.=(fs1^(<*v*>^fs2)).(e+1) by A3,A7,A17,A18,FINSEQ_1:24
.=(Del(fs,a)).e by A1,A7,A13,Def1;
end;
end;
hence (fs1^fs2).e=(Del(fs,a)).e;
end;
hence thesis by A5;
end;
Lm12: dom Del(fs,a) c= dom fs
proof
now
assume
A1: a in dom fs;
dom fs=Seg len fs by FINSEQ_1:def 3
.= Seg(len(Del(fs,a))+1) by A1,Def1
.= Seg len(Del(fs,a)) \/ {len(Del(fs,a))+1} by FINSEQ_1:9
.= dom(Del(fs,a)) \/ {len(Del(fs,a))+1} by FINSEQ_1:def 3;
hence thesis by XBOOLE_1:7;
end;
hence thesis by Def1;
end;
definition
let D;
let a be Nat;
let fs be D-valued FinSequence;
redefine func Del(fs,a) -> FinSequence of D; :: redefines Del (WSIERP_1, redefinition) → Del (FINSEQ_3, definition)
coherence
proof
rng fs c= D & rng Del(fs,a) c= rng fs by FINSEQ_3:106,RELAT_1:def 19;
hence rng Del(fs,a) c= D;
end;
end;
definition
let D;
let D1 be non empty Subset of D;
let a be Nat;
let fs be D1-valued FinSequence;
redefine func Del(fs,a) -> FinSequence of D1; :: redefines Del (WSIERP_1, redefinition) → Del (FINSEQ_3, definition)
coherence
proof
thus rng(Del(fs,a)) c= D1 by FINSEQ_1:def 4;
end;
end;
Lm13: (a<=len fs1 implies Del(fs1^fs2,a)=Del(fs1,a)^fs2) & (a>=1 implies Del(
fs1^fs2,len fs1 +a)=fs1^Del(fs2,a))
proof
set f=fs1^fs2;
A1: len f=len fs1 + len fs2 by FINSEQ_1:22;
A2: now
set f2=fs1^Del(fs2,a);
set f1= Del(f,len fs1 + a);
assume
A3: a>=1;
now
per cases;
suppose
A4: a>len fs2;
then
A5: not a in dom fs2 by FINSEQ_3:25;
len fs1 + a>len f by A1,A4,XREAL_1:6;
then not (len fs1 + a) in dom f by FINSEQ_3:25;
hence f1=fs1^fs2 by Def1
.=f2 by A5,Def1;
end;
suppose
A6: a<=len fs2;
then
A7: a in dom fs2 by A3,FINSEQ_3:25;
a-1>=0 by A3,XREAL_1:48;
then
A8: len fs1 +(a-1)>=len fs1 by Lm1;
A9: len fs1 + a>=1 by A3,NAT_1:12;
len fs1 + a <= len f by A1,A6,XREAL_1:6;
then
A10: (len fs1 + a) in dom f by A9,FINSEQ_3:25;
then consider g1,g2 being FinSequence such that
A11: f=g1^<*f.(len fs1 +a)*>^g2 and
A12: len g1=len fs1 +a -1 and
len g2=len f -(len fs1 +a) by Lm10;
A13: f1=g1^g2 by A10,A11,A12,Lm11;
f=g1^(<*f.(len fs1 +a)*>^g2) by A11,FINSEQ_1:32;
then consider t being FinSequence such that
A14: fs1^t=g1 by A12,A8,FINSEQ_1:47;
fs1^(t^<*f.(len fs1 +a)*>^g2)=fs1^(t^<*f.(len fs1 +a)*>)^g2 by
FINSEQ_1:32
.=f by A11,A14,FINSEQ_1:32;
then
A15: fs2=t^<*f.(len fs1 +a)*>^g2 by FINSEQ_1:33;
len fs1 +(a-1)=len fs1 +len t by A12,A14,FINSEQ_1:22;
then Del(fs2,a)=t^g2 by A7,A15,Lm11;
hence f1=f2 by A13,A14,FINSEQ_1:32;
end;
end;
hence f1=f2;
end;
now
set f3=<*f.a*>;
set f2=((Del(fs1,a))^fs2);
set f1= Del(f,a);
assume
A16: a<=len fs1;
len fs1<=len f by A1,NAT_1:11;
then
A17: a<=len f by A16,XXREAL_0:2;
now
per cases;
suppose
A18: a<1;
then
A19: not a in dom fs1 by FINSEQ_3:25;
not a in dom f by A18,FINSEQ_3:25;
hence f1=f by Def1
.=f2 by A19,Def1;
end;
suppose
A20: a>=1;
then
A21: a in dom f by A17,FINSEQ_3:25;
then consider g1,g2 being FinSequence such that
A22: f=g1^f3^g2 and
A23: len g1=a-1 and
len g2=len f -a by Lm10;
len(g1^f3)=a-1+1 by A23,FINSEQ_2:16
.=a;
then consider t being FinSequence such that
A24: fs1=g1^f3^t by A16,A22,FINSEQ_1:47;
g1^f3^g2=g1^f3^(t^fs2) by A22,A24,FINSEQ_1:32;
then
A25: g2=t^fs2 by FINSEQ_1:33;
a in dom fs1 by A16,A20,FINSEQ_3:25;
then
A26: Del(fs1,a)=g1^t by A23,A24,Lm11;
thus f1=g1^g2 by A21,A22,A23,Lm11
.=f2 by A26,A25,FINSEQ_1:32;
end;
end;
hence f1=f2;
end;
hence thesis by A2;
end;
Lm14: Del(<*v*>^fs,1)=fs & Del(fs^<*v*>,len fs + 1)=fs
proof
A1: len <*v*>=1 by FINSEQ_1:39;
then 1 in dom <*v*> by FINSEQ_3:25;
then len(Del(<*v*>,1))+1=1 by A1,Def1;
then
A2: Del(<*v*>,1)={};
1<=len <*v*> & {}^fs=fs by FINSEQ_1:34,39;
hence Del(<*v*>^fs,1)=fs by A2,Lm13;
fs^{}=fs by FINSEQ_1:34;
hence thesis by A2,Lm13;
end;
theorem
Del(<*v1*>,1) = {} & Del(<*v1,v2*>,1) = <*v2*> & Del(<*v1,v2*>,2) = <*
v1 *> & Del(<*v1,v2,v3*>,1) = <*v2,v3*> & Del(<*v1,v2,v3*>,2) = <*v1,v3*> & Del
(<*v1,v2,v3*>,3) = <*v1,v2*>
proof
thus Del(<*v1*>,1)=Del(<*v1*>^{},1) by FINSEQ_1:34
.={} by Lm14;
thus Del(<*v1,v2*>,1)=<*v2*> by Lm14;
len <*v1*> =1 by FINSEQ_1:39;
hence
A1: Del(<*v1,v2*>,2)=Del(<*v1*>^<*v2*>,len <*v1*> +1) .=<*v1*> by Lm14;
thus Del(<*v1,v2,v3*>,1)=Del(<*v1*>^<*v2,v3*>,1) by FINSEQ_1:43
.=<*v2,v3*> by Lm14;
A2: len<*v1,v2*>=2 by FINSEQ_1:44;
hence Del(<*v1,v2,v3*>,2)=<*v1,v3*> by A1,Lm13;
len <*v1,v2*>+1=3 by A2;
hence thesis by Lm14;
end;
Lm15: 1<=len fs implies fs=<*fs.1*>^Del(fs,1) & fs=Del(fs,len fs)^<*fs.(len fs
)*>
proof
set fs1=<*fs.1*>^Del(fs,1);
set fs2=Del(fs,len fs)^<*fs.(len fs)*>;
A1: len <*fs.1*>=1 by FINSEQ_1:39;
assume
A2: 1<=len fs;
then
A3: len fs in dom fs by FINSEQ_3:25;
A4: 1 in dom fs by A2,FINSEQ_3:25;
then
A5: len fs=len <*fs.1*> + len Del(fs,1) by A1,Def1
.=len fs1 by FINSEQ_1:22;
for b be Nat st 1<=b & b<=len fs holds fs.b=fs1.b
proof
let b be Nat;
assume that
A6: 1<=b and
A7: b<=len fs;
now
per cases by A6,XXREAL_0:1;
suppose
A8: b=1;
1 in dom <*fs.1*> by A1,FINSEQ_3:25;
hence fs1.b=<*fs.1*>.1 by A8,FINSEQ_1:def 7
.=fs.b by A8;
end;
suppose
A9: b>1;
then
A10: b-1>0 by XREAL_1:50;
then reconsider e=b-1 as Element of NAT by INT_1:3;
A11: e>=1 by A10,NAT_1:14;
thus fs1.b=(Del(fs,1)).e by A1,A5,A7,A9,FINSEQ_1:24
.=fs.(e+1) by A4,A11,Def1
.=fs.b;
end;
end;
hence thesis;
end;
hence fs1=fs by A5;
len <*fs.(len fs)*>=1 by FINSEQ_1:39;
then
A12: len fs=len <*fs.(len fs)*> + len Del(fs,len fs) by A3,Def1
.=len fs2 by FINSEQ_1:22;
A13: len(Del(fs,len fs))+1=len fs by A3,Def1;
then
A14: len Del(fs,len fs)=len fs -1;
for b be Nat st 1<=b & b<=len fs holds fs.b=fs2.b
proof
let b be Nat;
assume that
A15: 1<=b and
A16: b<=len fs;
now
per cases by A16,XXREAL_0:1;
suppose
A17: b=len fs;
reconsider e=b-(b-1) as Element of NAT;
thus fs2.b=<*fs.(len fs)*>.e by A13,A12,A17,FINSEQ_1:24,XREAL_1:146
.=fs.b by A17;
end;
suppose
A18: b<len fs;
then b+1 <= len fs by NAT_1:13;
then b <= len(Del(fs,len fs)) by A14,XREAL_1:19;
then b in dom Del(fs,len fs) by A15,FINSEQ_3:25;
hence fs2.b=(Del(fs,len fs)).b by FINSEQ_1:def 7
.=fs.b by A3,A18,Def1;
end;
end;
hence thesis;
end;
hence thesis by A12;
end;
Lm16: a in dom ft implies Product Del(ft,a)*(ft.a)=Product(ft)
proof
defpred P[Nat] means $1 in dom ft implies (ft.$1)*Product(Del(ft,$1))=
Product(ft);
A1: for a st P[a] holds P[a+1]
proof
let a such that
P[a];
now
per cases;
suppose
A2: a=0;
thus P[a+1]
proof
assume a+1 in dom ft;
then a + 1 <= len ft by FINSEQ_3:25;
then <*ft.1*>^Del(ft,1)=ft by A2,Lm15;
then Product(ft)=Product(<*ft.1*>)*Product Del(ft,1) by RVSUM_1:97
.=(ft.1)*Product Del(ft,1);
hence thesis by A2;
end;
end;
suppose
a>0 & a<len ft;
then a+1>=1 & a+1<=len ft by NAT_1:11,13;
then
A3: (a+1) in dom ft by FINSEQ_3:25;
then consider fs1,fs2 such that
A4: ft=fs1^<*ft.(a+1)*>^fs2 and
A5: len fs1=(a+1)-1 and
len fs2=len ft-(a+1) by Lm10;
A6: Del(ft,a+1)=fs1^fs2 by A3,A4,A5,Lm11;
reconsider fs2 as FinSequence of REAL by A4,FINSEQ_1:36;
reconsider fs1 as FinSequence of REAL by A6,FINSEQ_1:36;
Product(ft)=Product(fs1^<*ft.(a+1)*>)*Product(fs2) by A4,RVSUM_1:97
.=Product(fs1)*Product(<*ft.(a+1)*>)*Product(fs2) by RVSUM_1:97
.=(ft.(a+1))*Product(fs1)*Product(fs2)
.=(ft.(a+1))*(Product(fs1)*Product(fs2));
hence thesis by A6,RVSUM_1:97;
end;
suppose
a>=len ft;
then len ft < a+1 by NAT_1:13;
hence thesis by FINSEQ_3:25;
end;
end;
hence thesis;
end;
A7: P[0] by FINSEQ_3:25;
for a holds P[a] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem
a in dom ft implies Sum Del(ft,a)+(ft.a)=Sum(ft)
proof
defpred P[Nat] means $1 in dom ft implies (ft.$1)+Sum Del(ft,$1)=Sum(ft);
A1: for a st P[a] holds P[a+1]
proof
let a such that
P[a];
now
per cases;
suppose
A2: a=0;
thus P[a+1]
proof
reconsider ft1 = ft.1 as Element of REAL by XREAL_0:def 1;
assume a+1 in dom ft;
then a+1<=len ft by FINSEQ_3:25;
then <*ft.1*>^Del(ft,1)=ft by A2,Lm15;
then Sum(ft)=Sum(<*ft1*>)+Sum Del(ft,1) by RVSUM_1:75
.=(ft.1)+Sum Del(ft,1) by FINSOP_1:11;
hence thesis by A2;
end;
end;
suppose
a>0 & a<len ft;
then a+1>=1 & a+1<=len ft by NAT_1:11,13;
then
A3: (a+1) in dom ft by FINSEQ_3:25;
then consider fs1,fs2 such that
A4: ft=fs1^<*ft.(a+1)*>^fs2 and
A5: len fs1=(a+1)-1 and
len fs2=len ft-(a+1) by Lm10;
reconsider fta1 = ft.(a+1) as Element of REAL by XREAL_0:def 1;
A6: Del(ft,a+1)=fs1^fs2 by A3,A4,A5,Lm11;
reconsider fs2 as FinSequence of REAL by A4,FINSEQ_1:36;
reconsider fs1 as FinSequence of REAL by A6,FINSEQ_1:36;
Sum(ft)=Sum(fs1^<*ft.(a+1)*>)+Sum(fs2) by A4,RVSUM_1:75
.=Sum(fs1)+Sum(<*fta1*>)+Sum(fs2) by RVSUM_1:75
.=fta1+Sum(fs1)+Sum(fs2) by FINSOP_1:11
.=(ft.(a+1))+(Sum(fs1)+Sum(fs2));
hence thesis by A6,RVSUM_1:75;
end;
suppose
a>=len ft;
then a+1 > len ft by NAT_1:13;
hence thesis by FINSEQ_3:25;
end;
end;
hence thesis;
end;
A7: P[0] by FINSEQ_3:25;
for a holds P[a] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem
a in dom fp implies Product(fp)/fp.a is Element of NAT
proof
assume a in dom fp;
then consider fs1,fs2 such that
A1: fp=fs1^<*fp.a*>^fs2 and
len fs1=a-1 and
len fs2=len fp -a by Lm10;
per cases;
suppose
A2: fp.a<>0;
reconsider fs2 as FinSequence of NAT by A1,FINSEQ_1:36;
fs1^<*fp.a*> is FinSequence of NAT by A1,FINSEQ_1:36;
then reconsider fs1 as FinSequence of NAT by FINSEQ_1:36;
Product(fp)=Product(fs1^<*fp.a*>)*Product(fs2) by A1,RVSUM_1:97
.=(fp.a)*Product(fs1)*Product(fs2) by RVSUM_1:96
.=(fp.a)*(Product(fs1)*Product(fs2));
hence thesis by A2,XCMPLX_1:89;
end;
suppose
A3: fp.a=0;
Product(fp)/fp.a = Product(fp)*(fp.a)" by XCMPLX_0:def 9
.= Product(fp)*(0 qua Nat) by A3
.= 0;
hence thesis;
end;
end;
theorem Th22:
numerator(q),denominator(q) are_coprime
proof
set k=numerator(q);
set h=denominator(q);
reconsider a=k gcd h as Element of NAT by INT_2:20;
a divides k by INT_2:21;
then
A1: ex l st k=a*l;
(k gcd h) divides h by INT_2:21;
then consider b be Nat such that
A2: h=a*b by NAT_D:def 3;
a<>0 by INT_2:5;
then
A3: a>=0 qua Nat+1 by NAT_1:13;
reconsider b as Element of NAT by ORDINAL1:def 12;
A4: h=a*b by A2;
assume not k,h are_coprime;
then a<>1 by INT_2:def 3;
then a>1 by A3,XXREAL_0:1;
hence contradiction by A1,A4,RAT_1:29;
end;
theorem
q=k/a & a<>0 & k,a are_coprime implies k=numerator(q) & a=
denominator(q)
proof
assume that
A1: q=k/a & a<>0 and
A2: k,a are_coprime;
consider b being Nat such that
A3: k=numerator(q)*b & a=denominator(q)*b by A1,RAT_1:27;
numerator(q),denominator(q) are_coprime by Th22;
then k gcd a = |.b.| by A3,INT_2:24;
then 1=|.b.| by A2,INT_2:def 3
.=b by ABSVALUE:def 1;
hence thesis by A3;
end;
theorem Th24:
(ex q st a=q|^b) implies ex k st a=k|^b
proof
given q such that
A1: a=q|^b;
now
A2: now
set d=denominator(q);
set k=numerator(q);
assume b<>0;
then consider e be Nat such that
A3: e+1=b by NAT_1:6;
A4: d|^b <>0 by CARD_4:3;
(k |^ b),d are_coprime by Th10,Th22;
then
A5: (k|^b gcd d)=1 by INT_2:def 3;
A6: q=k/d;
then a=(k|^b)/(d|^b) by A1,PREPOWER:8;
then a*(d |^ b)=(k |^ b) by A4,XCMPLX_1:87;
then (k |^ b)=a*((d |^ e)*d) by A3,NEWTON:6
.=(a*(d |^ e))*d;
then d divides (k |^ b);
then d=1 or d=-1 by A5,INT_2:13,22;
hence thesis by A1,A6;
end;
now
assume
A7: b=0;
then a=1 by A1,NEWTON:4;
then a=1|^0;
hence thesis by A7;
end;
hence thesis by A2;
end;
hence thesis;
end;
theorem Th25:
(ex q st a=q|^d) implies ex b st a=b|^d
proof
assume ex q st a=q|^d;
then consider k such that
A1: a=k|^d by Th24;
A2: now
assume
A3: a=0;
then d<>0 by A1,NEWTON:4;
then a=0|^d by A3,NAT_1:14,NEWTON:11;
hence thesis;
end;
per cases;
suppose d<>0;
now
consider e such that
A4: d=2*e or d=2*e+1 by Lm4;
consider c being Nat such that
A5: k=c or k=-c by INT_1:2;
assume
A6: not k is Nat;
A7: now
assume d=2*e+1;
then -c|^d=a by A1,A6,A5,Th2;
hence thesis by A2;
end;
now
assume d=2*e;
then a=c|^d by A1,A5,Th2;
hence thesis;
end;
hence thesis by A4,A7;
end;
hence thesis by A1;
end;
suppose
A8: d=0;
then a=1 by A1,NEWTON:4;
then a=1|^0;
hence thesis by A8;
end;
end;
theorem
e>0 & (a|^e) divides (b|^e) implies a divides b
proof
assume that
A1: e>0 and
A2: (a|^e) divides (b|^e);
consider f be Nat such that
A3: (a|^e)*f=(b|^e) by A2,NAT_D:def 3;
A4: now
assume that
A5: a<>0 and
b<>0;
a|^e<>0 by A5,CARD_4:3;
then f=(b|^e)/(a|^e) by A3,XCMPLX_1:89
.=(b/a)|^e by PREPOWER:8;
then consider d such that
A6: f=d|^e by Th25;
b|^e=(a*d)|^e by A3,A6,NEWTON:7;
then b=a*d by A1,Th3;
hence thesis;
end;
A7: now
assume
A8: a=0;
then 0 divides (b|^e) by A1,A2,NAT_1:14,NEWTON:11;
then ex f be Nat st 0*f=b|^e by NAT_D:def 3;
hence thesis by A8,CARD_4:3;
end;
now
assume b=0;
then a*(0 qua Nat)=b;
hence thesis;
end;
hence thesis by A7,A4;
end;
theorem Th27:
ex m,n st a gcd b = a*m+b*n
proof
A1: ex m,n st 0 gcd c =0*m+c*n
proof
take 0,1;
thus thesis by NEWTON:52;
end;
now
per cases;
suppose
a=0;
hence thesis by A1;
end;
suppose
A2: b=0;
then ex m,n st (a gcd b)=0*m+a*n by A1;
hence thesis by A2;
end;
suppose
A3: a<>0 & b<>0;
defpred P[set] means ex m,n st $1=a*m+b*n & $1<>0;
a+b=a*1+b*1;
then
A4: ex c be Nat st P[c] by A3;
consider d being Nat such that
A5: P[d] & for c being Nat st P[c] holds d<=c from NAT_1:sch 5(A4);
consider e,f be Nat such that
A6: a=d*e+f and
A7: f<d by A5,NAT_1:17;
consider m,n such that
A8: d=a*m+b*n by A5;
A9: now
assume
A10: f<>0;
f=a-d*e by A6
.=a*(1-m*e)+b*(-(n*e)) by A8;
hence contradiction by A5,A7,A10;
end;
consider e,f be Nat such that
A11: b=d*e+f and
A12: f<d by A5,NAT_1:17;
now
assume
A13: f<>0;
f=b-d*e by A11
.=b*(1-n*e)+a*(-(m*e)) by A8;
hence contradiction by A5,A12,A13;
end;
then
A14: d divides b by A11;
d divides a by A6,A9;
then
A15: d divides (a gcd b) by A14,NAT_D:def 5;
(a gcd b) divides a & (a gcd b) divides b by NAT_D:def 5;
then (a gcd b) divides (d qua Integer) by A8,Th5;
hence thesis by A8,A15,NAT_D:5;
end;
end;
hence thesis;
end;
theorem Th28:
ex m1,n1 st m gcd n = m*m1+n*n1
proof
m gcd n=|.m.| gcd |.n.| by INT_2:34;
then consider m1,n1 such that
A1: |.m.|*m1+|.n.|*n1=(m gcd n) by Th27;
now
per cases;
suppose
m>=0 & n>=0;
then |.m.|=m & |.n.|=n by ABSVALUE:def 1;
hence thesis by A1;
end;
suppose
A2: m>=0 & n<0;
then |.n.|=-n by ABSVALUE:def 1;
then (m gcd n)=m*m1+n*(-n1) by A1,A2,ABSVALUE:def 1;
hence thesis;
end;
suppose
A3: m<0 & n>=0;
then |.m.|=-m by ABSVALUE:def 1;
then (m gcd n)=m*(-m1)+n*n1 by A1,A3,ABSVALUE:def 1;
hence thesis;
end;
suppose
m<0 & n<0;
then |.m.|=-m & |.n.|=-n by ABSVALUE:def 1;
then m gcd n=m*(-m1)+n*(-n1) by A1;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th29:
m divides n*k & m gcd n=1 implies m divides k
proof
assume that
A1: m divides n*k and
A2: (m gcd n)=1;
consider m1,n1 such that
A3: m*m1+n*n1=1 by A2,Th28;
k=(m*m1+n*n1)*k by A3
.=m*(m1*k)+(n*k)*n1;
hence thesis by A1,Th5;
end;
theorem
for a,b,c being Nat holds a gcd b=1 & a divides b*c implies a divides
c by Th29;
theorem Th31:
a<>0 & b<>0 implies ex c,d st a gcd b=a*c-b*d
proof
assume that
A1: a<>0 and
A2: b<>0;
consider m,n such that
A3: (a gcd b)=a*m+b*n by Th27;
set k=[/max(-m/b,n/a)\]+1;
k>n/a by INT_1:32,XXREAL_0:31;
then k*a>n by A1,XREAL_1:77;
then
A4: k*a-n>0 by XREAL_1:50;
k>-m/b by INT_1:32,XXREAL_0:31;
then k>(-m)/b by XCMPLX_1:187;
then k*b>-m by A2,XREAL_1:77;
then k*b--m>0 by XREAL_1:50;
then reconsider e=k*b+m,d=k*a-n as Element of NAT by A4,INT_1:3;
a*e-b*d=a*m+(0 qua Nat)+b*n;
hence thesis by A3;
end;
theorem
f>0 & g>0 & (f gcd g)=1 & a|^f=b|^g implies ex e st a=e|^g & b=e|^f
proof
assume that
A1: f>0 and
A2: g>0 and
A3: (f gcd g)=1 and
A4: a|^f=b|^g;
now
per cases;
suppose
A5: a=0;
then a|^f=0 by A1,NAT_1:14,NEWTON:11;
then
A6: b=0|^f by A4,A5,CARD_4:3;
a=0|^g by A2,A5,CARD_4:3;
hence thesis by A6;
end;
suppose
A7: b=0;
then b|^g=0 by A2,NAT_1:14,NEWTON:11;
then
A8: a=0|^g by A4,A7,CARD_4:3;
b=0|^f by A1,A7,CARD_4:3;
hence thesis by A8;
end;
suppose
A9: a<>0 & b<>0;
consider c,d such that
A10: f*c-g*d=1 by A1,A2,A3,Th31;
reconsider q=(b|^c)/(a|^d) as Rational;
a=a #Z 1 by PREPOWER:35
.=(a |^ (f*c))/(a |^ (d*g)) by A9,A10,PREPOWER:43
.=((a |^ f) |^ c)/(a |^ (d*g)) by NEWTON:9
.=((b |^ g) |^ c)/((a |^ d) |^ g) by A4,NEWTON:9
.=(b |^ (g*c))/((a |^ d) |^ g) by NEWTON:9
.=((b |^ c) |^ g)/((a |^ d) |^ g) by NEWTON:9
.=q|^g by PREPOWER:8;
then consider h such that
A11: a=h|^g by Th25;
b|^g=h|^(f*g) by A4,A11,NEWTON:9
.=(h|^f)|^g by NEWTON:9;
then b=h|^f by A2,Th3;
hence thesis by A11;
end;
end;
hence thesis;
end;
reserve x,y,t for Integer;
theorem Th33:
(ex x,y st m*x+n*y=k) iff (m gcd n) divides k
proof
A1: now
assume
A2: (m gcd n) divides k;
now
consider m1,n1 such that
A3: (m gcd n)=m*m1+n*n1 by Th28;
consider l such that
A4: (m gcd n)*l=k by A2;
k=m*(m1*l)+n*(n1*l) by A4,A3;
hence ex x,y st m*x+n*y=k;
end;
hence ex x,y st m*x+n*y=k;
end;
now
given x,y such that
A5: m*x+n*y=k;
(m gcd n) divides m & (m gcd n) divides n by INT_2:21;
hence (m gcd n) divides k by A5,Th5;
end;
hence thesis by A1;
end;
theorem
m<>0 & n<>0 & m*m1+n*n1=k implies for x,y st m*x+n*y=k ex t st x=m1+t*
(n/(m gcd n)) & y=n1-t*(m/(m gcd n))
proof
assume that
A1: m<>0 and
A2: n<>0 and
A3: m*m1+n*n1=k;
consider m2,n2 such that
A4: m=(m gcd n)*m2 and
A5: n=(m gcd n)*n2 and
A6: m2,n2 are_coprime by A1,INT_2:23;
A7: (m gcd n)<>0 by A1,INT_2:5;
then
A8: m2=m/(m gcd n) by A4,XCMPLX_1:89;
A9: n2=n/(m gcd n) by A7,A5,XCMPLX_1:89;
A10: (n2 gcd m2)=1 by A6,INT_2:def 3;
let x,y;
assume m*x+n*y=k;
then m*(x-m1)=n*(n1-y) by A3;
then
A11: m2*(x-m1)=(n*(n1-y))/(m gcd n) by A8,XCMPLX_1:74
.=n2*(n1-y) by A9,XCMPLX_1:74;
then n2 divides (m2*(x-m1));
then n2 divides (x-m1) by A10,Th29;
then consider t such that
A12: n2*t=x-m1;
A13: n2<>0 by A2,A5;
then
A14: t=(x-m1)/n2 by A12,XCMPLX_1:89;
A15: m2<>0 by A1,A4;
then (x-m1)/n2=(n1-y)/m2 by A13,A11,XCMPLX_1:94;
then t*m2=n1-y by A15,A14,XCMPLX_1:87;
then
A16: y=n1-t*m2;
x=m1+t*n2 by A12;
hence thesis by A8,A9,A16;
end;
theorem
a gcd b=1 & a*b=c|^d implies ex e,f st a=e|^d & b=f|^d
proof
assume that
A1: (a gcd b)=1 and
A2: a*b=c|^d;
set e=a gcd c;
e divides c by NAT_D:def 5;
then
A3: e|^d divides c|^d by Th14;
e divides a by NAT_D:def 5;
then e gcd b=1 by A1,Th15,NEWTON:57;
then e|^d gcd b=1 by Th12;
then e|^d divides a by A2,A3,Th29;
then consider g be Nat such that
A4: (e|^d)*g=a by NAT_D:def 3;
reconsider g as Element of NAT by ORDINAL1:def 12;
A5: now
assume
A6: d<>0;
then consider d1 being Nat such that
A7: d=1+d1 by NAT_1:10,14;
reconsider d1 as Element of NAT by ORDINAL1:def 12;
A8: d>=1 by A6,NAT_1:14;
A9: now
assume
A10: e<>0;
then
A11: a<>0 or c <>0 by INT_2:5;
then
A12: a <> 0 by A2,CARD_4:3;
A13: now
reconsider e1=e as Real;
assume
A14: c <>0;
then consider a1,c1 being Integer such that
A15: a=e*a1 and
A16: e*c1=c and
A17: a1,(c1 qua Integer) are_coprime by INT_2:23;
reconsider a1,c1 as Element of NAT by A12,A14,A15,A16,Lm6;
a1=(e|^(d1+1))*g/e by A4,A7,A10,A15,XCMPLX_1:89
.=(e*(e|^d1)*g)/e by NEWTON:6
.=e*((e|^d1)*g)/e
.=(e|^d1)*g by A10,XCMPLX_1:89;
then
A18: g divides a1;
(a1 gcd c1)=1 by A17,INT_2:def 3;
then (g gcd c1)=1 by A18,Th15,NEWTON:57;
then
A19: (g gcd c1|^d)=1 by Th12;
A20: e1|^d<>0 by A10,CARD_4:3;
c1=c/e by A10,A16,XCMPLX_1:89;
then
A21: c1|^d=(e|^d)*(g*b)/(e|^d) by A2,A4,PREPOWER:8
.=g*b by A20,XCMPLX_1:89;
then g divides (c1|^d);
then g=1 by A19,NEWTON:49;
hence thesis by A4,A21;
end;
now
assume 0=c;
then
A22: b=0 by A2,A8,A11,NEWTON:11,XCMPLX_1:6;
then a=1 by A1,NEWTON:52;
then
A23: a=1|^d;
b=0|^d by A6,A22,NAT_1:14,NEWTON:11;
hence thesis by A23;
end;
hence thesis by A13;
end;
now
assume e=0;
then
A24: a=0 by INT_2:5;
then b=1 by A1,NEWTON:52;
then
A25: b=1|^d;
a=0|^d by A6,A24,NAT_1:14,NEWTON:11;
hence thesis by A25;
end;
hence thesis by A9;
end;
now
assume
A26: d=0;
then
A27: a*b=1 by A2,NEWTON:4;
then b divides 1;
then b=1 by Th15;
then
A28: b=1|^0;
a divides 1 by A27;
then a=1 by Th15;
then a=1|^0;
hence thesis by A26,A28;
end;
hence thesis by A5;
end;
:: Chinese remainder theorem
::$N Chinese Remainder Theorem
::$L https://en.wikipedia.org/wiki/Chinese_remainder_theorem Chinese Remainder Theorem
theorem Th36:
for d holds (for a st a in dom fp holds fp.a gcd d=1) implies
Product(fp) gcd d = 1
proof
let d;
defpred TH[set] means ex f being FinSequence of NAT st f = $1 &
((for a st a in dom f holds f.a gcd d=1) implies Product(f) gcd d = 1);
A1: now
let fp;
let a be Element of NAT such that
A2: TH[fp];
thus TH[fp^<*a*>]
proof
set fp1=fp^<*a*>;
take fp1;
thus fp1 = fp^<*a*>;
assume
A3: for b st b in dom fp1 holds fp1.b gcd d=1;
A4: dom fp c= dom fp1 by FINSEQ_1:26;
A5: for b st b in dom fp holds fp.b gcd d=1
proof
let b;
assume
A6: b in dom fp;
then fp1.b gcd d=1 by A3,A4;
hence thesis by A6,FINSEQ_1:def 7;
end;
len fp1 in dom fp1 by FINSEQ_5:6;
then len fp1=len fp + 1 & fp1.len fp1 gcd d=1 by A3,FINSEQ_2:16;
then
A7: a gcd d=1 by FINSEQ_1:42;
Product(fp1)=Product(fp)*a by RVSUM_1:96;
hence thesis by A2,A5,A7,Th6;
end;
end;
A8: TH[<*>NAT]
proof
take <*>NAT;
thus thesis by NEWTON:51,RVSUM_1:94;
end;
for fp holds TH[fp] from FINSEQ_2:sch 2(A8,A1);
then ex f being FinSequence of NAT st f = fp &
((for a st a in dom f holds f.a gcd d=1) implies Product(f) gcd d=1);
hence thesis;
end;
theorem
len fp>=2 & (for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b
gcd fp.c)=1) implies for fr st len fr=len fp holds ex fr1 st (len fr1=len fp &
for b st b in dom fp holds (fp.b)*(fr1.b)+(fr.b)=(fp.1)*(fr1.1)+(fr.1))
proof
defpred CC[FinSequence of NAT] means for fr st len fr=len $1 holds ex fr1 st
(len fr1=len $1 & for b st b in dom $1 holds ($1.b)*(fr1.b)+(fr.b)=($1.1)*(fr1.
1)+(fr.1));
defpred RP[FinSequence of NAT] means for b,c st b in dom $1 & c in dom $1 &
b<>c holds ($1.b gcd $1.c)=1;
defpred TH[set] means ex f being FinSequence of NAT st f = $1 &
((len f>=2 & RP[f]) implies CC[f]);
A1: now
let fp;
let d be Element of NAT such that
A2: TH[fp];
set k=len fp;
set fp1=fp^<*d*>;
now
assume that
A3: len fp1>=2 and
A4: RP[fp1];
A5: len fp1=k+1 by FINSEQ_2:16;
now
per cases by A3,XXREAL_0:1;
suppose
A6: len fp1=2;
now
let fr such that
len fr=len fp1;
1 in dom fp1 & 2 in dom fp1 by A6,FINSEQ_3:25;
then fp1.1 gcd fp1.2=1 by A4;
then (fp1.1 gcd fp1.2) divides (fr.1 - fr.2) by INT_2:12;
then consider m,n such that
A7: (fp1.1)*m+(fp1.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*>;
thus len fr1=len fp1 by A6,FINSEQ_1:44;
let b;
assume b in dom fp1;
then
A8: b in Seg len fp1 by FINSEQ_1:def 3;
now
per cases by A6,A8,FINSEQ_1:2,TARSKI:def 2;
suppose
b=1;
hence (fp1.b)*(fr1.b)+(fr.b)=(fp1.1)*(fr1.1)+(fr.1);
end;
suppose
A9: b=2;
(fp1.2)*n-(fp1.1)*(-m)=fr.1-fr.2 by A7;
hence
(fp1.b)*(fr1.b)+(fr.b)=(fp1.1)*(fr1.1)+(fr.1) by A9,
XCMPLX_1:34;
end;
end;
hence (fp1.b)*(fr1.b)+(fr.b)=(fp1.1)*(fr1.1)+fr.1;
end;
hence CC[fp1];
end;
suppose
A11: len fp1 > 2;
A12: RP[fp]
proof
A13: dom fp c= dom fp1 by FINSEQ_1:26;
let b,c such that
A14: b in dom fp & c in dom fp and
A15: b<>c;
fp1.b=fp.b & (fp1.c)=fp.c by A14,FINSEQ_1:def 7;
hence thesis by A4,A14,A15,A13;
end;
A16: k+1 > 1+1 by A11,FINSEQ_2:16;
then
A17: k >= 1+1 by NAT_1:13;
now
let fr2;
assume
A18: len fr2=len fp1;
then consider
fr being FinSequence of INT,m being Element of INT such
that
A19: fr2=fr^<*m*> by FINSEQ_2:19;
A20: k + 1=len fr + 1 by A5,A18,A19,FINSEQ_2:16;
then consider fr1 such that
len fr1=k and
A21: for b 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;
a in dom fp implies fp.a gcd d=1
proof
A22: (len fp+1) in dom fp1 by A5,FINSEQ_5:6;
A23: dom fp c= dom fp1 & fp1.(len fp+1)=d by FINSEQ_1:26,42;
assume
A24: a in dom fp;
len fp+1>len fp by NAT_1:13;
then
A25: len fp+1 <> a by A24,FINSEQ_3:25;
fp1.a=fp.a by A24,FINSEQ_1:def 7;
hence thesis by A4,A24,A23,A25,A22;
end;
then Product(fp) gcd d=1 by Th36;
then (Product(fp) gcd d) divides (fr2.(k+1)-(fp.1)*(fr1.1)-fr2.1)
by INT_2:12;
then consider m1,n1 such that
A26: Product(fp)*m1+d*n1=fr2.(k+1)-(fp.1)*(fr1.1)-fr2.1 by Th33;
reconsider x=-n1 as Element of INT by INT_1:def 2;
deffunc F(Nat) = Product Del(fp,$1)*m1+fr1.$1;
consider s2 being FinSequence such that
A27: len s2=k & for a being Nat st a in dom s2 holds s2.a=F(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;
assume
A29: a in dom s2;
reconsider a as Element of NAT by ORDINAL1:def 12;
s2.a=Product Del(fp,a)*m1+fr1.a by A27,A29;
hence thesis by INT_1:def 2;
end;
A30: dom s2 = Seg k by A27,FINSEQ_1:def 3;
reconsider s2 as FinSequence of INT by A28,FINSEQ_2:12;
take fr3=s2^<*x*>;
thus len fr3=len fp1 by A5,A27,FINSEQ_2:16;
let b such that
A31: b in dom fp1;
thus (fp1.b)*(fr3.b)+(fr2.b)=(fp1.1)*(fr3.1)+(fr2.1)
proof
A32: c in Seg k implies (fp1.c)*(fr3.c)=Product(fp)*m1+(fp.c)*( fr1.c)
proof
assume
A33: c in Seg k;
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 = fp1.c by FINSEQ_1:def 7;
hence
(fp1.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;
end;
A37: 1<=b by A31,FINSEQ_3:25;
A38: b<=k+1 by A5,A31,FINSEQ_3:25;
now
per cases by A38,NAT_1:8;
suppose
A39: b<=k;
then 1<=k by A37,XXREAL_0:2;
then
A40: 1 in Seg k;
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 k 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 (fp1.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)
.=(fp1.1)*(fr3.1)+(fr2.1) by A32,A40,A41;
end;
suppose
A45: b=k+1;
then
A46: fp1.b=d by FINSEQ_1:42;
A47: fr2.b-((fp.1)*(fr1.1)+fr2.1) =d*n1+ Product(fp)*m1 by A26,A45
;
1<=k by A17,XXREAL_0:2;
then 1 in Seg k;
then
(fp1.1)*(fr3.1)+(fr2.1)= Product(fp)*m1+(fp.1)*(fr1.1)+
(fr2.1) by A32
.=fr2.b+d*(-n1) by A47;
hence thesis by A27,A45,A46,FINSEQ_1:42;
end;
end;
hence thesis;
end;
end;
hence CC[fp1];
end;
end;
hence CC[fp1];
end;
hence TH[fp1];
end;
A48: TH[<*>NAT]
proof
take <*>NAT;
thus thesis;
end;
for fp holds TH[fp] from FINSEQ_2:sch 2(A48,A1);
then ex f being FinSequence of NAT st f = fp &
((len f>=2 & RP[f]) implies CC[f]);
hence thesis;
end;
:: THUE'S THEOREM
Lm17: k divides m iff k divides (|.m.|)
proof
per cases;
suppose
m>=0;
hence thesis by ABSVALUE:def 1;
end;
suppose
m<0;
then |.m.|=-m by ABSVALUE:def 1;
hence thesis by INT_2:10;
end;
end;
Lm18: m*n mod n=0
proof
per cases;
suppose
A1: n<>0;
hence m*n mod n=m*n-(m*n div n)*n by INT_1:def 10
.=m*n-[\(m*n)/n/]*n by INT_1:def 9
.=m*n-[\m/]*n by A1,XCMPLX_1:89
.=m*n-m*n
.=0;
end;
suppose
n=0;
thus thesis;
end;
end;
Lm19: k mod n=m mod n implies (k-m) mod n=0
proof
assume
A1: k mod n=m mod n;
per cases;
suppose
A2: n <> 0;
then k-(k div n)*n=m mod n by A1,INT_1:def 10
.=m-(m div n)*n by A2,INT_1:def 10;
then k-m=n*((k div n)-(m div n));
hence thesis;
end;
suppose
n = 0;
hence thesis;
end;
end;
Lm20: n <> 0 & m mod n=0 implies n divides m
proof
assume n <> 0 & m mod n=0;
then m=(m div n)*n+(0 qua Nat) by NEWTON:66
.=(m div n)*n;
hence thesis;
end;
Lm21: (1<x implies 1<sqrt x & sqrt x<x) & (0<x & x<1 implies 0<sqrt x & sqrt x
<1 & x<sqrt x)
proof
hereby
assume
A1: 1<x;
hence 1<sqrt x by SQUARE_1:18,27;
then sqrt x<(sqrt x)^2 by SQUARE_1:14;
hence sqrt x<x by A1,SQUARE_1:def 2;
end;
hereby
assume that
A2: 0<x and
A3: x<1;
thus
A4: 0<sqrt x by A2,SQUARE_1:17,27;
thus sqrt x<1 by A2,A3,SQUARE_1:18,27;
then (sqrt x)^2<sqrt x by A4,SQUARE_1:13;
hence x<sqrt x by A2,SQUARE_1:def 2;
end;
end;
::$N Thue Theorem
theorem
a<>0 & a gcd k=1 implies ex b,e st 0<>b & 0<>e & b<=sqrt a & e<=sqrt a
& (a divides (k*b+e) or a divides (k*b-e))
proof
assume that
A1: a<>0 and
A2: (a gcd k)=1;
A3: a>=1 by A1,NAT_1:14;
per cases by A3,XXREAL_0:1;
suppose
A4: a=1;
take b=1, e=1;
thus b<>0 & e<>0;
thus b<=sqrt a & e<=sqrt a by A4;
thus a divides k*b+e or a divides k*b-e by A4,INT_2:12;
end;
suppose
A5: a>1;
A6: sqrt a>0 by A1,SQUARE_1:25;
set d=[\sqrt a/];
A7: d<=sqrt a by INT_1:def 6;
sqrt a<a by A5,Lm21;
then
A8: d<a by A7,XXREAL_0:2;
set d1=d+1;
A9: d>sqrt a -1 by INT_1:def 6;
sqrt a>1 by A5,SQUARE_1:18,27;
then
A10: sqrt a -1>0 by XREAL_1:50;
then reconsider d as Element of NAT by A9,INT_1:3;
A11: d+1>=1 by Lm1;
then reconsider d1 as Element of NAT;
set e1=d1^2;
e1=d1*d1;
then reconsider e1 as Element of NAT;
A12: (e1-1)/d1=d1-1/d1 by A11,XCMPLX_1:127;
deffunc F(Nat) = 1+ ((k*(($1-1) div d1)+(($1-1) mod d1)) mod a);
consider fs such that
A13: len fs=e1 & for b being Nat st b in dom fs holds fs.b=F(b) from
FINSEQ_1:sch 2;
A14: rng fs c= Seg a
proof
let v be object;
assume v in rng fs;
then consider b being Nat such that
A15: b in dom fs & fs.b=v by FINSEQ_2:10;
A16: v=1+ ((k*((b-1) div d1)+((b-1) mod d1)) mod a) by A13,A15;
then reconsider v1=v as Integer;
A17: 0<=((k*((b-1) div d1)+((b-1) mod d1)) mod a);
A18: 1<=v1 by A16,Lm1;
reconsider v1 as Element of NAT by A16,INT_1:3;
((k*((b-1) div d1)+((b-1) mod d1)) mod a)<a by A1,NEWTON:65;
then v1<=a by A16,Lm9;
hence thesis by A18;
end;
sqrt a<d1 by A9,XREAL_1:19;
then (sqrt a)^2<e1 by A6,SQUARE_1:16;
then
A19: a<e1 by SQUARE_1:def 2;
then
A20: Seg a c= Seg e1 by FINSEQ_1:5;
A21: Seg e1=dom fs by A13,FINSEQ_1:def 3;
then rng fs <> dom fs by A19,A14,FINSEQ_1:5;
then not fs is one-to-one by A21,A14,A20,FINSEQ_4:59,XBOOLE_1:1;
then consider v1,v2 being object such that
A22: v1 in dom fs and
A23: v2 in dom fs and
A24: fs.v1=fs.v2 and
A25: v1<>v2 by FUNCT_1:def 4;
reconsider v1,v2 as Element of NAT by A22,A23;
set x1=(v1-1) div d1, x2=(v2-1) div d1, x=x1-x2;
set y1=(v1-1) mod d1, y2=(v2-1) mod d1, y=y1-y2;
A26: y1>=0;
fs.v1=1+((k*x1+y1) mod a) & fs.v2=1+((k*x2+y2) mod a) by A13,A22,A23;
then
A27: ((k*x1+y1)-(k*x2+y2)) mod a = 0 by A24,Lm19,XCMPLX_1:2;
then
A28: a divides (k*x1+y1)-(k*x2+y2) by A1,Lm20;
1/d1>0 by A9,A10,XREAL_1:139;
then
A29: (e1-1)/d1<d1 by A12,Lm1;
A30: x2=[\(v2-1)/d1/] by INT_1:def 9;
then
A31: x2<=(v2-1)/d1 by INT_1:def 6;
v2<=e1 by A13,A23,FINSEQ_3:25;
then v2-1<=e1-1 by XREAL_1:9;
then (v2-1)/d1<=(e1-1)/d1 by XREAL_1:72;
then (v2-1)/d1<d1 by A29,XXREAL_0:2;
then x2<d1 by A31,XXREAL_0:2;
then
A32: x2<=d by Lm9;
set d2=k*x+y;
A33: [\0/]=0;
A34: x1=[\(v1-1)/d1/] by INT_1:def 9;
then
A35: x1<=(v1-1)/d1 by INT_1:def 6;
1<=v1 by A22,FINSEQ_3:25;
then v1-1>=0 by XREAL_1:48;
then x1>=0 by A34;
then x2-x1<=d by A32,Lm2;
then
A36: -(x2-x1)>=-d by XREAL_1:24;
A37: x<>0 or y<>0
proof
assume not thesis;
then v1-1=x2*d1+y2 by A11,NEWTON:66
.=v2-1 by A11,NEWTON:66;
hence contradiction by A25;
end;
v1<=e1 by A13,A22,FINSEQ_3:25;
then v1-1<=e1-1 by XREAL_1:9;
then (v1-1)/d1<=(e1-1)/d1 by XREAL_1:72;
then (v1-1)/d1<d1 by A29,XXREAL_0:2;
then x1<d1 by A35,XXREAL_0:2;
then
A38: x1<=d by Lm9;
A39: (k*x1+y1)-(k*x2+y2)=k*x+y;
y2<d1 by A9,A10,NEWTON:65;
then y2-y1<d1 by Lm3;
then y2-y1<=d by Lm9;
then
A40: -(y2-y1)>=-d by XREAL_1:24;
take b=|.x.|, e=|.y.|;
A41: y2>=0;
1<=v2 by A23,FINSEQ_3:25;
then v2-1>=0 by XREAL_1:48;
then x2>=0 by A30;
then x<=d by A38,Lm2;
then
A42: |.x.|<=d by A36,ABSVALUE:5;
then
A43: |.x.|<a by A8,XXREAL_0:2;
A44: now
assume
A45: y=0;
then a divides x by A1,A2,A27,A39,Lm20,Th29;
then a divides (|.x.|) by Lm17;
then |.x.|=0 by A43,NAT_D:7;
hence contradiction by A37,A45,ABSVALUE:2;
end;
y1<d1 by A9,A10,NEWTON:65;
then y<d1 by Lm3;
then y<=d by Lm9;
then
A46: |.y.|<=d by A40,ABSVALUE:5;
then
A47: |.y.|<a by A8,XXREAL_0:2;
now
assume
A48: x=0;
then a divides (|.y.|) by A28,Lm17;
then |.y.|=0 by A47,NAT_D:7;
hence contradiction by A37,A48,ABSVALUE:2;
end;
hence b<>0 & e<>0 by A44,ABSVALUE:2;
thus b<=sqrt a by A7,A42,XXREAL_0:2;
thus e<=sqrt a by A7,A46,XXREAL_0:2;
A49: b=x or b=-x by ABSVALUE:1;
A50: e=y or e=-y by ABSVALUE:1;
-d2=k*(-x)+-y;
hence thesis by A28,A49,A50,INT_2:10;
end;
end;
theorem
dom Del(fs,a) c= dom fs by Lm12;
theorem
Del (<*v*>^fs, 1) = fs & Del (fs^<*v*>, len fs + 1) = fs by Lm14;
begin :: Addenda
:: from JORDAN1D, 2007.07.27, A.T.
reserve n for Nat;
theorem
n > 0 & k mod n <> 0 implies - (k div n) = (-k) div n + 1
proof
assume
A1: n > 0;
assume k mod n <> 0;
then not n qua Integer divides k;
then
A2: k/n is not Integer by A1,Th17;
thus - (k div n) = - [\ k / n /] by INT_1:def 9
.= [\ (-k) / n /] + 1 by A2,INT_1:63
.= (-k) div n + 1 by INT_1:def 9;
end;
theorem
k mod n = 0 implies - (k div n) = (-k) div n
proof
assume
A1: k mod n = 0;
per cases;
suppose
A2: n > 0;
then n divides k by A1,INT_1:62;
then
A3: k/n is Integer by A2,Th17;
thus - (k div n) = - [\ k / n /] by INT_1:def 9
.= [\ (-k) / n /] by A3,INT_1:64
.= (-k) div n by INT_1:def 9;
end;
suppose n = 0;
hence thesis;
end;
end;
reserve i1,i2,i3 for Integer;
Lm4: i1 divides i2 & i1 divides i3 implies i1 divides (i2-i3)
proof
assume that
A1: i1 divides i2 and
A2: i1 divides i3;
consider i4 being Integer such that
A3: i2=i1*i4 by A1;
consider i5 being Integer such that
A4: i3=i1*i5 by A2;
i2-i3=i1*(i4-i5) by A3,A4;
hence thesis;
end;
theorem ::: INT_4:14
i1,i2 are_congruent_mod i3 implies i1 gcd i3 = i2 gcd i3
proof
set d=i2 gcd i3;
reconsider d as Nat;
assume i1,i2 are_congruent_mod i3;
then i3 divides (i1-i2);
then consider i being Integer such that
A1: i1-i2=i3*i;
A2: d = |.i2.| gcd |.i3.| by INT_2:34;
then d divides |.i2.| by NAT_D:def 5;
then |.d.| divides |.i2.| by ABSVALUE:def 1;
then
A3: d divides i2 by INT_2:16;
A4: i2=i1-i3*i by A1;
A5: for n being Nat st n divides |.i1.| & n divides |.i3.| holds n divides d
proof
let n be Nat;
assume that
A6: n divides |.i1.| and
A7: n divides |.i3.|;
|.n.| divides |.i3.| by A7,ABSVALUE:def 1;
then n divides i3 by INT_2:16;
then
A8: n divides i3*i by INT_2:2;
|.n.| divides |.i1.| by A6,ABSVALUE:def 1;
then n divides i1 by INT_2:16;
then n divides i2 by A4,A8,Lm4;
then |.n.| divides |.i2.| by INT_2:16;
then n divides |.i2.| by ABSVALUE:def 1;
hence thesis by A2,A7,NAT_D:def 5;
end;
A9: d divides |.i3.| by A2,NAT_D:def 5;
then |.d.| divides |.i3.| by ABSVALUE:def 1;
then d divides i3 by INT_2:16;
then
A10: d divides i3*i by INT_2:2;
i1=i3*i+i2 by A1;
then |.d.|=d & d divides i1 by A3,A10,ABSVALUE:def 1,Th4;
then d divides |.i1.| by INT_2:16;
then |.i1.| gcd |.i3.| = d by A9,A5,NAT_D:def 5;
hence thesis by INT_2:34;
end;