:: The Chinese Remainder Theorem :: by Andrzej Kondracki :: :: Received December 30, 1997 :: Copyright (c) 1997-2018 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; 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, INT_1; 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; 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: x|^2=x*x & (-x)|^2=x|^2 proof 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,INT_1:def 3; consider n1 such that A4: n=k*n1 by A2,INT_1:def 3; m+n=k*(m1+n1) by A3,A4; hence thesis by INT_1:def 3; 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 by INT_1:def 3; now per cases; suppose m>=0; then |.m.|*l=k by A2,ABSVALUE:def 1; hence (|.m.|) divides k by INT_1:def 3; end; suppose m<0; then |.m.|*(-l)=(-m)*(-l) by ABSVALUE:def 1 .=k by A2; hence |.m.| divides k by INT_1:def 3; end; end; hence |.m.| divides k; end; now assume |.m.| divides k; then consider l such that A3: |.m.|*l=k by INT_1:def 3; now per cases; suppose m>=0; then m*l=k by A3,ABSVALUE:def 1; hence m divides k by INT_1:def 3; end; suppose m<0; then k=(-m)*l by A3,ABSVALUE:def 1 .=m*(-l); hence m divides k by INT_1:def 3; 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 by NAT_D:def 3; 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 by NAT_D:def 3; end; hence thesis by A2; end; theorem Th17: k<>0 implies (k divides l iff l/k is Integer) proof assume A1: k<>0; A2: now assume l/k is Integer; then reconsider m=l/k as Integer; l=k*m by A1,XCMPLX_1:87; hence k divides l by INT_1:def 3; end; now assume k divides l; then ex m st l=k*m by INT_1:def 3; hence l/k is Integer by A1,XCMPLX_1:89; end; hence thesis by A2; 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,INT_1:def 3; 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 integer; coherence proof 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; end; end; definition let fp; redefine func Sum(fp) -> Element of NAT; 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; definition let fp; redefine func Product fp -> Element of NAT; 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; 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 :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+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; 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+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 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 FinSequence of D; redefine func Del(fs,a) -> FinSequence of D; coherence proof rng fs c= D & rng Del(fs,a) c= rng fs by FINSEQ_1:def 4,FINSEQ_3:106; 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 FinSequence of D1; redefine func Del(fs,a) -> FinSequence of D1; 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,FINSEQ_1:40; 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,FINSEQ_1:40; end; suppose A18: b^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) by RVSUM_1:95; hence thesis by A2; end; end; suppose a>0 & a=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) by RVSUM_1:95 .=(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=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 by INT_1:def 3; (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 by RAT_1:15; 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) by INT_1:def 3; 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 by NAT_D:def 3; 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 by NAT_D:def 3; 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: f0; 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: f0; 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,NAT_D:def 3; d divides a by A6,A9,NAT_D:def 3; 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,INT_1:def 3; 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)) by INT_1:def 3; then n2 divides (x-m1) by A10,Th29; then consider t such that A12: n2*t=x-m1 by INT_1:def 3; 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 by NAT_D:def 3; (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) by NAT_D:def 3; 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 by NAT_D:def 3; then b=1 by Th15; then A28: b=1|^0; a divides 1 by A27,NAT_D:def 3; 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 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; A10: fr1.1=-m & fr1.2=n by FINSEQ_1:44; (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,A10, 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 by INT_1:25 .=0; end; suppose n=0; hence thesis by INT_1:def 10; 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 by Lm18; end; suppose n = 0; hence thesis by INT_1:def 10; 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 by INT_1:def 3; end; Lm21: (10 & 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,SQUARE_1:18; 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 asqrt 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) by NEWTON:64; then A18: 1<=v1 by A16,Lm1; reconsider v1 as Element of NAT by A16,A17,INT_1:3; ((k*((b-1) div d1)+((b-1) mod d1)) mod a) 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 by NEWTON:64; 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=0 by XREAL_1:48; then x1>=0 by A34,A33,PRE_FF:9; 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=-d by XREAL_1:24; take b=|.x.|, e=|.y.|; A41: y2>=0 by NEWTON:64; 1<=v2 by A23,FINSEQ_3:25; then v2-1>=0 by XREAL_1:48; then x2>=0 by A30,A33,PRE_FF:9; then x<=d by A38,Lm2; then A42: |.x.|<=d by A36,ABSVALUE:5; then A43: |.x.|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 by A1,INT_1:62; 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 qua Integer 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 A4: n = 0; k div 0 = 0 & (-k) div 0 = 0 by INT_1:48; hence thesis by A4; 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;