:: Factorial and Newton coefficients
:: by Rafa{\l} Kwiatek
::
:: Received July 27, 1990
:: Copyright (c) 1990-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, XREAL_0, ORDINAL1, FINSEQ_1, RELAT_1, FUNCT_1,
XXREAL_0, XBOOLE_0, SUBSET_1, ARYTM_3, TARSKI, FINSEQ_2, XCMPLX_0,
CARD_3, REAL_1, CARD_1, ORDINAL4, REALSET1, ARYTM_1, PARTFUN1, INT_2,
INT_1, FINSET_1, SQUARE_1, FUNCOP_1, NEWTON, VALUED_0, FUNCT_7, MEMBERED;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, FUNCT_1, PARTFUN1, FUNCT_2, MEMBERED, VALUED_0,
FINSET_1, FINSEQ_1, FINSEQ_2, FUNCOP_1, INT_1, INT_2, NAT_1, NAT_D,
RVSUM_1, SQUARE_1, XXREAL_0;
constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2,
FINSOP_1, RVSUM_1, FUNCOP_1, RELSET_1, FINSEQOP;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, RVSUM_1, VALUED_0,
CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, FINSEQ_1, SQUARE_1, FINSEQ_2, RVSUM_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, RVSUM_1, FINSEQ_1, FINSEQ_2, FUNCT_1, INT_1, XREAL_0,
XBOOLE_0, XCMPLX_1, INT_2, CARD_2, CARD_1, XBOOLE_1, XREAL_1, XCMPLX_0,
XXREAL_0, FINSOP_1, ORDINAL1, NAT_D, PARTFUN1, VALUED_1, FUNCOP_1,
ZFMISC_1, FINSEQ_3;
schemes NAT_1, FINSEQ_1, SUBSET_1, NAT_D;
begin
reserve i,j,k,n,m,l,s,t for Nat;
reserve a,b for Real;
reserve F for real-valued FinSequence;
theorem Th1:
n>=1 implies Seg n = {1} \/ {k where k is Element of NAT: 1<k & k <n} \/ {n}
proof
assume
A1: n>=1;
A2: {1} \/ {k where k is Element of NAT: 1<k & k<n} \/ {n} c= Seg n
proof
let d be object;
A3: {k where k is Element of NAT: 1<k & k<n} c= Seg n
proof
let d be object;
assume d in {k where k is Element of NAT: 1<k & k<n};
then ex k being Element of NAT st d = k & 1<k & k<n;
hence thesis;
end;
1 in Seg n by A1; then
{1} c= Seg n by ZFMISC_1:31; then
A4: {1} \/ {k where k is Element of NAT: 1<k & k<n} c= Seg n by A3,XBOOLE_1:8;
n in Seg n by A1; then
{n} c= Seg n by ZFMISC_1:31; then
{1} \/ {k where k is Element of NAT: 1<k & k<n} \/ {n} c= Seg n
by A4,XBOOLE_1:8;
hence thesis;
end;
Seg n c= {1} \/ {k where k is Element of NAT: 1<k & k<n} \/ {n}
proof
let d be object;
assume
A5: d in Seg n;
per cases by A1,XXREAL_0:1;
suppose
A6: n>1;
reconsider l = d as Element of NAT by A5;
A7: l <= n by A5,FINSEQ_1:1;
1 <= l by A5,FINSEQ_1:1;
then 1 = l or 1<l & l<n or l = n or 1 = n by A7,XXREAL_0:1;
then
d in {1} or d in {k where k is Element of NAT: 1<k & k<n} or d in {n
} by A6,TARSKI:def 1;
then
d in {1} \/ {k where k is Element of NAT: 1<k & k<n} or d in {n} by
XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
n = 1;
hence thesis by A5,FINSEQ_1:2,XBOOLE_0:def 3;
end;
end;
hence thesis by A2;
end;
theorem Th2:
len (a*F) = len F
proof
dom(a*F) = dom F by VALUED_1:def 5;
hence thesis by FINSEQ_3:29;
end;
theorem
dom F = dom (a*F) by VALUED_1:def 5;
:: x |^ n Function
registration
let x be Complex, n be natural Number;
cluster n |-> x -> complex-valued;
coherence;
end;
definition
let x be Complex, n be natural Number;
func x |^ n -> number equals
Product (n |-> x);
coherence by TARSKI:1;
end;
registration
let x be Real, n be natural Number;
cluster x |^ n -> real;
coherence;
end;
reserve z for Complex;
registration
let z be Complex, n be natural Number;
cluster z|^n -> complex;
coherence;
end;
theorem
z|^0 = 1 by RVSUM_1:94;
theorem Th5:
z|^1 = z
proof
thus z|^1 = Product(<*z*>) by FINSEQ_2:59
.= z;
end;
registration
let a be Complex;
reduce a |^ 1 to a;
reducibility by Th5;
end;
theorem Th6:
z|^(s+1) = z|^s * z
proof
thus z|^(s+1) = Product((s |-> z) ^ <*z*>) by FINSEQ_2:60
.= z|^s*z by RVSUM_1:96;
end;
registration
let x, n be natural Number;
cluster x|^n -> natural;
coherence
proof
A0: n is Nat by TARSKI:1;
defpred P[Nat] means x|^$1 is natural;
A1: for a being Nat st P[a] holds P[a+1]
proof
let a be Nat;
assume P[a];
then reconsider b = x|^a as Nat;
x|^(a+1) = b*x by Th6;
hence thesis;
end;
A2: P[0] by RVSUM_1:94;
for a being Nat holds P[a] from NAT_1:sch 2(A2,A1);
hence thesis by A0;
end;
end;
reserve x,y for Complex;
reserve r,s,t for natural Number;
theorem
(x*y) |^ s = x|^s * y|^s
proof
reconsider x, y as Element of COMPLEX by XCMPLX_0:def 2;
x|^s*y|^s = Product(s |-> (x*y)) by RVSUM_1:113;
hence thesis;
end;
theorem Th8:
x|^(s+t) = x|^s * x|^t
proof
reconsider x as Element of COMPLEX by XCMPLX_0:def 2;
x|^s*x|^t = Product((s+t) |-> x) by RVSUM_1:111;
hence thesis;
end;
theorem
(x|^s) |^ t = x|^(s*t)
proof
reconsider x as Element of COMPLEX by XCMPLX_0:def 2;
x|^(s*t) = Product(t |-> x|^s) by RVSUM_1:112;
hence thesis;
end;
theorem Th10:
1|^s = 1
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means 1|^$1 = 1;
A1: now
let s be Nat;
assume P[s];
then 1|^(s+1) = 1 * 1 by Th6;
hence P[s+1];
end;
A2: P[0] by RVSUM_1:94;
for s be Nat holds P[s] from NAT_1:sch 2(A2,A1);
hence thesis by A0;
end;
registration
let n be Nat;
reduce 1|^n to 1;
reducibility by Th10;
end;
theorem Th11:
s >= 1 implies 0|^s = 0
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means 0|^$1 = 0;
A1: now
let n be Nat;
assume n>=1 & P[n];
0|^(n+1) = 0|^n * 0 by Th6
.= 0;
hence P[n+1];
end;
A2: P[1];
for n be Nat st n >=1 holds P[n] from NAT_1:sch 8(A2,A1);
hence thesis by A0;
end;
:: n! Function
registration
let n be natural Number;
cluster idseq n -> natural-valued;
coherence
proof
reconsider n as Nat by TARSKI:1;
Seg n is natural-membered;
hence thesis;
end;
end;
definition
let n be natural Number;
func n! -> number equals
Product idseq n;
coherence by TARSKI:1;
end;
registration
let n be natural Number;
cluster n! -> real;
coherence;
end;
theorem Th12:
0! = 1 by RVSUM_1:94;
theorem
1! = 1 by FINSEQ_2:50;
theorem
2! = 2
proof
thus 2! = 1*2 by FINSEQ_2:52,RVSUM_1:99
.= 2;
end;
theorem Th15:
(s+1)! = (s!) * (s+1)
proof
idseq (s+1) = idseq s ^ <* s+1 *> by FINSEQ_2:51;
hence thesis by RVSUM_1:96;
end;
theorem Th16:
s! is Element of NAT
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means $1! is Element of NAT;
A1: now
let s be Nat;
assume P[s];
then reconsider k=s! as Element of NAT;
(s+1)! = (s+1) * k by Th15;
hence P[s+1];
end;
A2: P[0] by RVSUM_1:94;
for s be Nat holds P[s] from NAT_1:sch 2(A2,A1);
hence thesis by A0;
end;
registration
let n be natural Number;
cluster n! -> natural;
coherence by Th16;
end;
theorem Th17:
s! > 0
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means $1!>0;
A1: now
let s be Nat;
assume P[s];
then (s+1) * (s!)>(s+1) * 0;
hence P[s+1] by Th15;
end;
A2: P[0] by RVSUM_1:94;
for s be Nat holds P[s] from NAT_1:sch 2(A2,A1);
hence thesis by A0;
end;
registration
let n be natural Number;
cluster n! -> positive;
coherence by Th17;
end;
theorem
(s!) * (t!) <> 0;
:: n choose k Function
definition
let k,n be natural Number;
func n choose k -> number means
:Def3:
for l be Nat st l = n-k holds it = (n!)/((k!) * (l!)) if n >= k
otherwise it = 0;
consistency;
existence
proof
thus n >= k implies ex r1 be set st for l being Nat st l = n-k holds r1 =
(n!)/((k!) * (l!))
proof
assume n >= k;
then reconsider m = n-k as Element of NAT by INT_1:5;
take (n!)/((k!)*(m!));
thus thesis;
end;
thus thesis;
end;
uniqueness
proof
let r1,r2 be set;
thus n>=k & (for l being Nat st l = n-k holds r1 = (n!)/((k!) * (l!))) & (
for l being Nat st l = n-k holds r2 = (n!)/((k!) * (l!))) implies r1 = r2
proof
assume n>=k;
then reconsider m = n-k as Element of NAT by INT_1:5;
assume that
A1: for l being Nat st l = n-k holds r1 = (n!)/((k!) * (l!)) and
A2: for l being Nat st l = n-k holds r2 = (n!)/((k!) * (l!));
r1 = (n!)/((k!) * (m!)) by A1;
hence thesis by A2;
end;
thus thesis;
end;
end;
registration
let k,n be natural Number;
cluster n choose k -> real;
coherence
proof
per cases;
suppose
A1: n >= k;
then reconsider l = n-k as Element of NAT by INT_1:5;
n choose k = (n!)/((k!) * (l!)) by A1,Def3;
hence thesis;
end;
suppose n < k;
hence thesis by Def3;
end;
end;
end;
theorem Th19:
s choose 0 = 1
proof
reconsider m = s-0 as Element of NAT by ORDINAL1:def 12;
m = s;
then (s choose 0) = (s!)/(1 * (s!)) by Def3,Th12
.= 1 by XCMPLX_1:60;
hence thesis;
end;
theorem Th20:
s >= t & r = s-t implies s choose t = s choose r
proof
assume
A1: s>=t;
t-s>=0-s by XREAL_1:9;
then
A2: --s>=-(t-s) by XREAL_1:24;
assume
A3: r = s-t;
then t = s-r;
then s choose r = (s!)/((r!) * (t!)) by A2,Def3;
hence thesis by A1,A3,Def3;
end;
theorem Th21:
s choose s = 1
proof
reconsider m = s-s as Element of NAT by INT_1:5;
m = 0;
then s choose s = s choose 0 by Th20;
hence thesis by Th19;
end;
theorem Th22:
(t+1) choose (s+1) = (t choose (s+1)) + (t choose s)
proof
per cases by XXREAL_0:1;
suppose
A1: s<t;
thus ((t+1) choose (s+1)) = (t choose (s+1)) + (t choose s)
proof
reconsider m1 = t-s as Element of NAT by A1,INT_1:5;
A2: s+1<=t by A1,NAT_1:13;
then reconsider m2 = t-(s+1) as Element of NAT by INT_1:5;
A3: s+1<=t+1 by A1,XREAL_1:6;
then reconsider m = (t+1)-(s+1) as Element of NAT by INT_1:5;
(t choose (s+1)) = (t!)/(((s+1)!) * (m2!)) by A2,Def3;
then
A4: (t choose (s+1)) + (t choose s) = (t!)/(((s+1)!) * (m2!)) + (t!)/((s
!) * (m1!)) by A1,Def3
.= ((t!)*((s!)*(m1!))+(t!)*(((s+1)!)*(m2!)))/((((s+1)!)*(m2!))*((s!)
*(m1!))) by XCMPLX_1:116
.= (t!*((s!)*(m1!))+(t!)*(s!*(s+1)*(m2!)))/((((s+1)!)*(m2!))*((s!)*(
m1!))) by Th15
.= (s!*((t!)*((m1!)+(s+1)*(m2!))))/(s!*((m1!)*((s+1)!*(m2!))))
.=(t!*(((m2+1)!)+(s+1)*(m2!)))/(m1!*((s+1)!*(m2!))) by XCMPLX_1:91
.= (t!*((m2!)*(m2+1)+(m2!)*(s+1)))/(m1!*((s+1)!*(m2!))) by Th15
.= (m2!*((t!)*((m2+1)+(s+1))))/(m2!*(((s+1)!)*(m1!)))
.= ((t!)*(t-(s-(s+1))))/(((s+1)!)*(m1!)) by XCMPLX_1:91
.= ((t+1)!)/(((s+1)!)*(m1!)) by Th15;
m = m1;
hence thesis by A4,A3,Def3;
end;
end;
suppose
A5: s=t;
then s<t+1 by NAT_1:13;
then
A6: t choose (s+1)=0 by A5,Def3;
(t+1) choose (s+1)=1 by A5,Th21;
hence thesis by A5,A6,Th21;
end;
suppose
A7: s>t;
then s+1 >t+1 by XREAL_1:8;
then
A8: (t+1) choose (s+1)=0 by Def3;
A9: s+1>t+0 by A7,XREAL_1:8;
t choose s =0 by A7,Def3;
hence thesis by A9,A8,Def3;
end;
end;
theorem Th23:
s >= 1 implies s choose 1 = s
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means $1 choose 1 = $1;
A1: now
let n be Nat;
assume that
n>=1 and
A2: P[n];
(n+1) choose 1 = (n+1) choose (0+1) .= n + n choose 0 by A2,Th22
.= n+1 by Th19;
hence P[n+1];
end;
A3: P[1] by Th21;
for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(A3,A1);
hence thesis by A0;
end;
theorem
s>=1 & t = s-1 implies s choose t = s
proof
assume that
A1: s>=1 and
A2: t = s-1;
s choose t = s choose 1 by A1,A2,Th20;
hence thesis by A1,Th23;
end;
theorem Th25:
s choose r is Element of NAT
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means for r holds ($1 choose r) is Element of NAT;
A1: for s be Nat st P[s] holds P[s+1]
proof
let s be Nat;
assume
A2: P[s];
A3: for r st r <> 0 holds ((s+1) choose r) is Element of NAT
proof
let r;
assume
A4: r <> 0;
((s+1) choose r) is Element of NAT
proof
consider t being Nat such that
A5: r = t+1 by A4,NAT_1:6;
reconsider t as Element of NAT by ORDINAL1:def 12;
reconsider m1 = (s choose t), m2 = (s choose (t+1)) as Element of NAT
by A2;
m1 + m2 =(s choose t) + (s choose (t+1));
hence thesis by A5,Th22;
end;
hence thesis;
end;
let r;
r = 0 or r<>0;
hence thesis by A3,Th19;
end;
A6: P[0]
proof
let r;
r = 0 or r > 0;
hence thesis by Def3,Th19;
end;
for s be Nat holds P[s] from NAT_1:sch 2(A6,A1);
hence thesis by A0;
end;
theorem
for m,F st m <> 0 & len F = m & (for i,l st i in dom F & l = n+i-1
holds F.i = l choose n) holds Sum F = (n+m) choose (n+1)
proof
defpred P[Nat] means for F st $1 <> 0 & len F = $1 & (for i,l st i in dom F
& l = n+i-1 holds F.i = l choose n) holds Sum F = (n+$1) choose (n+1);
A1: for m st P[m] holds P[m+1]
proof
let m;
assume
A2: P[m];
let F;
assume that
m+1 <> 0 and
A3: len F = m+1 and
A4: for i,l st i in dom F & l = n+i-1 holds F.i = l choose n;
rng F c= REAL;
then F is FinSequence of REAL by FINSEQ_1:def 4;
then
consider G be FinSequence of REAL,x being Element of REAL such that
A5: F = G^<*x*> by A3,FINSEQ_2:19;
A6: m+1 = len G +1 by A3,A5,FINSEQ_2:16;
per cases;
suppose
A7: m = 0;
A8: n = n+1-1;
reconsider c = n choose n as Element of REAL by XREAL_0:def 1;
A9: dom F = Seg 1 by A3,A7,FINSEQ_1:def 3;
then 1 in dom F;
then F.1 = n choose n by A4,A8;
hence Sum F = Sum<*c*> by A9,FINSEQ_1:def 8
.= n choose n by FINSOP_1:11
.= 1 by Th21
.= (n+(m+1)) choose (n+1) by A7,Th21;
end;
suppose
A10: m <> 0;
A11: n+m = n +(m+1)-1;
A12: for i,l st i in dom G & l = n+i-1 holds G.i = l choose n
proof
A13: dom G c= dom F by A5,FINSEQ_1:26;
let i,l;
assume that
A14: i in dom G and
A15: l = n+i-1;
G.i = F.i by A5,A14,FINSEQ_1:def 7;
hence thesis by A4,A14,A15,A13;
end;
dom F = Seg (m+1) by A3,FINSEQ_1:def 3;
then
A16: (n+m) choose n = (G^<*x*>).(len G +1) by A4,A5,A6,A11,FINSEQ_1:4
.= x by FINSEQ_1:42;
thus Sum F = Sum G + x by A5,RVSUM_1:74
.= (n+m) choose (n+1) + (n+m) choose n by A2,A6,A10,A12,A16
.= (n+m+1) choose (n+1) by Th22
.= (n+(m+1)) choose (n+1);
end;
end;
A17: P[0];
thus for m holds P[m] from NAT_1:sch 2(A17,A1);
end;
registration
let k,n be natural Number;
cluster n choose k -> natural;
coherence by Th25;
end;
definition
let k,n be Nat;
redefine func n choose k -> Element of NAT; :: redefines choose (NEWTON, definition)
coherence by ORDINAL1:def 12;
end;
definition
let a,b be Real;
let n be natural Number;
func (a,b) In_Power n -> FinSequence of REAL means
:Def4:
len it = n+1 & for i,l,m being Nat st i in dom it & m = i - 1 & l = n-m holds
it.i = (n choose m) * a|^l * b|^m;
existence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
defpred P[Nat,object] means
for l,m be Nat st m = $1 - 1 & l = n-m holds $2 =
(n choose m)* a|^l * b|^m;
A1: for k be Nat st k in Seg(n+1) ex x being object st P[k,x]
proof
let k be Nat;
assume
A2: k in Seg (n+1);
then k >= 1 by FINSEQ_1:1;
then reconsider m1 = k-1 as Element of NAT by INT_1:5;
k <= n+1 by A2,FINSEQ_1:1;
then k-1<=n+1-1 by XREAL_1:9;
then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
take (n choose m1)*a|^l1*b|^m1;
thus thesis;
end;
consider p being FinSequence such that
A3: dom p = Seg(n+1) and
A4: for k be Nat st k in Seg(n+1) holds P[k,p.k] from FINSEQ_1:sch 1(A1);
rng p c= REAL
proof
let x be object;
assume x in rng p;
then consider y be object such that
A5: y in dom p and
A6: x = p.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A5;
y >= 1 by A3,A5,FINSEQ_1:1;
then reconsider m1 = y-1 as Element of NAT by INT_1:5;
y <= n+1 by A3,A5,FINSEQ_1:1;
then y-1<=n+1-1 by XREAL_1:9;
then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
p.y = (n choose m1) *a|^l1*b|^m1 by A3,A4,A5;
then reconsider x as Real by A6;
x in REAL by XREAL_0:def 1;
hence thesis;
end;
then reconsider p as FinSequence of REAL by FINSEQ_1:def 4;
take p;
thus thesis by A3,A4,FINSEQ_1:def 3;
end;
uniqueness
proof
let G,H be FinSequence of REAL;
assume that
A7: len G = n+1 and
A8: for i,l,m be Nat st i in dom G & m = i - 1 & l = n-m holds G.i =
(n choose m)* a|^l * b|^m;
assume that
A9: len H = n+1 and
A10: for i,l,m be Nat st i in dom H & m = i - 1 & l = n-m holds H.i =
(n choose m)* a|^l * b|^m;
for i st i in dom G holds G.i = H.i
proof
let i;
assume
A11: i in dom G;
then
A12: i in Seg (n+1) by A7,FINSEQ_1:def 3;
then i>=1 by FINSEQ_1:1;
then reconsider m = i-1 as Element of NAT by INT_1:5;
i<=n+1 by A12,FINSEQ_1:1;
then i-1<=n+1-1 by XREAL_1:9;
then reconsider l = n-m as Element of NAT by INT_1:5;
i in dom H by A9,A12,FINSEQ_1:def 3;
then H.i = (n choose m)* a|^l *b|^m by A10;
hence thesis by A8,A11;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
theorem Th27:
(a,b) In_Power 0 = <*1*>
proof
set F = (a,b) In_Power 0;
A1: len F = 0+1 by Def4
.= 1;
then
A2: dom F = {1} by FINSEQ_1:2,def 3;
then 1 in dom F by TARSKI:def 1;
then consider i be set such that
A3: i in dom F;
reconsider i as Element of NAT by A3;
A4: i = 1 by A2,A3,TARSKI:def 1;
then reconsider m1 = i-1 as Element of NAT by INT_1:5;
reconsider l1 = 0-m1 as Element of NAT by A4;
1 in dom (a,b) In_Power 0 by A2,TARSKI:def 1;
then F.1 = (0 choose 0)*a|^l1*b|^m1 by A4,Def4
.= 1*a|^0*b|^0 by A4,Th21
.= 1 by RVSUM_1:94;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th28:
((a,b) In_Power s).1 = a|^s
proof
reconsider m1 = 1-1 as Element of NAT by INT_1:5;
reconsider l1 = s-m1 as Nat;
len ((a,b) In_Power s) = s+1 by Def4;
then
A1: dom ((a,b) In_Power s) = Seg (s+1) by FINSEQ_1:def 3;
s+1>=0+1 by XREAL_1:6;
then 1 in dom ((a,b) In_Power s) by A1;
then ((a,b) In_Power s).1 = (s choose 0)*a|^l1*b|^m1 by Def4
.= 1*a|^l1*b|^m1 by Th19
.= a|^s by RVSUM_1:94;
hence thesis;
end;
theorem Th29:
((a,b) In_Power s).(s+1) = b|^s
proof
reconsider m1 = s+1-1 as Element of NAT by INT_1:5,NAT_1:12;
reconsider l1 = s-m1 as Element of NAT by INT_1:5;
len ((a,b) In_Power s) = s+1 by Def4;
then dom ((a,b) In_Power s) = Seg (s+1) by FINSEQ_1:def 3;
then s+1 in dom ((a,b) In_Power s) by FINSEQ_1:4;
then ((a,b) In_Power s).(s+1) = (s choose s)*a|^l1*b|^m1 by Def4
.= 1*a|^l1*b|^m1 by Th21
.= 1*b|^m1 by RVSUM_1:94
.= b|^s;
hence thesis;
end;
theorem Th30:
(a+b) |^ s = Sum((a,b) In_Power s)
proof
A0: s is Nat by TARSKI:1;
defpred P[Nat] means (a+b) |^ $1 = Sum((a,b) In_Power $1);
A1: for n st P[n] holds P[n+1]
proof
reconsider a, b as Element of REAL by XREAL_0:def 1;
let n;
reconsider G1 = ((a*((a,b) In_Power n))^<*In(0,REAL)*>)
as FinSequence of REAL;
set G2 = (<*In(0,REAL)*>^(b*((a,b) In_Power n)));
assume P[n];
then
A2: (a+b) |^ (n+1) = (a+b)*Sum((a,b) In_Power n) by Th6
.= a*Sum((a,b) In_Power n) + b*Sum((a,b) In_Power n)
.= Sum(a*((a,b) In_Power n)) + b*Sum((a,b) In_Power n) by RVSUM_1:87
.= Sum(a*((a,b) In_Power n)) + Sum(b*((a,b) In_Power n)) by RVSUM_1:87;
len G2 = len <*0*> + len (b*((a,b) In_Power n)) by FINSEQ_1:22
.= 1+ len (b*((a,b) In_Power n)) by FINSEQ_1:40
.= 1+ len ((a,b) In_Power n) by Th2
.= n+1+1 by Def4;
then reconsider F2 = G2 as Element of (n+1+1)-tuples_on REAL by FINSEQ_2:92
;
len G1 = len (a*((a,b) In_Power n)) + len <*0*> by FINSEQ_1:22
.= len (a*((a,b) In_Power n)) +1 by FINSEQ_1:40
.= len ((a,b) In_Power n) +1 by Th2
.= n+1+1 by Def4;
then reconsider F1 = G1 as Element of (n+1+1)-tuples_on REAL by FINSEQ_2:92
;
A3: Sum F2 = 0+ Sum(b*((a,b) In_Power n)) by RVSUM_1:76
.= Sum(b*((a,b) In_Power n));
Sum F1 = Sum(a*((a,b) In_Power n)) +0 by RVSUM_1:74
.= Sum(a*((a,b) In_Power n));
then
A4: Sum(G1+G2) = Sum(a*((a,b) In_Power n))+ Sum (b*((a,b) In_Power n)) by A3,
RVSUM_1:89;
set F = F1 + F2;
A5: len F2 = n+1+1 by CARD_1:def 7;
A6: len F = n+1+1 by CARD_1:def 7;
A7: len F1 = n+1+1 by CARD_1:def 7;
A8: for i st i in dom ((a,b) In_Power (n+1)) holds F.i = ((a,b) In_Power
(n+1)).i
proof
let i;
assume
A9: i in dom ((a,b) In_Power (n+1));
set r2 = F2/.i;
set r1 = F1/.i;
set r = ((a,b) In_Power n)/.i;
A10: len ((a,b) In_Power (n+1)) = n+1+1 by Def4;
then
A11: i in Seg (n+1+1) by A9,FINSEQ_1:def 3;
then
A12: i in dom F1 by A7,FINSEQ_1:def 3;
A13: i in dom F2 by A5,A11,FINSEQ_1:def 3;
A14: i in {1} implies F.i = ((a,b) In_Power (n+1)).i
proof
n+1>=0+1 by XREAL_1:6;
then 1 in Seg (n+1);
then 1 in Seg len (((a,b) In_Power n)) by Def4;
then
A15: 1 in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
then
A16: 1 in dom (a*((a,b) In_Power n)) by VALUED_1:def 5;
assume i in {1};
then
A17: i = 1 by TARSKI:def 1;
then
A18: r = ((a,b) In_Power n).1 by A15,PARTFUN1:def 6;
r = ((a,b) In_Power n).i by A17,A15,PARTFUN1:def 6;
then
A19: r = a|^n by A17,Th28;
A20: r1 = ((a*((a,b) In_Power n))^<*0*>).1 by A12,A17,PARTFUN1:def 6
.= (a*((a,b) In_Power n)).1 by A16,FINSEQ_1:def 7
.= a *a|^n by A18,A19,RVSUM_1:44
.= a|^(n+1) by Th6;
A21: r2 = F2.i by A13,PARTFUN1:def 6;
A22: r1 = F1.i by A12,PARTFUN1:def 6;
r2 = (<*0*>^(b*((a,b) In_Power n))).1 by A13,A17,PARTFUN1:def 6
.= 0 by FINSEQ_1:41;
then F.i = r1+0 by A22,A21,RVSUM_1:11
.= ((a,b) In_Power (n+1)).i by A17,A20,Th28;
hence thesis;
end;
i>=1 by A11,FINSEQ_1:1;
then reconsider j = i-1 as Element of NAT by INT_1:5;
set x = ((a,b) In_Power n)/.j;
A23: i = j+1;
A24: i in dom F by A6,A11,FINSEQ_1:def 3;
A25: i in {k where k is Element of NAT: k>1 & k<n+1+1} implies F.i = ((a
,b) In_Power (n+1)).i
proof
assume i in {k where k is Element of NAT: 1<k & k<n+1+1};
then
A26: ex k being Element of NAT st k=i & 1<k & k<n+1+1;
then reconsider m1 = i-1 as Element of NAT by INT_1:5;
A27: r1 = ((a*((a,b) In_Power n))^<*0*>).i by A12,PARTFUN1:def 6;
1<=j by A23,A26,NAT_1:13;
then reconsider m2 = j-1 as Element of NAT by INT_1:5;
A28: j<=n+1 by A23,A26,XREAL_1:6;
then j-1<=n+1-1 by XREAL_1:9;
then reconsider l2 = n-m2 as Element of NAT by INT_1:5;
1<=j by A23,A26,NAT_1:13;
then j in Seg (n+1) by A28;
then j in Seg len ((a,b) In_Power n) by Def4;
then
A29: j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
then
A30: x = ((a,b) In_Power n).j by PARTFUN1:def 6;
A31: i<=n+1 by A26,NAT_1:13;
then i in Seg (n+1) by A26;
then i in Seg len ((a,b) In_Power n) by Def4;
then
A32: i in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
then
A33: r = ((a,b) In_Power n).i by PARTFUN1:def 6;
i in dom (a*((a,b) In_Power n)) by A32,VALUED_1:def 5;
then
A34: r1 = (a*((a,b) In_Power n)).i by A27,FINSEQ_1:def 7
.= a*r by A33,RVSUM_1:44;
i-1<=n+1-1 by A31,XREAL_1:9;
then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
A35: l1+1 = n+1-(m2+1);
A36: j in dom (b*((a,b) In_Power n)) by A29,VALUED_1:def 5;
A37: r2 = (<*0*>^(b*((a,b) In_Power n))).i by A13,PARTFUN1:def 6;
then r2 = (<*0*>^(b*((a,b) In_Power n))).(len <*0*> +j) by A23,
FINSEQ_1:40
.= (b*((a,b) In_Power n)).j by A36,FINSEQ_1:def 7
.= b*x by A30,RVSUM_1:44;
then F.i = a*r + b*x by A24,A27,A37,A34,VALUED_1:def 1
.= a*(a|^l1*(n choose m1)*b|^m1) + b*x by A32,A33,Def4
.= a*a|^l1*((n choose m1)*b|^m1) + b*x
.= a|^(l1+1)*((n choose m1)*b|^m1) + b*x by Th6
.= a|^(l1+1)*((n choose m1)*b|^m1) + b*(b|^m2*((n choose m2)*a|^l2
)) by A29,A30,Def4
.= a|^(l1+1)*((n choose m1)*b|^m1) + b*b|^m2*((n choose m2)*a|^l2)
.= a|^(l1+1)*((n choose (m2+1))*b|^(m2+1)) + b|^(m2+1)*((n choose
m2)*a|^l2) by Th6
.= ((n choose (m2+1)) + (n choose m2))*a|^(l1+1)*b|^(m2+1)
.= ((n+1) choose (m2+1))*a|^(l1+1)*b|^(m2+1) by Th22
.= ((a,b) In_Power (n+1)).i by A9,A35,Def4;
hence thesis;
end;
A38: i in {n+1+1} implies F.i = ((a,b) In_Power (n+1)).i
proof
assume
A39: i in {n+1+1};
then
A40: i = n+1+1 by TARSKI:def 1;
A41: j = n+1+1-1 by A39,TARSKI:def 1
.= n+1;
n+1 in Seg (n+1) by FINSEQ_1:4;
then j in Seg len (((a,b) In_Power n)) by A41,Def4;
then
A42: j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
then
A43: x = ((a,b) In_Power n).(n+1) by A41,PARTFUN1:def 6
.= b|^n by Th29;
A44: x = ((a,b) In_Power n).j by A42,PARTFUN1:def 6;
A45: j in dom (b*((a,b) In_Power n)) by A42,VALUED_1:def 5;
A46: r2 = (<*0*>^(b*((a,b) In_Power n))).(1+n+1) by A13,A40,PARTFUN1:def 6
.= (<*0*>^(b*((a,b) In_Power n))).(len <*0*> +j) by A41,FINSEQ_1:39
.= (b*((a,b) In_Power n)).j by A45,FINSEQ_1:def 7
.= b*b|^n by A44,A43,RVSUM_1:44
.= b|^(n+1) by Th6;
A47: r2 = F2.i by A13,PARTFUN1:def 6;
n+1 = len ((a,b) In_Power n) by Def4
.= len (a*((a,b) In_Power n)) by Th2;
then
A48: r1 = ((a*((a,b) In_Power n))^<*0*>).(len (a*((a,b) In_Power n))+1
) by A12,A40,PARTFUN1:def 6
.= 0 by FINSEQ_1:42;
r1 = F1.i by A12,PARTFUN1:def 6;
then F.i = 0+r2 by A48,A47,RVSUM_1:11
.= ((a,b) In_Power (n+1)).i by A40,A46,Th29;
hence thesis;
end;
A49: now
assume
i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} \/ { n+1+1};
then i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} or i in
{n+1+1} by XBOOLE_0:def 3;
hence thesis by A14,A25,A38,XBOOLE_0:def 3;
end;
dom ((a,b) In_Power (n+1)) = Seg (n+1+1) by A10,FINSEQ_1:def 3;
hence thesis by A9,A49,Th1,NAT_1:12;
end;
len ((a,b) In_Power (n+1)) = len F by A6,Def4;
hence thesis by A2,A4,A8,FINSEQ_2:9;
end;
(a+b) |^ 0 = Sum<*In(1,REAL)*> by FINSOP_1:11,RVSUM_1:94
.= Sum((a,b) In_Power 0) by Th27;
then
A50: P[0];
for n holds P[n] from NAT_1:sch 2(A50,A1);
hence thesis by A0;
end;
definition
let n be natural Number;
func Newton_Coeff n -> FinSequence of REAL means
:Def5:
len it = n+1 & for i,k be Nat st i in dom it & k = i-1 holds
it.i = n choose k;
existence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
defpred P[Nat,object] means
for s st s = $1-1 holds $2 = n choose s;
A1: for l be Nat st l in Seg (n+1) ex x being object st P[l,x]
proof
let l be Nat;
assume l in Seg (n+1);
then l>=1 by FINSEQ_1:1;
then reconsider k = l-1 as Element of NAT by INT_1:5;
set x = n choose k;
take x;
thus thesis;
end;
consider F being FinSequence such that
A2: dom F = Seg (n+1) & for l be Nat st l in Seg (n+1) holds P[l,F.l]
from FINSEQ_1:sch 1(A1);
rng F c= REAL
proof
let x be object;
assume x in rng F;
then consider y be object such that
A3: y in dom F and
A4: x = F.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A3;
y >= 1 by A2,A3,FINSEQ_1:1;
then reconsider m1 = y-1 as Element of NAT by INT_1:5;
F.y = n choose m1 by A2,A3;
then reconsider x as Real by A4;
x in REAL by XREAL_0:def 1;
hence thesis;
end;
then reconsider F as FinSequence of REAL by FINSEQ_1:def 4;
take F;
thus thesis by A2,FINSEQ_1:def 3;
end;
uniqueness
proof
let G,H be FinSequence of REAL;
assume that
A5: len G = n+1 and
A6: for i,m be Nat st i in dom G & m = i - 1 holds G.i = n choose m;
assume that
A7: len H = n+1 and
A8: for i,m be Nat st i in dom H & m = i - 1 holds H.i = n choose m;
for i st i in dom G holds G.i = H.i
proof
let i;
assume
A9: i in dom G;
then
A10: i in Seg (n+1) by A5,FINSEQ_1:def 3;
then i>=1 by FINSEQ_1:1;
then reconsider m = i-1 as Element of NAT by INT_1:5;
i in dom H by A7,A10,FINSEQ_1:def 3;
then H.i = n choose m by A8;
hence thesis by A6,A9;
end;
hence thesis by A5,A7,FINSEQ_2:9;
end;
end;
theorem Th31:
Newton_Coeff s = (1,1) In_Power s
proof
A1: for i st i in dom (Newton_Coeff s) holds (Newton_Coeff s).i = ((1,1)
In_Power s).i
proof
let i;
assume
A2: i in dom (Newton_Coeff s);
A3: dom (Newton_Coeff s) = Seg len (Newton_Coeff s) by FINSEQ_1:def 3
.= Seg (s+1) by Def5;
then i>=1 by A2,FINSEQ_1:1;
then reconsider m1 = i-1 as Element of NAT by INT_1:5;
i<=(s+1) by A2,A3,FINSEQ_1:1;
then s+1-1>=i-1 by XREAL_1:9;
then reconsider l1 = s-m1 as Element of NAT by INT_1:5;
dom (Newton_Coeff s) = Seg len ((1,1) In_Power s) by A3,Def4
.= dom ((1,1) In_Power s) by FINSEQ_1:def 3;
then ((1,1) In_Power s).i = (s choose m1)*1|^l1*1|^m1 by A2,Def4
.= (Newton_Coeff s).i by A2,Def5;
hence thesis;
end;
len (Newton_Coeff s) = s+1 by Def5
.= len ((1,1) In_Power s) by Def4;
hence thesis by A1,FINSEQ_2:9;
end;
theorem
2|^s = Sum(Newton_Coeff s)
proof
2|^s = (1+1) |^ s .= Sum((1,1) In_Power s) by Th30
.= Sum(Newton_Coeff s) by Th31;
hence thesis;
end;
begin :: Addenda
:: from NAT_LAT
theorem Th33:
l >= 1 implies k*l >= k
proof
assume
A1: l>=1;
for k holds k*l>=k
proof
defpred P[Nat] means $1*l>=$1;
A2: for k st P[k] holds P[k+1]
proof
let k;
A3: (k + 1)*l = k * l + 1*l;
A4: k+l>=k+1 by A1,XREAL_1:7;
assume k*l>=k;
then (k+1)*l>=k+l by A3,XREAL_1:7;
hence (k+1)*l>=k+1 by A4,XXREAL_0:2;
end;
A5: P[0];
thus for k holds P[k] from NAT_1:sch 2(A5,A2);
end;
hence thesis;
end;
theorem Th34:
l >= 1 & n >= k*l implies n >= k
proof
assume that
A1: l>=1 and
A2: n>=k*l;
k*l>=k by A1,Th33;
hence thesis by A2,XXREAL_0:2;
end;
definition
let n;
redefine func n! -> Element of NAT; :: redefines ! (NEWTON, definition)
coherence by Th16;
end;
theorem Th35:
l <> 0 implies l divides l!
proof
assume l<>0;
then consider n being Nat such that
A1: l = n+1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
(n+1)! = (n+1) * (n!) by Th15;
hence thesis by A1,NAT_D:def 3;
end;
theorem
n <> 0 implies (n+1)/n > 1
proof
assume
A1: n<>0;
(n+1)/n=n/n+1/n by XCMPLX_1:62
.=1+1/n by A1,XCMPLX_1:60;
hence thesis by A1,XREAL_1:29;
end;
theorem Th37:
k/(k+1) < 1
proof
m < m+1 by XREAL_1:29;
hence thesis by XREAL_1:189;
end;
theorem Th38:
l! >= l
proof
defpred P[Nat] means $1! >= $1;
A1: for l st P[l] holds P[l+1]
proof
let l;
assume
A2: l!>=l;
A3: l!*(l+1)=(l+1)! by Th15;
l=0 & (l+1)!>=(l+1) or l>=1 & (l+1)!>=(l+1)
proof
per cases by NAT_1:14;
case
l=0;
hence thesis by FINSEQ_2:50;
end;
case
A4: l>=1;
(l+1)!>=(l+1)*l by A2,A3,XREAL_1:64;
hence thesis by A4,Th34;
end;
end;
hence thesis;
end;
A5: P[0];
for l being Nat holds P[l] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th39:
m<>1 & m divides n implies not m divides (n+1)
proof
assume that
A1: m<>1 and
A2: m divides n and
A3: m divides (n+1);
consider t being Nat such that
A4: n = m * t by A2,NAT_D:def 3;
consider s being Nat such that
A5: n+1 = m * s by A3,NAT_D:def 3;
t <= s
proof
(n+1)*t=m*s*t by A5
.= n*s by A4;
then
A6: t=n*s/(n+1) by XCMPLX_1:89
.=s*(n/(n+1)) by XCMPLX_1:74;
assume
A7: t > s;
s>0 by A5;
hence contradiction by A7,A6,Th37,XREAL_1:157;
end;
then reconsider r =s-t as Element of NAT by INT_1:5;
1=m*s-m*t by A4,A5;
then 1=m*r;
hence contradiction by A1,NAT_1:15;
end;
theorem Th40:
j<>0 implies j divides (j+k)!
proof
defpred P[Nat] means for j st j<>0 holds j divides (j+$1)!;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: for j st j<>0 holds j divides (j+k)!;
let j;
assume j<>0;
then j divides ((j+k)!)*((j+k)+1) by A2,NAT_D:9;
hence thesis by Th15;
end;
A3: P[0] by Th35;
for k holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th41:
j<=l & j<>0 implies j divides l!
proof
assume that
A1: j<=l and
A2: j<>0;
ex k being Nat st l=j+k by A1,NAT_1:10;
hence thesis by A2,Th40;
end;
theorem
j<>1 & j<>0 & j divides (l!+1) implies j>l by Th39,Th41;
:: The fundamental properties of lcm, hcf
theorem
m lcm (n lcm k) = (m lcm n) lcm k
proof
set M = n lcm k;
set K = m lcm M;
set N = m lcm n;
set L = N lcm k;
A1: m divides K by NAT_D:def 4;
A2: M divides K by NAT_D:def 4;
n divides M by NAT_D:def 4;
then n divides K by A2,NAT_D:4;
then
A3: N divides K by A1,NAT_D:def 4;
k divides M by NAT_D:def 4;
then k divides K by A2,NAT_D:4;
then
A4: L divides K by A3,NAT_D:def 4;
A5: N divides L by NAT_D:def 4;
A6: k divides L by NAT_D:def 4;
n divides N by NAT_D:def 4;
then n divides L by A5,NAT_D:4;
then
A7: M divides L by A6,NAT_D:def 4;
m divides N by NAT_D:def 4;
then m divides L by A5,NAT_D:4;
then K divides L by A7,NAT_D:def 4;
hence thesis by A4,NAT_D:5;
end;
theorem Th44:
m divides n iff m lcm n = n
proof
thus m divides n implies m lcm n = n
proof
set M = m lcm n;
assume m divides n;
then
A1: M divides n by NAT_D:def 4;
n divides M by NAT_D:def 4;
hence thesis by A1,NAT_D:5;
end;
thus thesis by NAT_D:def 4;
end;
theorem
n divides m & k divides m iff n lcm k divides m
proof
n lcm k divides m implies n divides m & k divides m
proof
set M = n lcm k;
A1: n divides M by NAT_D:def 4;
A2: k divides M by NAT_D:def 4;
assume n lcm k divides m;
hence thesis by A1,A2,NAT_D:4;
end;
hence thesis by NAT_D:def 4;
end;
theorem
m lcm 1 = m
proof
set M = m lcm 1;
1 divides m by NAT_D:6;
then
A1: M divides m by NAT_D:def 4;
m divides M by NAT_D:def 4;
hence thesis by A1,NAT_D:5;
end;
theorem Th47:
m lcm n divides m*n
proof
set s=m*n;
A1: n divides s by NAT_D:9;
m divides s by NAT_D:9;
hence thesis by A1,NAT_D:def 4;
end;
theorem
m gcd (n gcd k) = (m gcd n) gcd k
proof
set M = n gcd k;
set K = m gcd M;
set N = m gcd n;
set L = N gcd k;
A1: K divides M by NAT_D:def 5;
A2: K divides m by NAT_D:def 5;
M divides n by NAT_D:def 5;
then K divides n by A1,NAT_D:4;
then
A3: K divides N by A2,NAT_D:def 5;
A4: L divides N by NAT_D:def 5;
A5: L divides k by NAT_D:def 5;
N divides n by NAT_D:def 5;
then L divides n by A4,NAT_D:4;
then
A6: L divides M by A5,NAT_D:def 5;
N divides m by NAT_D:def 5;
then L divides m by A4,NAT_D:4;
then
A7: L divides K by A6,NAT_D:def 5;
M divides k by NAT_D:def 5;
then K divides k by A1,NAT_D:4;
then K divides L by A3,NAT_D:def 5;
hence thesis by A7,NAT_D:5;
end;
theorem Th49:
n divides m implies n gcd m = n
proof
set N = n gcd m;
assume n divides m;
then
A1: n divides N by NAT_D:def 5;
N divides n by NAT_D:def 5;
hence thesis by A1,NAT_D:5;
end;
theorem
m divides n & m divides k iff m divides n gcd k
proof
m divides n gcd k implies m divides n & m divides k
proof
set M = n gcd k;
A1: M divides n by NAT_D:def 5;
A2: M divides k by NAT_D:def 5;
assume m divides n gcd k;
hence thesis by A1,A2,NAT_D:4;
end;
hence thesis by NAT_D:def 5;
end;
theorem
m gcd 1 = 1
proof
set M = m gcd 1;
A1: 1 divides M by NAT_D:6;
M divides 1 by NAT_D:def 5;
hence thesis by A1,NAT_D:5;
end;
theorem
m gcd 0 = m
proof
set M = m gcd 0;
m divides 0 by NAT_D:6;
then
A1: m divides M by NAT_D:def 5;
M divides m by NAT_D:def 5;
hence thesis by A1,NAT_D:5;
end;
theorem Th53:
(m gcd n) lcm n = n
proof
set M = m gcd n;
M divides n by NAT_D:def 5;
hence thesis by Th44;
end;
theorem Th54:
m gcd (m lcm n) = m
proof
set M = m lcm n;
m divides M by NAT_D:def 4;
hence thesis by Th49;
end;
theorem
m gcd (m lcm n) = (n gcd m) lcm m
proof
m gcd (m lcm n) = m by Th54;
hence thesis by Th53;
end;
theorem
m divides n implies m gcd k divides n gcd k
proof
set M = m gcd k;
A1: M divides k by NAT_D:def 5;
assume
A2: m divides n;
M divides m by NAT_D:def 5;
then M divides n by A2,NAT_D:4;
hence thesis by A1,NAT_D:def 5;
end;
theorem
m divides n implies k gcd m divides k gcd n
proof
set M = k gcd m;
A1: M divides k by NAT_D:def 5;
assume
A2: m divides n;
M divides m by NAT_D:def 5;
then M divides n by A2,NAT_D:4;
hence thesis by A1,NAT_D:def 5;
end;
theorem Th58:
for m,n being Integer holds
n > 0 implies n gcd m > 0
proof
let m,n be Integer;
assume that
A1: n>0 and
A2: n gcd m <= 0;
A3: n gcd m divides n by INT_2:def 2;
n gcd m = 0 or n gcd m < 0 by A2;
then ex r being Integer st n = 0*r by A3,INT_1:def 3;
hence contradiction by A1;
end;
theorem
m > 0 & n > 0 implies m lcm n > 0
proof
assume that
A1: m>0 and
A2: n>0 and
A3: m lcm n <= 0;
A4: (m lcm n) divides m*n by Th47;
m lcm n = 0 or m lcm n < 0 by A3;
then ex r being Nat st m*n = 0*r by A4,NAT_D:def 3;
hence contradiction by A1,A2;
end;
theorem
(n gcd m) lcm (n gcd k) divides n gcd (m lcm k)
proof
set M = m lcm k;
set N = n gcd k;
set P = n gcd m;
set L = P lcm N;
A1: N divides k by NAT_D:def 5;
k divides M by NAT_D:def 4;
then
A2: N divides M by A1,NAT_D:4;
A3: P divides m by NAT_D:def 5;
m divides M by NAT_D:def 4;
then P divides M by A3,NAT_D:4;
then
A4: L divides M by A2,NAT_D:def 4;
A5: P divides n by NAT_D:def 5;
N divides n by NAT_D:def 5;
then L divides n by A5,NAT_D:def 4;
hence thesis by A4,NAT_D:def 5;
end;
theorem
m divides l implies m lcm (n gcd l) divides (m lcm n) gcd l
proof
set M = m lcm n;
set K = M gcd l;
set N = n gcd l;
A1: m divides M by NAT_D:def 4;
A2: N divides n by NAT_D:def 5;
A3: N divides l by NAT_D:def 5;
n divides M by NAT_D:def 4;
then N divides M by A2,NAT_D:4;
then
A4: N divides K by A3,NAT_D:def 5;
assume m divides l;
then m divides K by A1,NAT_D:def 5;
hence thesis by A4,NAT_D:def 4;
end;
theorem
n gcd m divides n lcm m
proof
A1: n divides n lcm m by NAT_D:def 4;
n gcd m divides n by NAT_D:def 5;
hence thesis by A1,NAT_D:4;
end;
:: from GR_CY_2
reserve p,q for natural Number;
reserve i0,i,i1,i2,i4 for Integer;
theorem
0 < m implies n mod m = n - m * (n div m)
proof
reconsider z1=m * (n div m),z2=(n mod m) as Integer;
assume m > 0;
then n - z1 = z1 + z2 -z1 by NAT_D:2;
hence thesis;
end;
theorem
i2 >= 0 implies i1 mod i2 >= 0;
theorem
i2 > 0 implies i1 mod i2 < i2 by INT_1:58;
theorem
i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2) by INT_1:59;
::$N Bezout's identity
::$L https://en.wikipedia.org/wiki/Bézout's_theorem Bezout's theorem
theorem
ex i,i1 st i*m + i1*n = m gcd n by NAT_D:68;
:: from NAT_LAT
definition
func SetPrimes -> Subset of NAT means
:Def6:
for n being Nat holds n in it iff n is prime;
existence
proof
defpred P[Nat] means $1 is prime;
consider X being Subset of NAT such that
A1: for n being Element of NAT holds n in X iff P[n] from SUBSET_1:sch 3;
take X;
let n be Nat;
thus n in X implies n is prime by A1;
assume
A2: n is prime;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,A2;
end;
uniqueness
proof
let A, B be Subset of NAT such that
A3: for n being Nat holds n in A iff n is prime and
A4: for n being Nat holds n in B iff n is prime;
thus A c= B
by A3,A4;
let x be object;
assume
A5: x in B;
then reconsider x as Element of NAT;
x is prime by A4,A5;
hence thesis by A3;
end;
end;
registration
cluster prime for Element of NAT;
existence by INT_2:28;
end;
reserve x for set;
definition
let p be natural Number;
func SetPrimenumber p -> Subset of NAT means
:Def7:
for q being Nat holds q in it iff q < p & q is prime;
existence
proof
defpred P[Nat] means $1 < p & $1 is prime;
consider X being Subset of NAT such that
A1: for q being Element of NAT holds q in X iff P[q] from SUBSET_1:sch 3;
take X;
let q be Nat;
thus q in X implies q < p & q is prime by A1;
assume that
A2: q < p and
A3: q is prime;
q in NAT by ORDINAL1:def 12;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let A, B be Subset of NAT such that
A4: for q being Nat holds q in A iff q < p & q is prime and
A5: for q being Nat holds q in B iff q < p & q is prime;
thus A c= B
proof
let x be object;
assume
A6: x in A;
then reconsider x as Element of NAT;
A7: x is prime by A4,A6;
x < p by A4,A6;
hence thesis by A5,A7;
end;
let x be object;
assume
A8: x in B;
then reconsider x as Element of NAT;
A9: x is prime by A5,A8;
x < p by A5,A8;
hence thesis by A4,A9;
end;
end;
theorem Th68:
SetPrimenumber p c= SetPrimes
proof
let x be object;
assume
A1: x in SetPrimenumber p;
then reconsider x9 = x as Element of NAT;
x9 is prime by A1,Def7;
hence thesis by Def6;
end;
theorem
p <= q implies SetPrimenumber p c= SetPrimenumber q
proof
assume
A1: p <= q;
let x be object;
assume
A2: x in SetPrimenumber p;
then reconsider x9 = x as Element of NAT;
x9 < p by A2,Def7;
then
A3: x9 < q by A1,XXREAL_0:2;
x9 is prime by A2,Def7;
hence thesis by A3,Def7;
end;
theorem Th70:
SetPrimenumber p c= Seg p
proof
let x be object;
assume
A1: x in SetPrimenumber p;
then reconsider q = x as Element of NAT;
q is prime by A1,Def7;
then
A2: 1 <= q by INT_2:def 4;
q < p by A1,Def7;
hence thesis by A2;
end;
theorem Th71:
SetPrimenumber p is finite
proof
SetPrimenumber p c= Seg p by Th70;
hence thesis;
end;
registration
let n be natural Number;
cluster SetPrimenumber n -> finite;
coherence by Th71;
end;
reserve p for Prime;
theorem Th72:
for l being Nat ex p being Prime st p > l
proof
let l be Nat;
reconsider two = 2 as Prime by INT_2:28;
reconsider l as Element of NAT by ORDINAL1:def 12;
l=0 & (ex p st p is prime & p>l) or l=1 & (ex p st p is prime & p>l) or
2<=l & ex p st p is prime & p>l
proof
l <= 2 implies l = 0 or ... or l = 2;
then per cases;
case
A1: l=0;
take two;
thus thesis by A1;
end;
case
A2: l=1;
take two;
thus thesis by A2;
end;
case
A3: 2<=l;
l<=l! by Th38;
then 2<=l! by A3,XXREAL_0:2;
then (2+0) <= (l!+1) by XREAL_1:7;
then consider j being Element of NAT such that
A4: j is prime and
A5: j divides (l!+1) by INT_2:31;
reconsider j9=j as Prime by A4;
take j9;
A6: j<>0 by A4,INT_2:def 4;
j<>1 by A4,INT_2:def 4;
hence thesis by A5,A6,Th39,Th41;
end;
end;
hence thesis;
end;
Lm1:
SetPrimenumber 2 = {}
proof
assume SetPrimenumber 2<>{};
then consider x being object such that
A1: x in SetPrimenumber 2 by XBOOLE_0:def 1;
reconsider x as Nat by A1;
A2: x is prime by A1,Def7;
x<1+1 by A1,Def7;
then x <= 1 by NAT_1:13;
then 0 is prime or 1 is prime by A2,NAT_1:25;
hence contradiction by INT_2:def 4;
end;
registration
cluster SetPrimes -> non empty;
coherence by Def6,INT_2:28;
end;
registration
cluster SetPrimenumber 2 -> empty;
coherence by Lm1;
end;
theorem
SetPrimenumber m c= Seg m
proof
let x be object;
assume
A1: x in SetPrimenumber m;
then reconsider x as Element of NAT;
x is prime by A1,Def7;
then
A2: 1 <= x by INT_2:def 4;
x < m by A1,Def7;
hence thesis by A2;
end;
theorem
k>=m implies not k in SetPrimenumber m by Def7;
theorem
SetPrimenumber n \/ {n} is finite;
theorem Th76:
for f being Prime, g being Nat st f < g holds SetPrimenumber f
\/ {f} c= SetPrimenumber g
proof
let f be Prime,g be Nat;
assume
A1: f<g;
let x be object;
assume
A2: x in SetPrimenumber f\/{f};
then reconsider x as Nat;
per cases by A2,XBOOLE_0:def 3;
suppose
A3: x in SetPrimenumber f;
then x < f by Def7;
then
A4: x < g by A1,XXREAL_0:2;
x is prime by A3,Def7;
hence thesis by A4,Def7;
end;
suppose
x in {f};
then x = f by TARSKI:def 1;
hence thesis by A1,Def7;
end;
end;
theorem
k>=m implies not k in SetPrimenumber m by Def7;
Lm2: SetPrimenumber n = {k where k is Element of NAT:k<n & k is prime}
proof
thus SetPrimenumber n c= {k where k is Element of NAT:k<n & k is prime}
proof
let x be object;
assume
A1: x in SetPrimenumber n;
then reconsider x as Element of NAT;
A2: x is prime by A1,Def7;
x < n by A1,Def7;
hence thesis by A2;
end;
let x be object;
assume x in {k where k is Element of NAT:k<n & k is prime};
then ex k be Element of NAT st x=k & k<n & k is prime;
hence thesis by Def7;
end;
definition
let n be Nat;
func primenumber n -> prime Element of NAT means
:Def8:
n = card SetPrimenumber it;
existence
proof
defpred P1[Nat] means ex m st $1=card SetPrimenumber m & m is Prime;
A1: for n st P1[n] holds P1[n+1]
proof
let n;
given m such that
A2: n=card SetPrimenumber m and
A3: m is Prime;
defpred P[Nat] means $1 is prime & $1>m;
A4: not m in SetPrimenumber m by Def7;
A5: ex k be Nat st P[k]
proof
ex p st p>m by Th72;
hence thesis;
end;
consider k be Nat such that
A6: P[k] & for l be Nat st P[l] holds k <= l from NAT_1:sch 5(A5);
take k;
A7: SetPrimenumber k c= SetPrimenumber m\/{m}
proof
let s be object;
assume
A8: s in SetPrimenumber k;
then reconsider s as Element of NAT;
A9: s is prime by A8,Def7;
s<k by A8,Def7;
then
A10: s<=m by A6,A9;
per cases by A10,XXREAL_0:1;
suppose
s=m;
then s in {m} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A11: s<m;
A12: SetPrimenumber m c= SetPrimenumber m\/{m} by XBOOLE_1:7;
s in SetPrimenumber m by A9,A11,Def7;
hence thesis by A12;
end;
end;
SetPrimenumber m\/{m} c= SetPrimenumber k by A3,A6,Th76;
then SetPrimenumber k=SetPrimenumber m\/{m} by A7;
hence n + 1 = card SetPrimenumber k by A2,A4,CARD_2:41;
thus thesis by A6;
end;
SetPrimenumber 2 = {k where k is Element of NAT:k<2 & k is prime} by Lm2;
then
A13: P1[0] by CARD_1:27,INT_2:28;
for n holds P1[n] from NAT_1:sch 2(A13,A1);
then consider m such that
A14: n=card SetPrimenumber m and
A15: m is Prime;
m in NAT by ORDINAL1:def 12;
hence thesis by A14,A15;
end;
uniqueness
proof
let f,g be prime Element of NAT;
assume that
A16: n = card SetPrimenumber f and
A17: n = card SetPrimenumber g;
assume
A18: f<>g;
f<g & n+1 <= n or g<f & n+1 <= n
proof
per cases by A18,XXREAL_0:1;
case
A19: f<g;
A20: not f in SetPrimenumber f by Def7;
card (SetPrimenumber f\/{f}) <= card SetPrimenumber g by A19,Th76,
NAT_1:43;
hence thesis by A16,A17,A20,CARD_2:41;
end;
case
A21: g<f;
A22: not g in SetPrimenumber g by Def7;
card (SetPrimenumber g\/{g}) <= card SetPrimenumber f by A21,Th76,
NAT_1:43;
hence thesis by A16,A17,A22,CARD_2:41;
end;
end;
hence contradiction by NAT_1:13;
end;
end;
theorem
SetPrimenumber n = {k where k is Element of NAT: k<n & k is prime} by Lm2;
::$N The Infinitude of Primes
::$L https://en.wikipedia.org/wiki/Prime_number#Infinitude The Infinitude of Primes
theorem Th79:
SetPrimes is infinite
proof
assume
A1: SetPrimes is finite;
then reconsider SP = SetPrimes as finite set;
consider n be Nat such that
A2: SetPrimes,Seg n are_equipotent by A1,FINSEQ_1:56;
card SetPrimes = card Seg n by A2,CARD_1:5;
then card SetPrimes = card n by FINSEQ_1:55;
then
A3: card SP = n;
set p=primenumber (n+1);
set SPp = SetPrimenumber p;
A4: n+1 = card SetPrimenumber p by Def8;
card SPp <= card SP by Th68,NAT_1:43;
hence contradiction by A3,A4,NAT_1:13;
end;
registration
cluster SetPrimes -> infinite;
coherence by Th79;
end;
reserve i for Nat;
:: divisibility
theorem
i is prime implies for m,n being Nat holds i divides m * n implies
i divides m or i divides n
proof
defpred P[Nat] means $1 is prime & ex m,n being Nat st $1 divides m * n &
not $1 divides m & not $1 divides n;
assume
A1: i is prime;
given m,n being Nat such that
A2: i divides m * n and
A3: not( (i divides m or i divides n));
A4: ex i be Nat st P[i] by A1,A2,A3;
consider p9 being Nat such that
A5: P[p9] and
A6: for p1 being Nat st P[p1] holds p9 <= p1 from NAT_1:sch 5(A4);
defpred Q[Nat] means ex n being Nat st p9 divides $1 * n & not p9 divides $1
& not p9 divides n;
A7: ex i be Nat st Q[i] by A5;
consider m be Nat such that
A8: Q[m] and
A9: for m1 being Nat st Q[m1] holds m <= m1 from NAT_1:sch 5(A7);
A10: m > 0 by A8;
consider n being Nat such that
A11: p9 divides m * n and
A12: not p9 divides m and
A13: not p9 divides n by A8;
A14: m < p9
proof
set m1 = m mod p9;
assume
A15: m >= p9;
A16: p9 > 0 by A5,INT_2:def 4;
then m = p9* (m div p9) + m1 by NAT_D:2;
then
A17: m * n = p9 * (m div p9) * n + m1 * n;
m1 < p9 by A16,NAT_D:1;
then
A18: m1 < m by A15,XXREAL_0:2;
A19: p9 divides p9 * (m div p9) by NAT_D:def 3;
p9 divides p9 * ((m div p9) * n) by NAT_D:def 3;
then
A20: p9 divides m1 * n by A11,A17,NAT_D:10;
m = p9* (m div p9) + m1 by A16,NAT_D:2;
then not p9 divides m1 by A12,A19,NAT_D:8;
hence contradiction by A9,A13,A18,A20;
end;
A21: m < 2
proof
assume m >= 2;
then consider p1 being Element of NAT such that
A22: p1 is prime and
A23: p1 divides m by INT_2:31;
A24: p1 > 1 by A22,INT_2:def 4;
A25: not p1 divides p9
proof
assume p1 divides p9;
then p1 = 1 or p1 = p9 by A5,INT_2:def 4;
hence contradiction by A8,A22,A23,INT_2:def 4;
end;
p1 <= m by A10,A23,NAT_D:7;
then
A26: not p9 <= p1 by A14,XXREAL_0:2;
A27: p1 <> 0 by A22,INT_2:def 4;
consider k being Nat such that
A28: m * n = p9 * k by A11,NAT_D:def 3;
p1 divides p9 * k by A23,A28,NAT_D:9;
then p1 divides k by A6,A22,A26,A25;
then consider k1 being Nat such that
A29: k = p1 * k1 by NAT_D:def 3;
consider m1 being Nat such that
A30: m = p1 * m1 by A23,NAT_D:def 3;
A31: m1 > 0 by A8,A30;
A32: m1 <> m
proof
assume m1 = m;
then m = 1 * m1;
hence contradiction by A24,A30,A31,XREAL_1:68;
end;
m1 divides m by A30,NAT_D:def 3;
then m1 <= m by A10,NAT_D:7;
then
A33: m1 < m by A32,XXREAL_0:1;
(p9 * k1) * p1 = p1 *(m1 * n) by A28,A29,A30;
then m1 * n = p9 * k1 by A27,XCMPLX_1:5;
then
A34: p9 divides m1 * n by NAT_D:def 3;
not p9 divides m1 by A12,A30,NAT_D:9;
hence contradiction by A9,A13,A33,A34;
end;
m >= 2
proof
A35: m >= 0 + 1 by A10,NAT_1:13;
assume
A36: m < 2;
then m <= 1 + 1;
then m = 1 by A36,A35,NAT_1:9;
hence contradiction by A11,A13;
end;
hence thesis by A21;
end;
theorem
for x being Complex holds x |^ 2 = x * x & x^2 = x |^ 2
proof
let x be Complex;
thus x * x = (x |^ 1) * x
.= x |^ (1+1) by Th6
.= x |^ 2;
hence thesis;
end;
:: from SCMFSA9A, 2005.11.16, A.T
theorem
m qua Integer div n = m div n & m qua Integer mod n = m mod n;
:: from HEINE, 2006.01.07, A.T
reserve x for Real;
theorem
x > 0 implies x|^k > 0
proof
defpred P[Nat] means for x st x > 0 holds x|^$1 > 0;
A1: for k holds P[k] implies P[k+1]
proof
let k such that
A2: for x st x > 0 holds x|^k > 0;
let x;
A3: x|^(k+1) = x * x|^k by Th6;
assume
A4: x > 0;
then x|^k > 0 by A2;
hence thesis by A4,A3;
end;
A5: P[0] by RVSUM_1:94;
for k holds P[k] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
:: missing, 2006.07.17, A.T.
theorem
n > 0 implies 0 |^ n = 0
proof
assume n>0;
then n>=1+0 by NAT_1:13;
hence thesis by Th11;
end;
:: from CARD_4 and WSIERP_1, 2007.02.07, AK
definition
let m,n be Element of NAT;
redefine func m|^n -> Element of NAT; :: redefines |^ (NEWTON, definition)
coherence by ORDINAL1:def 12;
end;
:: from HEINE, 2007.07.27, A.T.
defpred P[Nat] means for i st 2 <= i holds i|^$1 >= $1 + 1;
Lm3: P[0] by RVSUM_1:94;
Lm4: for n st P[n] holds P[n+1]
proof
let n;
assume
A0: P[n];
let i such that
A4: 2 <= i;
i|^n >= n+1 by A0,A4;
then
A2: i*i|^n >= i*(n+1) by XREAL_1:64;
A1: i|^(n+1) = i*i|^n by Th6;
A3: 2+n <= i+n by A4,XREAL_1:6;
1 <= i by A4,XXREAL_0:2;
then i*n >= n by XREAL_1:151;
then i*n+i >= n+i by XREAL_1:6;
then i*i|^n >= n+i by A2,XXREAL_0:2;
hence thesis by A1,A3,XXREAL_0:2;
end;
theorem Th85:
2 <= i implies i|^n >= n + 1
proof
for n holds P[n] from NAT_1:sch 2(Lm3,Lm4);
hence thesis;
end;
theorem
2 <= i implies i|^n > n
proof
assume 2 <= i;
then i|^n >= n+1 by Th85;
hence thesis by NAT_1:13;
end;
:: from AMI_4, 2008.02.14, A.T.
reserve k for Nat;
scheme
Euklides9 { F(Nat) -> Element of NAT, G(Nat) -> Element of NAT,
a() -> Element of NAT, b() -> Element of NAT } :
ex k st F(k) = a() gcd b() & G(k) = 0
provided
A1: 0 < b() and
A2: b() < a() and
A3: F(0) = a() and
A4: G(0) = b() and
A5: for k st G(k) > 0 holds F(k+1) = G(k) & G(k+1) = F(k) mod G(k)
proof
deffunc F(Nat,set) = IFEQ($2,0,0,G($1));
consider q being sequence of NAT such that
A6: q.0 = a() and
A7: for i being Nat holds q.(i+1) = F(i,q.i) from NAT_1:sch 12;
deffunc Q(Nat) = q.$1;
q.(0+1) = IFEQ(q.0,0,0,G(0)) by A7
.= G(0) by A2,A6,FUNCOP_1:def 8;
then
A8: Q(0) = a() & Q(1 qua Element of NAT) = b() by A4,A6;
A9: for k st q.k qua Element of NAT > 0 holds q.k = F(k)
proof
let k such that
A10: q.k qua Element of NAT > 0;
now
per cases;
case
k = 0;
hence thesis by A3,A6;
end;
case
k <> 0;
then consider i being Nat such that
A11: k = i+1 by NAT_1:6;
reconsider i as Element of NAT by ORDINAL1:def 12;
A12: now
assume
A13: q.i qua Element of NAT = 0;
q.k = IFEQ(q.i,0,0,G(i)) by A7,A11
.= 0 by A13,FUNCOP_1:def 8;
hence contradiction by A10;
end;
q.k = IFEQ(q.i,0,0,G(i)) by A7,A11
.= G(i) by A12,FUNCOP_1:def 8;
hence thesis by A5,A10,A11;
end;
end;
hence thesis;
end;
A14: for k holds Q(k+2) = Q(k) mod Q(k+1)
proof
let k;
now
per cases;
case
A15: q.(k+1) <> 0;
A16: now
A17: q.k = 0 or q.k <> 0;
assume
A18: G(k) = 0;
q.(k+1) = IFEQ(q.k,0,0,G(k)) by A7
.= 0 by A18,A17,FUNCOP_1:def 8;
hence contradiction by A15;
end;
A19: q.(k+(1+1)) = q.((k+1)+1) .= IFEQ(q.(k+1),0,0,G(k+1)) by A7
.= G(k+1) by A15,FUNCOP_1:def 8
.= F(k) mod G(k) by A5,A16;
A20: now
assume
A21: q.k = 0;
q.(k+1) = IFEQ(q.k,0,0,G(k)) by A7
.= 0 by A21,FUNCOP_1:def 8;
hence contradiction by A15;
end;
q.(k+1) = IFEQ(q.k,0,0,G(k)) by A7
.= G(k) by A20,FUNCOP_1:def 8;
hence thesis by A9,A19,A20;
end;
case
A22: q.(k+1) = 0;
thus q.(k+2) = q.((k+1)+1) .= IFEQ(q.(k+1),0,0,G(k+1)) by A7
.= 0 by A22,FUNCOP_1:def 8
.= q.(k) mod q.(k+1) by A22;
end;
end;
hence thesis;
end;
A23: 0 < b() & b() < a() by A1,A2;
consider k such that
A24: Q(k) = a() gcd b() & Q(k + 1) = 0 from NAT_D:sch 1(A23,A8,A14);
take k;
thus F(k) = a() gcd b() by A1,A9,A24,Th58;
a() gcd b() > 0 by A1,Th58;
hence G(k) = IFEQ(q.k,0,0,G(k)) by A24,FUNCOP_1:def 8
.= 0 by A7,A24;
end;
:: from CARD_4, 2008.05.11, A.T.
reserve k,n,n1,n2,m1,m2 for Nat;
theorem Th87:
r <> 0 or n = 0 iff r|^n <> 0
proof
defpred P[Nat] means r <> 0 or $1 = 0 iff r|^$1 <> 0;
A1: P[k] implies P[k+1]
proof
assume
A2: P[k];
r|^(k+1) = r|^k*r by Th6;
hence thesis by A2;
end;
A3: P[0] by RVSUM_1:94;
P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm5: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 <= n2
proof
assume
A1: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
assume
A2: n1 > n2;
then consider n being Nat such that
A3: n1 = n2+n by NAT_1:10;
n <> 0 by A2,A3;
then consider k being Nat such that
A4: n = k+1 by NAT_1:6;
A5: 2|^n2 <> 0 by Th87;
reconsider k as Element of NAT by ORDINAL1:def 12;
2|^n1 = (2|^n2)*(2|^(k+1)) by A3,A4,Th8;
then (2|^n1)*(2*m1+1) = 2|^n2*(2|^(k+1)*(2*m1+1));
then 2|^(k+1)*(2*m1+1) = 2*m2+1 by A1,A5,XCMPLX_1:5;
then 2*m2+1 = 2|^k*(2|^1)*(2*m1+1) by Th8
.= 2*((2|^k)*(2*m1+1));
then
A6: 2 divides 2*m2+1 by NAT_D:def 3;
2 divides 2*m2 by NAT_D:def 3;
hence contradiction by A6,NAT_D:7,10;
end;
theorem
(2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 = n2 & m1 = m2
proof
A1: 2|^n1 <> 0 by Th87;
assume
A2: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
then
A3: n2 <= n1 by Lm5;
n1 <= n2 by A2,Lm5;
hence n1 = n2 by A3,XXREAL_0:1;
then 2*m1+1 = 2*m2+1 by A2,A1,XCMPLX_1:5;
hence thesis;
end;
theorem
k <= n implies m |^ k divides m |^ n
proof
assume k <= n;
then consider t being Nat such that
A1: n = k + t by NAT_1:10;
reconsider t as Element of NAT by ORDINAL1:def 12;
m |^ n = (m |^ k)*(m |^ t) by A1,Th8;
hence thesis by NAT_D:def 3;
end;