Copyright (c) 1990 Association of Mizar Users
environ vocabulary ARYTM_3, INT_1, ARYTM_1, ABSVALUE, FILTER_0, INT_2; notation SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1, GROUP_1; constructors REAL_1, NAT_1, GROUP_1, XBOOLE_0; clusters INT_1, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, ARITHM; theorems AXIOMS, INT_1, REAL_1, ABSVALUE, NAT_1, XCMPLX_0, XCMPLX_1; schemes REAL_1; begin :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: SOME PROPERTIES ON FUNCTIONS: HCF & LCM FOR NATURAL NUMBERS :: :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: reserve a,b,c,d,e,f,g,h,z for Nat; canceled 2; theorem Th3: 0 divides a iff a = 0 proof 0 divides a implies a = 0 proof assume 0 divides a; then ex b st a = 0*b by NAT_1:def 3; hence thesis; end; hence thesis; end; theorem Th4: a = 0 or b = 0 iff a lcm b = 0 proof A1: a = 0 implies a lcm b = 0 proof assume a = 0; then 0 divides (a lcm b) by NAT_1:def 4; hence thesis by Th3; end; A2: b = 0 implies (a lcm b) = 0 proof assume b = 0; then 0 divides (a lcm b) by NAT_1:def 4; hence thesis by Th3; end; (a lcm b) = 0 implies a = 0 or b = 0 proof assume A3: (a lcm b) = 0; A4: a divides a implies a divides a*b by NAT_1:56; b divides b implies b divides b*a by NAT_1:56; then 0 divides a*b by A3,A4,NAT_1:def 4; then a*b = 0 by Th3; hence thesis by XCMPLX_1:6; end; hence thesis by A1,A2; end; theorem a = 0 & b = 0 iff a hcf b = 0 proof (a hcf b) = 0 implies a = 0 & b = 0 proof assume (a hcf b) = 0; then 0 divides a & 0 divides b by NAT_1:def 5; hence thesis by Th3; end; hence thesis; end; theorem a*b = (a lcm b)*(a hcf b) proof A1: a<>0 & b<>0 implies a*b = (a lcm b)*(a hcf b) proof assume A2: a<>0 & b<>0; A3: a divides a implies a divides a*b by NAT_1:56; b divides b implies b divides b*a by NAT_1:56; then (a lcm b) divides a*b by A3,NAT_1:def 4; then consider c such that A4: a*b = (a lcm b)*c by NAT_1:def 3; A5: a divides (a lcm b) & b divides (a lcm b) by NAT_1:def 4; then consider d such that A6: (a lcm b) = a*d by NAT_1:def 3; consider e such that A7: (a lcm b) = b*e by A5,NAT_1:def 3; a*b = a*(c*d) by A4,A6,XCMPLX_1:4; then A8: b = c*d by A2,XCMPLX_1:5; a*b = b*(c*e) by A4,A7,XCMPLX_1:4; then a = c*e by A2,XCMPLX_1:5; then A9:c divides a & c divides b by A8,NAT_1:def 3; f divides a & f divides b implies f divides c proof assume A10: f divides a & f divides b; then consider g such that A11: a = f*g by NAT_1:def 3; consider h such that A12: b = f*h by A10,NAT_1:def 3; A13: b*g = g*h*f by A12,XCMPLX_1:4; a*h = g*h*f by A11,XCMPLX_1:4; then a divides g*h*f & b divides g*h*f by A13,NAT_1:def 3; then (a lcm b) divides g*h*f by NAT_1:def 4; then consider z such that A14: g*h*f = (a lcm b)*z by NAT_1:def 3; A15: c*(a lcm b) = (g*(h*f))*f by A4,A11,A12,XCMPLX_1:4 .= (a lcm b)*z*f by A14,XCMPLX_1:4 .= (z*f)*(a lcm b) by XCMPLX_1:4; (a lcm b) <> 0 by A2,Th4; then c = f*z by A15,XCMPLX_1:5; hence thesis by NAT_1:def 3; end; hence thesis by A4,A9,NAT_1:def 5; end; a = 0 or b = 0 implies a*b = (a lcm b)*(a hcf b) proof assume A16: a = 0 or b = 0; then a*b = 0*(a hcf b) .= (a lcm b)*(a hcf b) by A16,Th4; hence thesis; end; hence thesis by A1; end; :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: SOME PROPERTIES OF INTEGER NUMBERS :: :: LCM,HCF :: :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: reserve m,n for Nat; reserve a,b,c,d,a1,b1,a2,b2,k,l for Integer; canceled; theorem Th8: -n is Nat iff n = 0 proof thus -n is Nat implies n = 0 proof assume -n is Nat; then A1: -n>=0 & n>=0 by NAT_1:18; then n+(-n)>=0+n by AXIOMS:24; then n-n>=0+n by XCMPLX_0:def 8; then 0>=n by XCMPLX_1:14; hence thesis by A1,AXIOMS:21; end; thus n = 0 implies -n is Nat; thus thesis; end; theorem Th9: not -1 is Nat by Th8; theorem Th10: 0 divides a iff a = 0 proof 0 divides a implies a = 0 proof assume 0 divides a; then consider a1 such that A1: a = 0*a1 by INT_1:def 9; thus thesis by A1; end; hence thesis; end; theorem Th11: a divides -a & -a divides a proof thus a divides -a proof -a = -(a*1) .= a*(-1) by XCMPLX_1:175; hence thesis by INT_1:def 9; end; thus thesis proof a = -(-(a*1)).= (-a)*(-1) by XCMPLX_1:176; hence thesis by INT_1:def 9; end; end; theorem Th12: a divides b implies a divides b*c proof assume a divides b; then consider d such that A1: b = a*d by INT_1:def 9; b*c = a*(d*c) by A1,XCMPLX_1:4; hence thesis by INT_1:def 9; end; theorem Th13: a divides b & b divides c implies a divides c proof assume that A1: a divides b and A2: b divides c; consider k such that A3: b = a*k by A1,INT_1:def 9; consider l such that A4: c = b*l by A2,INT_1:def 9; c = a*(k*l) by A3,A4,XCMPLX_1:4; hence thesis by INT_1:def 9; end; theorem Th14: (a divides b iff a divides -b) & (a divides b iff -a divides b) & (a divides b iff -a divides -b) & (a divides -b iff -a divides b) proof thus A1: a divides b iff a divides -b proof A2: a divides b implies a divides -b proof assume A3: a divides b; b divides -b by Th11; hence thesis by A3,Th13; end; a divides -b implies a divides b proof assume A4: a divides -b; -b divides b by Th11; hence thesis by A4,Th13; end; hence thesis by A2; end; thus A5: a divides b iff -a divides b proof A6: a divides b implies -a divides b proof assume A7: a divides b; -a divides a by Th11; hence thesis by A7,Th13; end; -a divides b implies a divides b proof assume A8: -a divides b; a divides -a by Th11; hence thesis by A8,Th13; end; hence thesis by A6; end; thus a divides b iff -a divides -b proof A9: a divides b implies -a divides -b proof assume A10: a divides b; -a divides a by Th11; hence thesis by A1,A10,Th13; end; -a divides -b implies a divides b proof assume A11: -a divides -b; -b divides b by Th11; hence thesis by A5,A11,Th13; end; hence thesis by A9; end; thus thesis by A1,A5; end; theorem a divides b & b divides a implies a = b or a = -b proof assume A1: a divides b & b divides a; then consider a1 such that A2: b = a*a1 by INT_1:def 9; consider b1 such that A3: a = b*b1 by A1,INT_1:def 9; a<>0 implies a = b or a = -b proof assume A4: a<>0; 1*a = a*(a1*b1) by A2,A3,XCMPLX_1:4; then a1*b1 = 1 by A4,XCMPLX_1:5; then a = b*1 or a = b*(-1) by A3,INT_1:22; then a = b*1 or a = (-b)*1 by XCMPLX_1:175; hence thesis; end; hence thesis by A1,Th10; end; theorem Th16: a divides 0 & 1 divides a & -1 divides a proof thus a divides 0 proof 0 = a*0; hence thesis by INT_1:def 9; end; thus 1 divides a proof a = 1*a; hence thesis by INT_1:def 9; end; thus thesis proof a = -(1*(-a)) .= (-1)*(-a) by XCMPLX_1:175; hence thesis by INT_1:def 9; end; end; theorem Th17: a divides 1 or a divides -1 implies a = 1 or a = -1 proof assume A1: a divides 1 or a divides -1; A2: a divides 1 implies a = 1 or a = -1 proof assume a divides 1; then consider b such that A3: 1 = a*b by INT_1:def 9; thus thesis by A3,INT_1:22; end; a divides -1 implies a = 1 or a = -1 proof assume a divides -1; then ex b st -1 = a*b by INT_1:def 9; hence thesis by INT_1:23; end; hence thesis by A1,A2; end; theorem a = 1 or a = -1 implies a divides 1 & a divides -1 by Th16; theorem a,b are_congruent_mod c iff c divides (a-b) proof A1: a,b are_congruent_mod c implies c divides (a-b) proof assume a,b are_congruent_mod c; then ex d st (a-b) = c*d by INT_1:def 3; hence thesis by INT_1:def 9; end; c divides (a-b) implies a,b are_congruent_mod c proof assume c divides (a-b); then ex d st (a-b) = c*d by INT_1:def 9; hence thesis by INT_1:def 3; end; hence thesis by A1; end; theorem abs(a) is Nat; theorem Th21: a divides b iff (abs(a)) divides (abs(b)) proof A1: a divides b implies (abs(a)) divides (abs(b)) proof assume a divides b; then consider c such that A2: b = a*c by INT_1:def 9; abs(b) = abs(a)*abs(c) by A2,ABSVALUE:10; hence thesis by NAT_1:def 3; end; (abs(a)) divides (abs(b)) implies a divides b proof assume (abs(a)) divides (abs(b)); then consider m such that A3: abs(b) = abs(a)*m by NAT_1:def 3; A4: a>=0 implies a divides b proof assume a>=0; then A5: abs(b) = a*m by A3,ABSVALUE:def 1; A6: b>=0 implies a divides b proof assume b>=0; then b = a*m by A5,ABSVALUE:def 1; hence thesis by INT_1:def 9; end; b<0 implies a divides b proof assume b<0; then -b = a*m by A5,ABSVALUE:def 1; then b = -(a*m) .= a*(-m) by XCMPLX_1:175; hence thesis by INT_1:def 9; end; hence thesis by A6; end; a<0 implies a divides b proof assume a<0; then A7: abs(b) = (-a)*m by A3,ABSVALUE:def 1; A8: b>=0 implies a divides b proof assume b>=0; then b = (-a)*m by A7,ABSVALUE:def 1 .= a*(-m) by XCMPLX_1:176; hence thesis by INT_1:def 9; end; b<0 implies a divides b proof assume b<0; then -b = (-a)*m by A7,ABSVALUE:def 1 .= -(a*m) by XCMPLX_1:175; then -(-b) = a*m; hence thesis by INT_1:def 9; end; hence thesis by A8; end; hence thesis by A4; end; hence thesis by A1; end; :::::::::::::::::: :: LCM :: :::::::::::::::::: definition let a,b; canceled; func a lcm' b -> Integer equals :Def2: abs(a) lcm abs(b); coherence; commutativity; end; canceled; theorem a lcm' b is Nat proof a lcm' b = abs(a) lcm abs(b) by Def2; hence thesis; end; canceled; theorem Th25: a divides (a lcm' b) proof abs(a) divides (abs(a) lcm abs(b)) by NAT_1:def 4; then consider m such that A1: (abs(a) lcm abs(b)) = abs(a)*m by NAT_1:def 3 ; A2: a>=0 implies a divides (a lcm' b) proof assume A3: a>=0; reconsider c = (abs(a) lcm abs(b)) as Integer; reconsider a1 = m as Integer; c = a*a1 by A1,A3,ABSVALUE:def 1; then a divides c by INT_1:def 9; hence thesis by Def2; end; a<0 implies a divides (a lcm' b) proof assume A4: a<0; reconsider c = abs(a) lcm abs(b) as Integer; reconsider b1 = m as Integer; c = (-a)*b1 by A1,A4,ABSVALUE:def 1 .= a*(-b1) by XCMPLX_1:176; then a divides c by INT_1:def 9; hence thesis by Def2; end; hence thesis by A2; end; theorem b divides (a lcm' b) by Th25; theorem Th27: for c st a divides c & b divides c holds (a lcm' b) divides c proof let c; assume A1: a divides c & b divides c; then A2: (abs(a)) divides (abs(c)) by Th21; (abs(b)) divides (abs(c)) by A1,Th21; then (abs(a) lcm abs(b)) divides (abs(c)) by A2,NAT_1:def 4; then consider m such that A3: abs(c) = (abs(a) lcm abs(b))*m by NAT_1:def 3; A4: c>=0 implies (a lcm' b) divides c proof assume c>=0; then abs(c) = c by ABSVALUE:def 1; then c = (a lcm' b)*m by A3,Def2; hence thesis by INT_1:def 9; end; c <0 implies (a lcm' b) divides c proof assume c <0; then abs(c) = -c by ABSVALUE:def 1; then -c = (a lcm' b)*m by A3,Def2; then c = -((a lcm' b)*m) .= (a lcm' b)*(-m) by XCMPLX_1:175; hence thesis by INT_1:def 9; end; hence thesis by A4; end; :::::::::::::::::: :: GCD :: :::::::::::::::::: definition let a,b; func a gcd b -> Integer equals :Def3: abs(a) hcf abs(b); coherence; commutativity; end; canceled; theorem Th29: a gcd b is Nat proof a gcd b = abs(a) hcf abs(b) by Def3; hence thesis; end; canceled; theorem Th31: (a gcd b) divides a proof (abs(a) hcf abs(b)) divides (abs(a)) by NAT_1:def 5; then consider m such that A1: abs(a) = (abs(a) hcf abs(b))*m by NAT_1:def 3; A2: a>=0 implies (a gcd b) divides a proof assume A3: a>=0; reconsider c = abs(a) hcf abs(b) as Integer; reconsider a1 = m as Integer; a = c*a1 by A1,A3,ABSVALUE:def 1; then c divides a by INT_1:def 9; hence thesis by Def3; end; a<0 implies (a gcd b) divides a proof assume A4: a<0; reconsider c = abs(a) hcf abs(b) as Integer; reconsider b1 = m as Integer; -(-a) = -(c*b1) by A1,A4,ABSVALUE:def 1 .= c*(-b1) by XCMPLX_1:175; then c divides a by INT_1:def 9; hence thesis by Def3; end; hence thesis by A2; end; theorem (a gcd b) divides b by Th31; theorem Th33: for c st c divides a & c divides b holds c divides (a gcd b) proof let c; assume A1: c divides a & c divides b; then A2: (abs(c)) divides (abs(a)) by Th21; (abs(c)) divides (abs(b)) by A1,Th21; then (abs(c)) divides (abs(a) hcf abs(b)) by A2,NAT_1:def 5; then consider m such that A3: abs(a) hcf abs(b) = (abs(c))*m by NAT_1:def 3; A4: c>=0 implies c divides (a gcd b) proof assume c>=0; then abs(c) = c by ABSVALUE:def 1; then a gcd b = c*m by A3,Def3; hence thesis by INT_1:def 9; end; c <0 implies c divides (a gcd b) proof assume c <0; then abs(c) = -c by ABSVALUE:def 1; then a gcd b = (-c)*m by A3,Def3; then a gcd b = c*(-m) by XCMPLX_1:176; hence thesis by INT_1:def 9; end; hence thesis by A4; end; theorem a = 0 or b = 0 iff a lcm' b = 0 proof A1: a = 0 implies a lcm' b = 0 proof assume a = 0; then 0 divides (a lcm' b) by Th25; hence thesis by Th10; end; A2: b = 0 implies a lcm' b = 0 proof assume b = 0; then 0 divides (a lcm' b) by Th25; hence thesis by Th10; end; a lcm' b = 0 implies a = 0 or b = 0 proof assume A3: a lcm' b = 0; A4: a divides a implies a divides a*b by Th12; b divides b implies b divides b*a by Th12; then 0 divides a*b by A3,A4,Th27; then a*b = 0 by Th10; hence thesis by XCMPLX_1:6; end; hence thesis by A1,A2; end; theorem Th35: a = 0 & b = 0 iff a gcd b = 0 proof A1: a = 0 & b = 0 implies a gcd b = 0 proof assume a = 0 & b = 0; then 0 divides (a gcd b) by Th33; hence thesis by Th10; end; a gcd b = 0 implies a = 0 & b = 0 proof assume a gcd b = 0; then 0 divides a & 0 divides b by Th31; hence thesis by Th10; end; hence thesis by A1; end; :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: RELATIVE PRIME NUMBERS :: :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let a,b; pred a,b are_relative_prime means :Def4: a gcd b = 1; symmetry; end; canceled 2; theorem a<>0 or b<>0 implies ex a1,b1 st a = (a gcd b)*a1 & b = (a gcd b)*b1 & a1,b1 are_relative_prime proof assume A1: a<>0 or b<>0; (a gcd b) divides a by Th31; then consider a1 such that A2: a = (a gcd b)*a1 by INT_1:def 9; (a gcd b) divides b by Th31; then consider b1 such that A3: b = (a gcd b)*b1 by INT_1:def 9; (a1 gcd b1) divides a1 by Th31; then consider a2 such that A4: a1 = (a1 gcd b1)*a2 by INT_1:def 9; (a1 gcd b1) divides b1 by Th31; then consider b2 such that A5: b1 = (a1 gcd b1)*b2 by INT_1:def 9; A6: a = ((a gcd b)*(a1 gcd b1))*a2 by A2,A4,XCMPLX_1:4; b = ((a gcd b)*(a1 gcd b1))*b2 by A3,A5,XCMPLX_1:4; then (a gcd b)*(a1 gcd b1) divides a & (a gcd b)*(a1 gcd b1) divides b by A6,INT_1:def 9; then (a gcd b)*(a1 gcd b1) divides (a gcd b) by Th33; then consider c such that A7: a gcd b = ((a gcd b)*(a1 gcd b1))*c by INT_1:def 9; A8: (a gcd b)*1 = (a gcd b)*((a1 gcd b1)*c) by A7,XCMPLX_1:4; a gcd b <>0 by A1,Th35; then 1 = (a1 gcd b1)*c by A8,XCMPLX_1:5; then a1 gcd b1 = 1 or a1 gcd b1 = -1 by INT_1:22; then a1,b1 are_relative_prime by Def4,Th9,Th29; hence thesis by A2,A3; end; theorem Th39: a,b are_relative_prime implies (c*a gcd c*b) = abs(c) & c*a gcd b*c = abs(c) & a*c gcd c*b = abs(c) & a*c gcd b*c = abs(c) proof assume a,b are_relative_prime; then A1: a gcd b = 1 by Def4; thus A2: c*a gcd c*b = abs(c) proof c divides c*a & c divides c*b by Th12; then c divides (c*a gcd c*b) by Th33; then consider d such that A3: c*a gcd c*b = c*d by INT_1:def 9; (c*a gcd c*b) divides c*a by Th31; then consider k such that A4: c*a = (c*a gcd c*b)*k by INT_1:def 9; (c*a gcd c*b) divides c*b by Th31; then consider l such that A5: c*b = (c*a gcd c*b)*l by INT_1:def 9; A6: c*a = c*(d*k) by A3,A4,XCMPLX_1:4; A7: c*b = c*(d*l) by A3,A5,XCMPLX_1:4; A8: c <>0 implies c*a gcd c*b = abs(c) proof assume A9: c <>0; then a = d*k by A6,XCMPLX_1:5; then A10: d divides a by INT_1:def 9; b = d*l by A7,A9,XCMPLX_1:5; then d divides b by INT_1:def 9; then d divides 1 by A1,A10,Th33; then c*a gcd c*b = c*1 or c*a gcd c*b = c*(-1) by A3,Th17; then c*a gcd c*b = c*1 or c*a gcd c*b = (-c)*1 by XCMPLX_1:175; then A11: abs((c*a gcd c*b)) = abs(c) by ABSVALUE:17; c*a gcd c*b is Nat by Th29; then c*a gcd c*b >=0 by NAT_1:18; hence thesis by A11,ABSVALUE:def 1; end; c = 0 implies c*a gcd c*b = abs(c) proof assume A12: c = 0; then c*a gcd c*b = 0 by Th35 .= abs(0) by ABSVALUE:def 1; hence thesis by A12; end; hence thesis by A8; end; hence c*a gcd b*c = abs(c); thus thesis by A2; end; theorem Th40: c divides a*b & a,c are_relative_prime implies c divides b proof assume A1: c divides a*b & a,c are_relative_prime; then A2: a*b gcd c*b = abs(b) by Th39; c divides c*b by Th12; then A3: c divides (a*b gcd c*b) by A1,Th33; b<0 implies c divides b proof assume b<0; then c divides (-b) by A2,A3,ABSVALUE:def 1; hence thesis by Th14; end; hence thesis by A2,A3,ABSVALUE:def 1; end; theorem a,c are_relative_prime & b,c are_relative_prime implies a*b,c are_relative_prime proof assume a,c are_relative_prime & b,c are_relative_prime; then A1: (a gcd c) = 1 & (b gcd c) = 1 by Def4; A2: (a*b gcd c) divides a*b & (a*b gcd c) divides c by Th31; A3: ((a*b gcd c) gcd a) divides (a*b gcd c) & ((a*b gcd c) gcd a) divides a by Th31; then ((a*b gcd c) gcd a) divides c by A2,Th13; then ((a*b gcd c) gcd a) divides 1 by A1,A3,Th33; then (a*b gcd c) gcd a = 1 or (a*b gcd c) gcd a = -1 by Th17; then a,(a*b gcd c) are_relative_prime by Def4,Th9,Th29; then (a*b gcd c) divides b by A2,Th40; then (a*b gcd c) divides 1 by A1,A2,Th33; then a*b gcd c = 1 or a*b gcd c = -1 by Th17; hence thesis by Def4,Th9,Th29; end; ::***************************************************************************:: :: PRIME NUMBERS :: ::***************************************************************************:: reserve p,p1,q,k,l for Nat; reserve x for Real; reserve X for Subset of REAL; definition let p; attr p is prime means :Def5: p>1 & for n holds n divides p implies n = 1 or n = p; end; definition let m,n; pred m,n are_relative_prime means :Def6: m hcf n = 1; end; canceled 2; theorem 2 is prime proof thus 2>1 & for n holds n divides 2 implies n = 1 or n = 2 proof thus 2>1; let n; assume A1: n divides 2; then n<>0 by Th3; then n>0 by NAT_1:19; then A2: n>=0+1 by NAT_1:38; then n+(-1+1)>=1; then (n+-1)+1>=1 by XCMPLX_1:1; then A3: (n-1)+1>=1 by XCMPLX_0:def 8; n-1>=1-1 by A2,REAL_1:49; then reconsider m = n-1 as Nat by INT_1:16; m+1 = 1 or m>=1 by A3,NAT_1:26; then (n-1)+1 = 1 or (n-1)+1>=1+1 by AXIOMS:24; then n+-1+1 = 1 or (n+-1)+1>=1+1 by XCMPLX_0:def 8; then A4: n+(-1+1) = 1 or n+(-1+1)>=2 by XCMPLX_1:1; n<=2 by A1,NAT_1:54; hence thesis by A4,AXIOMS:21; end; end; canceled; theorem ex p st not p is prime proof take 4; ex n st n divides 4 & n<>1 & n<>4 proof take 2; 4 = 2*2; hence thesis by NAT_1:def 3; end; hence thesis by Def5; end; theorem p is prime & q is prime implies p,q are_relative_prime or p = q proof assume A1: p is prime & q is prime; assume not p,q are_relative_prime; then A2: (p hcf q)<>1 by Def6; (p hcf q) divides p & (p hcf q) divides q by NAT_1:def 5; then (p hcf q) = p & (p hcf q) = q by A1,A2,Def5; hence thesis; end; scheme Ind1 { a() -> Nat,P[Nat] } : for k st k>=a() holds P[k] provided A1: P[a()] and A2: for k st k>=a() & P[k] holds P[k+1] proof let k; assume k>=a(); then k-a()>=a()-a() by REAL_1:49; then k-a()>=0 by XCMPLX_1:14; then reconsider m = k-a() as Nat by INT_1:16; k-(a()-a()) = m+a() by XCMPLX_1:37; then A3: k-0 = m+a() by XCMPLX_1:14; defpred P1[Real] means ex m st P[m+a()] & m = $1; consider X such that A4: x in X iff P1[x] from SepReal; P[0+a()] by A1; then A5: 0 in X by A4; for x st x in X holds x+1 in X proof let x; assume x in X; then consider m such that A6: P[m+a()] & m = x by A4; m+a()>=a() & P[m+a()] implies P[m+a()+1] by A2; then A7: m+a()>=a() & P[m+a()] implies P[m+1+a()] by XCMPLX_1:1; m>=0 by NAT_1:18; then m+a()>=0+a() by AXIOMS:24; hence thesis by A4,A6,A7; end; then m in X by A5,NAT_1:2; then ex n st P[n+a()] & n = m by A4; hence P[k] by A3; end; scheme Comp_Ind1 { a() -> Nat,P[Nat] } : for k st k>=a() holds P[k] provided A1: for k st k>=a() & (for n st n>=a() & n<k holds P[n]) holds P[k] proof defpred P1[Nat] means for n st (n>=a() & n<$1) holds P[n]; A2: P1[a()]; A3: for k st k>=a() holds P1[k] implies P1[k+1] proof let k; assume k>=a(); assume A4: for n st n>=a() & n<k holds P[n]; let n; assume A5: n>=a() & n<k+1; then n<=k by NAT_1:38; then n<k or n = k by REAL_1:def 5; hence thesis by A1,A4,A5; end; let k; A6: for k st k>=a() holds P1[k] from Ind1(A2,A3); assume A7: k>=a(); then for n st (n>=a() & n<k) holds P[n] by A6; hence P[k] by A1,A7; end; theorem l>=2 implies ex p st p is prime & p divides l proof assume A1: l>=2; defpred P[Nat] means (ex p st p is prime & p divides $1); A2: for k st k>=2 holds (for n st n>=2 holds n<k implies P[n]) implies P[k] proof let k; assume k>=2; then k+1>1+1 by NAT_1:38; then k+1-1>1+1-1 by REAL_1:54; then A3: k+(1-1)>1+1-1 by XCMPLX_1:29; assume A4: for n st n>=2 holds n<k implies (ex p st p is prime & p divides n); not k is prime implies ex p st p is prime & p divides k proof assume not k is prime; then consider m such that A5: m divides k & m<>1 & m<>k by A3,Def5; m>=2 & m<k proof thus m>=2 proof m<>0 by A5,Th3; then m>0 by NAT_1:19; then m>=0+1 by NAT_1:38; then m>1 by A5,REAL_1:def 5; then m>=1+1 by NAT_1:38; hence thesis; end; k>0 by A3,AXIOMS:22; then m<=k by A5,NAT_1:54; hence thesis by A5,REAL_1:def 5; end; then consider p1 such that A6: p1 is prime & p1 divides m by A4; take p1; thus thesis by A5,A6,NAT_1:51; end; hence thesis; end; for k st k>=2 holds P[k] from Comp_Ind1 (A2); hence thesis by A1; end;