:: Factorial and Newton coefficients :: by Rafa{\l} Kwiatek :: :: Received July 27, 1990 :: Copyright (c) 1990-2017 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; 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,G,H for FinSequence of REAL; theorem Th1: n>=1 implies Seg n = {1} \/ {k where k is Element of NAT: 1=1; A2: {1} \/ {k where k is Element of NAT: 11; 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 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 by RVSUM_1:95; 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,RVSUM_1:95; 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: st; 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; 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; 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; 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).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 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; 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; 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,RVSUM_1:95; 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 by INT_1:57; 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 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; cluster prime for Nat; existence by INT_2:28; end; definition mode Prime is prime Nat; 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: ex p st p>l proof 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=m implies not k in SetPrimenumber m by Def7; Lm2: SetPrimenumber n = {k where k is Element of NAT:k 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; sg; f non empty 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; 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,NAT_D:def 2; 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;