:: Prime Factorization of Sums and Differences of Two Like Powers
:: by Rafa{\l} Ziobro
::
:: Received June 30, 2016
:: Copyright (c) 2016-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 ABIAN, NUMBERS, NAT_1, INT_1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1,
INT_2, COMPLEX1, RELAT_1, NEWTON, SQUARE_1, XCMPLX_0, POWER, PYTHTRIP,
NAT_3, REAL_1, SUBSET_1, ORDINAL1, ZFMISC_1, ABSVALUE;
notations ABIAN, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, INT_2, ORDINAL1,
SQUARE_1, NEWTON, POWER, XREAL_0, PYTHTRIP, IRRAT_1, NAT_3,
TARSKI,
XBOOLE_0, SUBSET_1, CARD_1, ZFMISC_1, NAT_1, NAT_D, RELAT_1, FUNCT_1;
constructors ABIAN, SQUARE_1, NAT_1, NAT_D, NEWTON, POWER, PREPOWER, ORDINAL1,
PEPIN, PYTHTRIP, RAT_1, NAT_3, NUMBERS, XXREAL_0, XREAL_0, WSIERP_1,
MOEBIUS1, EULER_1, ABSVALUE;
registrations ABIAN, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON,
WSIERP_1, XCMPLX_0, PYTHTRIP, NEWTON01, NEWTON02, ABSVALUE, NAT_6, INT_2,
MOEBIUS1, NAT_5;
requirements REAL, NUMERALS, SUBSET, ARITHM;
expansions ABIAN, INT_1, INT_2;
theorems INT_2, NAT_1, ABSVALUE, INT_1, PREPOWER, NEWTON, XCMPLX_1, XREAL_1,
XXREAL_0, NAT_D, SQUARE_1, PEPIN, ABIAN, NAT_3, WSIERP_1, TAYLOR_2,
POWER, NEWTON01, NEWTON02, ORDINAL1, PYTHTRIP, COMPLEX1, NAT_2, NAT_6,
INT_6, NAT_4, NAT_5, INT_4, GROUPP_1, INT_5;
schemes NAT_1;
begin
reserve a,b,c,d,x,j,k,l,m,n,o,xi,xj for Nat,
p,q,t,z,u,v for Integer,
a1,b1,c1,d1 for Complex;
theorem
a1|^(n+k) + b1|^(n+k) = a1|^n*(a1|^k + b1|^k) + b1|^k*(b1|^n-a1|^n)
proof
a1|^(n+k) = a1|^n * a1|^k & b1|^(n+k) = b1|^n*b1|^k by NEWTON:8;
hence thesis;
end;
theorem RI2:
a1|^(n+k) - b1|^(n+k) = a1|^n*(a1|^k - b1|^k) +
b1|^k*(a1|^n - b1|^n)
proof
a1|^(n+k) = a1|^n * a1|^k & b1|^(n+k) = b1|^n*b1|^k by NEWTON:8;
hence thesis;
end;
theorem RI3:
a1|^(m+2) + b1|^(m+2) =
(a1+b1)*(a1|^(m+1) + b1|^(m+1)) - a1*b1*(a1|^(m)+ b1|^(m))
proof
a1|^((m+1)+1) = a1*a1|^(m+1) & b1|^((m+1)+1) = b1*b1|^(m+1) &
a1|^((m)+1) = a1*a1|^(m) & b1|^((m)+1) = b1*b1|^(m) by NEWTON:6;
hence thesis;
end;
definition
let a be Nat;
redefine attr a is trivial means :Def0: :: redefines trivial (ZFMISC_1, definition)
a <= 1;
compatibility
proof
a <= 1 implies a = 1 or a < 1 by XXREAL_0:1;
hence thesis by NAT_2:def 1,NAT_1:14;
end;
end;
definition
let a be Complex;
redefine func a^2 -> set equals :: redefines ^2 (SQUARE_1, definition)
a|^2;
correctness by NEWTON:81;
end;
definition
let a,b be Integer;
redefine func a gcd b -> Nat equals :: redefines gcd (INT_2, definition)
|.a.| gcd |.b.|;
correctness by INT_2:34;
redefine func a lcm b -> Nat equals :Def2: :: redefines lcm (INT_2, definition)
|.a.| lcm |.b.|;
correctness by INT_2:33;
end;
registration
let a,b be positive Real;
cluster max(a,b) -> positive;
coherence by XXREAL_0:def 10;
cluster min(a,b) -> positive;
coherence by XXREAL_0:def 9;
end;
registration
let a be non zero Integer, b be Integer;
cluster a gcd b -> non zero;
coherence by INT_2:5;
end;
registration
let a be non zero Complex, n be Nat;
cluster a|^n -> non zero;
coherence by PREPOWER:5;
end;
registration
let a be non trivial Nat, n be non zero Nat;
cluster a|^n -> non trivial;
coherence
proof
reconsider m = n-1 as Nat;
a|^(m+1) = a*a|^m & a > 1 by NEWTON:6,Def0;
then a|^(m+1) > 1*a|^m & a|^m >= 1 by XREAL_1:68,NAT_1:14;
hence thesis by XXREAL_0:2;
end;
end;
registration
let a be Integer;
cluster |.a.| -> natural;
coherence;
end;
registration
let a be even Integer;
cluster |.a.| -> even;
coherence
proof
2 divides a iff |.2.| divides |.a.| by INT_2:16;
hence thesis by ABIAN:def 1;
end;
end;
registration
let a be Nat;
reduce a lcm a to a;
reducibility by NAT_D:31;
reduce a gcd a to a;
reducibility by NAT_D:32;
end;
registration
let a be non zero Integer, b be Integer;
cluster a gcd b -> positive;
coherence;
end;
registration
let a,b be Integer;
reduce a gcd (a gcd b) to a gcd b;
correctness
proof
a gcd (a gcd b) = (a gcd a) gcd b by INT_6:18
.= |.a.| gcd |.a.| gcd b by INT_2:34;
hence thesis by INT_6:14;
end;
reduce a lcm (a lcm b) to a lcm b;
correctness
proof
a lcm (a lcm b) = |.a.| lcm |.(a lcm b).| by INT_2:33
.= |.a.| lcm (|.a.| lcm |.b.|) by INT_2:33
.= (|.a.| lcm |.a.|) lcm |.b.| by NEWTON:43
.= a lcm b by INT_2:33;
hence thesis;
end;
end;
registration
let a be Integer;
reduce (a+1) gcd a to 1;
reducibility
proof
1*a+1 gcd a = 1 gcd a by NEWTON02:5;
hence thesis;
end;
end;
theorem NEWTON027:
for t,z be Integer holds
t|^n gcd z|^n = (t gcd z)|^n
proof
let t,z be Integer;
A1: t|^n gcd z|^n = |.t|^n.| gcd |.z|^n.|
& t gcd z = |.t.| gcd |.z.| by INT_2:34;
|.t|^n.| = |.t.||^n & |.z|^n.| = |.z.||^n by TAYLOR_2:1;
hence thesis by A1, NEWTON02:7;
end;
registration
let a be Integer, n be Nat;
reduce (a+1)|^n gcd a|^n to 1;
reducibility
proof
1|^n = (a gcd (a+1))|^n;
hence thesis by NEWTON027;
end;
end;
registration
let a1,b1;
reduce a1|^0 - b1|^0 to 0;
reducibility
proof
1*a1|^0 - 1*b1|^0 = 0;
hence thesis;
end;
end;
registration
let a be non negative Real, n be Nat;
cluster a|^n -> non negative;
coherence
proof
a|^n >= 0|^n by NEWTON02:41;
hence thesis;
end;
end;
registration
cluster non trivial for odd Nat;
existence
proof
3 is non trivial & 2*1+1 is odd;
hence thesis;
end;
cluster non trivial for even Nat;
existence
proof
2 is non trivial & 2*1 is even;
hence thesis;
end;
end;
registration
let a be positive Real, n be Nat;
cluster a|^n -> positive;
coherence;
end;
registration
let a be Integer;
cluster a*a -> square;
coherence
proof
reconsider b = |.a.| as Nat;
b = a or b = -a by COMPLEX1:71; then
b*b = a*a or b*b = (-a)*(-a); then
a*a = b^2 by SQUARE_1:def 1;
hence thesis;
end;
cluster a/a -> square;
coherence
proof
per cases;
suppose a is zero; then
a/a = 0^2;
hence thesis;
end;
suppose a is non zero; then
a/a = 1^2 by XCMPLX_1:60;
hence thesis;
end;
end;
end;
registration
cluster non square for Nat;
existence
proof
3 is not square by PEPIN:41;
hence thesis;
end;
end;
registration
cluster prime -> non square for Nat;
coherence;
end;
registration
cluster even for prime Nat;
correctness
proof
2 is even & 2 is prime by INT_2:28;
hence thesis;
end;
cluster odd for prime Nat;
correctness
proof
2*1+1 is odd & 3 is prime by PEPIN:41;
hence thesis;
end;
end;
registration
cluster prime -> non square for Integer;
coherence
proof
let p be Integer;
assume p is prime; then
reconsider p as non square Element of NAT by ORDINAL1:def 12;
p is non square;
hence thesis;
end;
end;
registration
let a be square Nat;
cluster sqrt a -> natural;
coherence
proof
reconsider a as Nat;
consider m be Nat such that
A0: m^2 = a by PYTHTRIP:def 3;
thus thesis by A0,SQUARE_1:def 2;
end;
end;
registration
let a be Integer;
cluster a|^2 -> square;
coherence
proof
a|^2 = a^2
.=|.a.|^2 by COMPLEX1:75;
hence thesis;
end;
cluster a*a -> square;
coherence;
end;
registration
cluster non square for Integer;
existence by INT_2:28;
end;
registration
cluster zero -> trivial for Nat;
correctness;
end;
registration
cluster square for Nat;
existence
proof
0*0 = 0^2;
hence thesis;
end;
end;
registration
cluster non zero for Element of NAT;
existence by INT_2:28;
cluster non trivial for square Element of NAT;
existence
proof
A1: 2^2 = 2*2 by SQUARE_1:def 1;
4 is non trivial Element of NAT by NAT_2:def 1;
hence thesis by A1;
end;
end;
registration
cluster non trivial for square Nat;
existence
proof
A1: 2^2 = 2*2 by SQUARE_1:def 1;
4 is non trivial Element of NAT by NAT_2:def 1;
hence thesis by A1;
end;
end;
registration
cluster trivial -> square for Nat;
coherence
proof
1*1 = 1^2 & 0*0 = 0^2;
hence thesis by NAT_2:def 1;
end;
end;
registration
cluster non square -> non zero for Integer;
coherence;
end;
theorem NAT31:
for a,b,c,d be Integer holds
a divides b & c divides d implies a*c divides b*d by NAT_3:1;
theorem LCM1:
for a,b be Integer holds
a divides b iff a lcm b = |.b.|
proof
let a,b be Integer;
thus a divides b implies a lcm b= |.b.|
proof
assume a divides b; then
|.b.| = |.a.| lcm |.b.| by INT_2:16, NEWTON:44;
hence thesis by Def2;
end;
assume a lcm b = |.b.|; then
|.a.| lcm |.b.| = |.b.| by Def2;
hence thesis by NEWTON:44,INT_2:16;
end;
registration
let a be Integer;
reduce a lcm 0 to 0;
reducibility by INT_2:4;
end;
registration
let a be Nat;
reduce a lcm 1 to a;
reducibility by NEWTON:46;
end;
registration let a,b;
reduce a*b lcm a to a*b;
reducibility
proof
a divides a*b; then
a lcm a*b = |.a*b.| by LCM1;
hence thesis;
end;
reduce (a gcd b) lcm b to b;
reducibility by NEWTON:53;
reduce a gcd (a lcm b) to a;
reducibility by NEWTON:54;
end;
theorem NATD29:
for a,b be Integer holds
|.a*b.| = (a gcd b)*(a lcm b)
proof
let a,b be Integer;
|.a*b.| = |.a.|*|.b.| by COMPLEX1:65
.= (|.a.|gcd |.b.|)*(|.a.| lcm |.b.|) by NAT_D:29
.= (a gcd b)*(|.a.| lcm |.b.|) by INT_2:34
.= (a gcd b)*(a lcm b) by INT_2:33;
hence thesis;
end;
theorem LmLCM:
for a,b be Integer holds a|^n lcm b|^n = (a lcm b)|^n
proof
let a,b be Integer;
A2: a|^n gcd b|^n = (a gcd b)|^n by NEWTON027;
A3: |.a|^n*b|^n.| = (a|^n gcd b|^n)*(a|^n lcm b|^n) &
|.a*b.| = (a gcd b)*(a lcm b) by NATD29; then
A4: (a|^n gcd b|^n)*(a|^n lcm b|^n) = |.(a*b)|^n.| by NEWTON:7
.= ((a gcd b)*(a lcm b))|^n by A3,TAYLOR_2:1
.= (a gcd b)|^n*(a lcm b)|^n by NEWTON:7
.= (a|^n gcd b|^n)*(a lcm b)|^n by NEWTON027;
per cases;
suppose (a gcd b) = 0; then
a = 0 & b = 0;
hence thesis;
end;
suppose (a gcd b) <> 0;
hence thesis by A2,A4,XCMPLX_1:5;
end;
end;
registration
let a,b be square Nat;
cluster a gcd b -> square;
coherence
proof
reconsider t = sqrt a as Element of NAT by ORDINAL1:def 12;
reconsider q = sqrt b as Element of NAT by ORDINAL1:def 12;
A1: t^2 = a & q^2 = b by SQUARE_1:def 2;
t^2 gcd q^2 = (t gcd q)^2 by NEWTON02:7;
hence thesis by A1;
end;
cluster a lcm b -> square;
coherence
proof
reconsider t = sqrt a, q = sqrt b as Element of NAT by ORDINAL1:def 12;
A1: t^2 = a & q^2 = b by SQUARE_1:def 2;
t^2 lcm q^2 = (t lcm q)^2 by LmLCM;
hence thesis by A1;
end;
end;
registration
let a,b be square Integer;
cluster a gcd b -> square;
coherence
proof
consider x be Nat such that
A1: a = x^2 by PYTHTRIP:def 3;
consider y be Nat such that
A2: b = y^2 by PYTHTRIP:def 3;
a gcd b = (x gcd y)^2 by A1,A2,NEWTON02:7;
hence thesis;
end;
cluster a lcm b -> square;
coherence
proof
consider x be Nat such that
A1: a = x^2 by PYTHTRIP:def 3;
consider y be Nat such that
A2: b = y^2 by PYTHTRIP:def 3;
a lcm b = (x lcm y)^2 by A1,A2,LmLCM;
hence thesis;
end;
end;
theorem ODD:
for t be Integer holds t is odd iff t gcd 2 = 1
proof
let t be Integer;
thus t is odd implies t gcd 2 = 1
proof
assume t is odd; then
consider z be Integer such that
A1: t = 2*z + 1 by ABIAN:1;
t gcd 2 = 1 gcd (1 + 1*1) by A1,NEWTON02:5
.= 1;
hence thesis;
end;
t gcd 2 <> |.2.| implies not 2 divides t by NEWTON02:3;
hence thesis;
end;
definition
let t be Integer;
redefine attr t is odd means :Def3: :: redefines odd (ABIAN, antonym) → even (ABIAN, definition)
t gcd 2 = 1;
compatibility by ODD;
end;
registration
let a be odd Integer;
cluster |.a.| -> odd;
coherence
proof
1 = a gcd 2 by Def3;
hence thesis by INT_6:14;
end;
cluster -a -> odd;
coherence
proof
1 = |.a.| gcd 2 by Def3
.= |.-a.| gcd 2 by COMPLEX1:52;
hence thesis by INT_6:14;
end;
end;
registration
let a,b be even Integer;
cluster a gcd b -> even;
coherence by NEWTON02:9;
end;
registration
let a be Integer;
let b be odd Integer;
cluster a gcd b -> odd;
coherence by NEWTON02:9;
end;
registration
let a be Nat;
reduce |.-a.| to a;
reducibility
proof
|.-a.| = -(-a) by ABSVALUE:30;
hence thesis;
end;
end;
registration
let t,z be even Integer;
cluster t + z -> even;
correctness;
cluster t - z -> even;
correctness;
cluster t*z -> even;
correctness;
end;
registration
let t,z be odd Integer;
cluster t + z -> even;
coherence;
cluster t - z -> even;
coherence;
cluster t*z -> odd;
coherence;
end;
registration
let t be odd Integer, z be even Integer;
cluster t + z -> odd;
coherence;
cluster t - z -> odd;
coherence;
cluster t*z -> even;
coherence;
end;
theorem PT1:
for a be non zero square Integer, b be Integer holds
a*b is square implies b is square
proof
let a be non zero square Integer, b be Integer;
assume
A1: a*b is square;
consider x be Nat such that
A2: a = x^2 by PYTHTRIP:def 3;
consider y be Nat such that
A3: a*b = y^2 by A1,PYTHTRIP:def 3;
x^2 divides y^2 by A2,A3; then
|.x.| divides |.y.| by PYTHTRIP:6; then
consider k be Integer such that
A4: y = k*x;
A5: k*k = k^2 & x*x = x^2 & y*y = y^2 by SQUARE_1:def 1;
a*b = a*k^2 by A2,A3,A4,A5; then
b = k^2 by XCMPLX_1:5
.= |.k.|^2 by COMPLEX1:75;
hence thesis;
end;
registration
let a be square Nat, n be Nat;
cluster a|^n -> square;
coherence
proof
consider k be Nat such that
A1: k^2 = a by PYTHTRIP:def 3;
a|^n = k|^(2*n) by A1,NEWTON:9
.= (k|^n)^2 by NEWTON:9;
hence thesis;
end;
end;
registration
let a be square Integer, n be Nat;
cluster a|^n -> square;
coherence
proof
reconsider a as square Element of NAT by ORDINAL1:def 12;
a|^n is square;
hence thesis;
end;
end;
registration
let a be non zero square Integer, b be non square Integer;
cluster a*b -> non square;
coherence by PT1;
end;
registration
let a be Nat;
let b be even Nat;
cluster a|^b -> square;
coherence
proof
reconsider x = b/2 as Nat;
reconsider k = a|^x as Element of NAT by ORDINAL1:def 12;
a|^(2*x) = (a|^x)|^2 by NEWTON:9;
hence thesis;
end;
end;
registration
let a be non square Nat;
let b be odd Nat;
cluster a|^b -> non square;
coherence
proof
reconsider x = (b-1)/2 as Nat;
reconsider k = a|^(2*x) as square Nat;
a|^(2*x+1) = a|^(2*x)*a by NEWTON:6;
hence thesis;
end;
end;
LmNAT: for a,n be Nat, x be non negative Real holds
a|^n < x|^n < (a+1)|^n implies x is not Nat
proof
let a,n be Nat, x be non negative Real;
assume a|^n < x|^n < (a+1)|^n; then
a < x < (a+1) by NEWTON02:41;
hence thesis by NAT_1:13;
end;
registration
let a be non zero square Integer;
cluster a+1 -> non square;
coherence
proof
consider b be Nat such that
A1: a = b^2 by PYTHTRIP:def 3;
a = b*b by A1,SQUARE_1:def 1; then
b > 0; then
A2: (b*b +1) + 2*b > (b*b + 1) + 0 by XREAL_1:6;
A3: b*b = b^2 & (b+1)*(b+1) = (b+1)^2 by SQUARE_1:def 1;
b*b + 1 > b*b + 0 by XREAL_1:6; then
not ex k be Nat st b^2 + 1 = k^2 by A2,A3,LmNAT;
hence thesis by A1,PYTHTRIP:def 3;
end;
end;
registration
let a be non zero square object, b be non square Nat;
cluster a*b -> non square;
coherence;
end;
registration
let a be non zero square Integer;
let n,m be Nat;
cluster a|^n + a|^m -> non square;
coherence
proof
per cases;
suppose
n >= m; then
consider x be Nat such that
A1: n = m + x by NAT_1:10;
reconsider l = a|^x as non zero square Integer;
a|^(m+x) + a|^m = a|^m*a|^x + a|^m by NEWTON:8
.= (l+1)*(a|^m);
hence thesis by A1;
end;
suppose
m > n; then
consider x be Nat such that
A1: m = n + x by NAT_1:10;
reconsider l = a|^x as non zero square Integer;
a|^(n+x) + a|^n = a|^n*a|^x + a|^n by NEWTON:8
.= (l+1)*(a|^n);
hence thesis by A1;
end;
end;
end;
registration
let a be non zero square Nat;
let n,m be Nat;
cluster a|^n + a|^m -> non square;
coherence;
end;
registration
let a be non zero square Integer;
let p be prime Nat;
cluster p*a -> non square;
coherence;
end;
registration
let a be non trivial Nat;
cluster a-1 -> non zero;
coherence;
end;
registration
let q be square Integer;
cluster |.q.| -> square;
coherence;
end;
registration
let x be non zero Integer;
cluster |.x.| -> non zero;
coherence by COMPLEX1:47;
end;
registration
let a be non trivial square Nat;
cluster a-1 -> non square;
coherence
proof
assume not thesis; then
reconsider k = a-1 as square Element of NAT by ORDINAL1:def 12;
k + 1 is non square;
hence contradiction;
end;
end;
LmN30: for a,b be non square Nat holds
a,b are_coprime implies a*b is non square
proof
let a,b be non square Nat;
assume
A1: a,b are_coprime;
assume not thesis; then
consider k be Nat such that
A2: a*b = k^2 by PYTHTRIP:def 3;
ex k st k|^2 = a by A1,A2,NEWTON02:30;
hence contradiction;
end;
COMPLEX175:
for a be Integer holds |.a.||^2 = a|^2
proof
let a be Integer;
thus |.a.||^2 = |.a.|^2
.= a^2 by COMPLEX1:75
.= a|^2;
end;
registration
let a be non trivial Nat;
cluster a*(a-1) -> non square;
coherence
proof
per cases;
suppose
a is square;
hence thesis;
end;
suppose
a is non square; then
reconsider a as non square Nat;
per cases;
suppose a - 1 is square;
hence thesis;
end;
suppose
a - 1 is non square; then
reconsider k = a-1 as non square Element of NAT by ORDINAL1:def 12;
a-1,(a-1)+1 are_coprime; then
a*k is non square by LmN30;
hence thesis;
end;
end;
end;
end;
registration
let a,b be Integer, n,m be Nat;
cluster ((a|^n+b|^n)*(a|^m-b|^m)+(a|^m+b|^m)*(a|^n-b|^n)) -> even;
coherence
proof
((a|^n+b|^n)*(a|^m-b|^m)+(a|^m+b|^m)*(a|^n-b|^n))/2*2 =
(a|^(n+m) - b|^(n+m))*2 by NEWTON01:5;
hence thesis;
end;
cluster ((a|^n+b|^n)*(a|^m+b|^m)+(a|^m-b|^m)*(a|^n-b|^n)) -> even;
coherence
proof
((a|^n+b|^n)*(a|^m+b|^m)+(a|^m-b|^m)*(a|^n-b|^n))/2*2 =
(a|^(n+m) + b|^(n+m))*2 by NEWTON01:8;
hence thesis;
end;
end;
registration
let a be even Integer;
cluster a/2 -> integer;
coherence;
end;
registration
let a,b be non zero Nat;
cluster a+b -> non trivial;
coherence
proof
b >= 1 by NAT_1:14; then
a + b > 0 + 1 by XREAL_1:8;
hence thesis;
end;
end;
registration
let b be non zero Nat, a,c be non trivial Nat;
reduce c |-count c|^(a |-count b) to (a |-count b);
reducibility by Def0,NAT_3:25;
end;
Lemma1:
for a being Integer holds a / |.a.| is Integer
proof
let a be Integer;
per cases;
suppose a >= 0; then
a / |.a.| = a / a by ABSVALUE:def 1;
hence thesis;
end;
suppose A1: a < 0; then
a / |.a.| = a / (-a) by ABSVALUE:def 1
.= -1 by A1,XCMPLX_1:198;
hence thesis;
end;
end;
registration
let a,b be Integer;
cluster a / (a gcd b) -> integer;
coherence
proof
per cases;
suppose A0: a <> 0 & b <> 0;
(a gcd b) divides a by INT_2:def 2; then
consider k be Integer such that
A1: a = (a gcd b) * k;
a / (a gcd b) = k by A0,A1,XCMPLX_1:89;
hence thesis;
end;
suppose a = 0;
hence thesis;
end;
suppose
B1: b = 0 & a <> 0; then
reconsider b as zero Integer;
reconsider a as non zero Integer by B1;
a/(a gcd b) = a/|.a.| by INT_2:12, NEWTON02:3;
hence thesis by Lemma1;
end;
end;
cluster a / (b gcd a) -> integer;
coherence;
cluster (a lcm b) / b -> integer;
coherence
proof
per cases;
suppose A0: a <> 0 & b <> 0;
b divides (a lcm b) by INT_2:def 1; then
consider k be Integer such that
A1: a lcm b = b * k;
(a lcm b) / b = k by A0,A1,XCMPLX_1:89;
hence thesis;
end;
suppose a = 0 or b = 0;
hence thesis;
end;
end;
cluster (a lcm b) / (a gcd b) -> integer;
coherence
proof
per cases;
suppose A0: a <> 0 & b <> 0;
A1: (a gcd b) divides a by INT_2:def 2;
a divides (a lcm b) by INT_2:def 1; then
(a gcd b) divides (a lcm b) by A1,INT_2:9; then
consider k be Integer such that
A2: (a lcm b) = (a gcd b) * k;
(a lcm b) / (a gcd b) = k by A0,A2,XCMPLX_1:89;
hence thesis;
end;
suppose a = 0 or b = 0;
hence thesis;
end;
end;
end;
registration
let a be even Integer;
reduce a gcd 2 to 2;
reducibility
proof
2 divides a by ABIAN:def 1; then
consider k be Integer such that
A1: a = 2*k;
k,1 are_coprime; then
2*k gcd 2*1 = |.2.| by INT_2:24;
hence thesis by A1;
end;
end;
registration
cluster non zero for even Nat;
existence
proof
2 is even & 2 is non zero;
hence thesis;
end;
end;
registration
let a be even Integer, n be non zero Nat;
cluster a*n -> even;
coherence;
cluster a|^n -> even;
coherence;
end;
registration
let a be Integer, n be zero Nat;
cluster a*n -> even;
coherence;
cluster a|^n -> odd;
coherence
proof
1*a|^n is odd;
hence thesis;
end;
end;
registration
let a be Nat;
reduce |.a.| to a;
reducibility;
end;
registration
let a be non negative Real;
let n be non zero Nat;
reduce n-root (a|^n) to a;
reducibility
proof
n >= 1 & a >= 0 by NAT_1:14;
hence thesis by POWER:4;
end;
reduce (n-root a)|^n to a;
reducibility
proof
n >= 1 & a >= 0 by NAT_1:14;
hence thesis by POWER:4;
end;
end;
:: solvable by ATP, yet not by verifier
theorem INT29:
not a divides b implies not a*c divides b
proof
a divides a*c;
hence thesis by INT_2:9;
end;
:: Roots
:: see PEPIN:30;
theorem POW1:
for a,b be non negative Real, n be positive Nat holds
a|^n = b|^n iff a = b
proof
let a,b be non negative Real, n be positive Nat;
(a > b implies a|^n > b|^n) &
(a < b implies a|^n < b|^n) by NEWTON02:40;
hence thesis by XXREAL_0:1;
end;
registration
let a be Real, n be even Nat;
cluster a|^n -> non negative;
coherence
proof
per cases;
suppose
a >= 0;
hence thesis;
end;
suppose
a < 0;
hence thesis;
end;
end;
end;
registration
let a be negative Real, n be odd Nat;
cluster a|^n -> negative;
coherence
proof
(-a)|^n is positive; then
-(a|^n) is positive by POWER:2;
hence thesis;
end;
end;
theorem POW2:
for a,b be Real, n be odd Nat holds a|^n = b|^n iff a = b
proof
let a,b be Real, n be odd Nat;
per cases;
suppose
A1: a >= 0;
per cases;
suppose b >= 0;
hence thesis by A1,POW1;
end;
suppose b < 0;
hence thesis by A1;
end;
end;
suppose
A2: a < 0;
per cases;
suppose b < 0; then
reconsider k = -b as positive Real;
reconsider l = -a as positive Real by A2;
B1: (-a)|^n = -(a|^n) & (-b)|^n = -(b|^n) by POWER:2;
k|^n = l|^n iff k = l by POW1;
hence thesis by B1;
end;
suppose b >= 0;
hence thesis by A2;
end;
end;
end;
theorem
for a,b st a,b are_coprime holds for n be non zero Nat holds
a*b = c|^n iff
(n-root a in NAT & n-root b in NAT & c = (n-root a)*(n-root b))
proof
let a,b such that
A1: a,b are_coprime;
let n be non zero Nat;
thus a*b = c|^n implies
(n-root a in NAT & n-root b in NAT & c = (n-root a)*(n-root b))
proof
assume
B1: a*b = c|^n; then
consider k such that
B2: a = k|^n by A1,NEWTON02:30;
consider l such that
B3: b = l|^n by A1,B1, NEWTON02:30;
n-root c|^n = n-root (a*b) by B1
.= (n-root a)*(n-root b) by POWER:11,NAT_1:14
.=(n-root k|^n)*(n-root l|^n) by B2,B3;
hence thesis by ORDINAL1:def 12,B2,B3;
end;
assume
n-root a in NAT & n-root b in NAT & c = (n-root a)*(n-root b); then
c|^n = (n-root a)|^n*(n-root b)|^n by NEWTON:7;
hence thesis;
end;
:: DIVISION
theorem POWD:
for n be non zero Nat, a be Integer, b be Integer holds
b|^n divides a|^n iff b divides a
proof
let n be non zero Nat, a be Integer, b be Integer;
thus b|^n divides a|^n implies b divides a
proof
assume
A1: b|^n divides a|^n;
|.b.||^n = |.b|^n.| by TAYLOR_2:1
.= b|^n gcd a|^n by A1,NEWTON02:3
.= (b gcd a)|^n by NEWTON027;
hence thesis by NEWTON02:3,WSIERP_1:3;
end;
thus thesis by NEWTON02:15;
end;
theorem NEWTON89:
for a be Integer, m,n be Nat st
m >= n holds a|^n divides a|^m
proof
let a be Integer, m,n be Nat;
A1: |.a|^n.| = |.a.||^n & |.a|^m.| = |.a.||^m by TAYLOR_2:1;
assume m >= n;
hence thesis by INT_2:16,A1,NEWTON:89;
end;
LmX: for a,b be Integer holds
a|^m divides b & not a|^n divides b implies n > m
proof
let a,b be Integer;
assume
A1: a|^m divides b & not a|^n divides b;
assume not thesis; then
a|^n divides a|^m by NEWTON89;
hence contradiction by A1,INT_2:9;
end;
theorem LmY:
for a,b be Integer holds
a divides b & b|^m divides c implies a|^m divides c
proof
let a,b be Integer;
assume
A1: a divides b & b|^m divides c; then
a gcd b = |.a.| by NEWTON02:3; then
(a|^m gcd b|^m) = |.a.||^m by NEWTON027
.= |.a|^m.| by TAYLOR_2:1; then
a|^m divides b|^m by NEWTON02:3;
hence thesis by A1,INT_2:9;
end;
theorem
for a,p be Integer st
p|^(2*n+k) divides a|^2 holds p|^n divides a
proof
let a,p be Integer;
assume
A1: p|^(2*n+k) divides a|^2;
p|^(2*n) divides p|^(2*n+k) by NAT_1:11,NEWTON89; then
p|^(2*n) divides a|^2 by A1,INT_2:9; then
A2: (p|^n)|^2 divides a|^2 by NEWTON:9;
|.p|^n.||^2 = |.(p|^n)|^2.| by TAYLOR_2:1
.= (p|^n)|^2 gcd a|^2 by A2,NEWTON02:3
.= ((p|^n) gcd a)|^2 by NEWTON027;
hence thesis by POW1,NEWTON02:3;
end;
theorem
for a,b be odd square Nat holds 8 divides a - b
proof
let a,b be odd square Nat;
consider c such that
A1: a = c^2 by PYTHTRIP:def 3;
consider d such that
A2: b = d^2 by PYTHTRIP:def 3;
c is odd & d is odd & a = c|^2 & b = d|^2 by A1,A2;
hence thesis by NEWTON02:63;
end;
theorem
for a,b be odd Nat holds 4 divides a-b implies not 4 divides a|^n + b|^n
proof
let a,b be odd Nat;
assume
A1: 4 divides a-b;
per cases;
suppose n is odd;
hence thesis by A1,NEWTON02:69;
end;
suppose n is even; then
4 divides a|^n - b|^n by NEWTON02:65;
hence thesis by NEWTON02:58;
end;
end;
theorem
for a,b be odd Nat holds
(4 divides a|^n + b|^n) implies not 4 divides a|^(2*n) + b|^(2*n)
proof
let a,b be odd Nat;
A0: (a|^n)|^2 = a|^(2*n) & (b|^n)|^2 = b|^(2*n) by NEWTON:9;
assume 4 divides a|^n + b|^n; then
4 divides (a|^n + b|^n)*(a|^n - b|^n) by INT_2:2; then
4 divides a|^(2*n) - b|^(2*n) by A0,NEWTON01:1;
hence thesis by NEWTON02:58;
end;
theorem
for a,b be odd Nat holds
(4 divides a|^n - b|^n) implies not 4 divides a|^(2*n) + b|^(2*n)
proof
let a,b be odd Nat;
A0: (a|^n)|^2 = a|^(2*n) & (b|^n)|^2 = b|^(2*n) by NEWTON:9;
assume 4 divides a|^n - b|^n; then
4 divides (a|^n + b|^n)*(a|^n - b|^n) by INT_2:2; then
4 divides (a|^n)|^2 - (b|^n)|^2 by NEWTON01:1;
hence thesis by NEWTON02:58,A0;
end;
theorem Even:
for a,b be odd Nat holds
2|^m divides a|^n - b|^n implies 2|^(m+1) divides a|^(2*n) - b|^(2*n)
proof
let a,b be odd Nat;
A0: a|^(2*n) = (a|^n)|^2 & b|^(2*n) = (b|^n)|^2 by NEWTON:9;
assume
A1: 2|^m divides a|^n - b|^n;
A2: 2 divides a|^n + b|^n by ABIAN:def 1;
a|^(2*n) - b|^(2*n) = (a|^n - b|^n)*(a|^n + b|^n) by A0,NEWTON01:1; then
2*2|^m divides a|^(2*n) - b|^(2*n) by A1,A2,NEWTON02:2;
hence thesis by NEWTON:6;
end;
theorem N3:
a1|^3 - b1|^3 = (a1 - b1)*(a1|^2 + b1|^2 + a1*b1)
proof
a1|^(2+1) - b1|^(2+1) = a1|^2*(a1|^1 - b1|^1) + b1|^1*(a1|^2 - b1|^2)
by RI2
.= a1|^2*(a1-b1)+b1*((a1+b1)*(a1-b1)) by NEWTON01:1
.= (a1-b1)*(a1|^2+ b1*b1 + a1*b1);
hence thesis by NEWTON:81;
end;
:: por NEWTON02:196;
theorem
for n be odd Nat holds 3 divides a|^n + b|^n iff 3 divides a + b
proof
let n be odd Nat;
consider k such that
A0: n = 2*k + 1 by ABIAN:9;
3 divides a|^n + b|^n implies 3 divides a + b
proof
assume
A1: 3 divides a|^n + b|^n;
3 divides a|^n - a & 3 divides b|^n - b by A0,NEWTON02:173; then
3 divides (a|^n - a) + (b|^n - b) by WSIERP_1:4; then
3 divides (a|^n + b|^n) + -(a + b); then
3 divides -(a+b) by A1,INT_2:1;
hence thesis by INT_2:10;
end;
hence thesis by A0,NEWTON02:196,PEPIN:41;
end;
theorem D3:
for c be Integer holds c divides (a-b) implies c divides a|^n - b|^n
proof
let c be Integer;
assume
A1: c divides (a-b);
(a-b) divides (a|^n - b|^n) by NEWTON01:33;
hence thesis by A1,INT_2:9;
end;
theorem
for n be odd Nat holds 3 divides a|^n - b|^n iff 3 divides a - b
proof
let n be odd Nat;
consider k such that
A0: n = 2*k + 1 by ABIAN:9;
3 divides a|^n - b|^n implies 3 divides a - b
proof
assume
A1: 3 divides a|^n - b|^n;
3 divides a|^n - a & 3 divides -(b|^n - b)
by A0,NEWTON02:173,INT_2:10; then
3 divides (a|^n - a) + -(b|^n - b) by WSIERP_1:4; then
3 divides (a|^n - b|^n) + -(a - b); then
3 divides -(a-b) by A1,INT_2:1;
hence thesis by INT_2:10;
end;
hence thesis by D3;
end;
theorem
for n be Nat holds a|^n, (a-b)|^n are_congruent_mod b
proof
b divides ((a-b)+b)|^n - (a-b)|^n by NEWTON02:10;
hence thesis;
end;
theorem
for a be non trivial Nat holds
ex n be prime Nat st n divides a
proof
let a be non trivial Nat;
per cases;
suppose a is prime;
hence thesis;
end;
suppose not a is prime; then
ex n be Element of NAT st n > 1 & n*n <= a & n is prime &
n divides a by NAT_4:14,Def0;
hence thesis;
end;
end;
theorem PSQ:
for p be prime Nat holds p divides (p+(k+1))*(p-(k+1)) implies k+1 >= p
proof
let p be prime Nat;
p divides p*p; then
A1: p divides p|^2 by NEWTON:81;
A2: p|^2 = (p|^2 - (k+1)|^2)+(k+1)|^2;
assume p divides (p+(k+1))*(p-(k+1)); then
p divides p|^2 - (k+1)|^2 by NEWTON01:1;then
p divides (k+1)|^2 by A1,A2,INT_2:1;
hence thesis by NAT_D:7,NAT_3:5;
end;
theorem
for p be prime Nat, k be non zero Nat st k < p holds
not p divides p|^2 - k|^2
proof
let p be prime Nat, k be non zero Nat;
reconsider a = k-1 as Nat;
p divides (p - (a+1))*(p + (a+1)) implies a+1 >= p by PSQ;
hence thesis by NEWTON01:1;
end;
theorem SUD:
for a,b be Integer, p be odd prime Nat st not p divides b holds
p divides (a-b) implies not p divides (a+b)
proof
let a,b be Integer, p be odd prime Nat such that
A1: not p divides b;
p gcd 2 = 1 by Def3; then
not p divides 2 by INT_2:28, PEPIN:2, PYTHTRIP:def 2; then
A2: not p divides 2*b by A1,INT_5:7;
assume p divides (a-b); then
not p divides ((a-b) + 2*b) by A2,INT_2:1;
hence thesis;
end;
LmSQ: for p be prime Nat, k be square Nat holds
p divides k implies p^2 divides k
proof
let p be prime Nat, k be square Nat;
consider a be Nat such that
A1: a^2 = k by PYTHTRIP:def 3;
assume p divides k;
hence thesis by A1,NAT_3:5,NEWTON02:15;
end;
theorem
for a be non zero square Nat, p be prime Nat st
p divides a holds not a+p is square
proof
let a be non zero square Nat;
let p be prime Nat;
assume
B0: p divides a; then
consider k such that
B1: a = p*k by NAT_D:def 3;
B3: not p is trivial;
p^2 divides a by B0,LmSQ; then
p*p divides p*k by B1,SQUARE_1:def 1; then
p divides k by INT_4:7; then
consider n such that
B4: k = p*n by NAT_D:def 3;
not p divides 1*(k+1) by B3,INT_2:13,B4,NEWTON02:77; then
not p*p divides p*(k+1) by INT_4:7; then
not p^2 divides p*(k+1) by SQUARE_1:def 1;
hence thesis by B1,LmSQ,INT_1:def 3;
end;
theorem
for a be non zero square Nat, p be prime Nat holds
a+p is square implies p = 2*sqrt(a) + 1
proof
let a be non zero square Nat;
let p be prime Nat;
assume a+p is square; then
consider m such that
B2: a+p = m^2 by PYTHTRIP:def 3;
consider n such that
B3: a = n^2 by PYTHTRIP:def 3;
B4: p = m^2 - n^2 by B2,B3
.= (m-n)*(m+n) by NEWTON01:1;
m - n > 0 by B4; then
reconsider l = m-n as Element of NAT by INT_1:3;
(m-n) divides p & (m+n) divides p by B4; then
B5: ((m+n) = p or (m+n)=1) & (l = p or l=1) by INT_2:def 4;
n >= -n & not p is trivial; then
n+m >= -n+m & p > 1 by XREAL_1:6; then
p = 2*n + 1 by B4,B5;
hence thesis by B3,SQUARE_1:def 2;
end;
theorem
for a,b,c be Integer st a,b are_coprime holds
c gcd (a*b) = (c gcd a)*(c gcd b)
proof
let a,b,c be Integer such that
A1: a,b are_coprime;
reconsider k = |.a.|, l = |.b.|, m = |.c.| as Nat;
A2: k,l are_coprime by A1,INT_2:34;
|.a.|*|.b.| = |.a*b.| by COMPLEX1:65; then
c gcd (a*b) = m gcd (k*l) & c gcd a = m gcd k & c gcd b = m gcd l
by INT_2:34;
hence thesis by A2,NAT_5:17;
end;
theorem
for p be prime Nat holds a divides p|^n implies ex k st a = p|^k
proof
let p be prime Nat;
assume a divides p|^n; then
ex k be Nat st a = p|^k & k <= n by GROUPP_1:2;
hence thesis;
end;
theorem
for a,b be non zero Nat, p be prime Nat st a + b = p holds a,b are_coprime
proof
let a,b be non zero Nat, p be prime Nat;
A1: a+b > a+0 by XREAL_1:6;
assume
A2: a+b = p; then
a,p are_coprime by A1,NAT_D:7,NAT_6:6;
hence thesis by A2,NEWTON02:45;
end;
theorem
for a,b be non zero Nat, p be prime Nat holds
a|^n + b|^n = p|^n implies a,b are_coprime
proof
let a,b be non zero Nat, p be prime Nat;
A1: a|^n+b|^n > a|^n+0 by XREAL_1:6;
assume
A2: a|^n + b|^n = p|^n; then
reconsider n as non zero Nat;
a|^n < p|^n by A1,A2; then
a < p by NEWTON02:40; then
a,p are_coprime by NAT_D:7,NAT_6:6; then
a|^n, p|^n are_coprime by WSIERP_1:11; then
a|^n, b|^n are_coprime by A2,NEWTON02:45; then
a, b|^n are_coprime by NEWTON02:73;
hence thesis by NEWTON02:73;
end;
theorem
for a,b be non zero Nat st c >= a+b holds
c|^(k+1)*(a+b) > a|^(k+2) + b|^(k+2)
proof
let a,b be non zero Nat;
A1: a|^(1) + b|^(1) <= (a+b)|^(1) implies
a|^((k+1)+1) + b|^((k+1)+1) < (a+b)|^((k+1)+1) by NEWTON01:18;
assume c >= a+b; then
c|^(k+1) >= (a+b)|^(k+1) by NEWTON02:40; then
c|^(k+1)*(a+b) >= (a+b)|^(k+1)*(a+b) by XREAL_1:64; then
c|^(k+1)*(a+b) >= (a+b)|^((k+1)+1) by NEWTON:6;
hence thesis by A1,XXREAL_0:2;
end;
theorem
for a,c be Nat, b be non zero Nat holds
a*b < c < a*(b+1) implies not a divides c & not c divides a
proof
let a,c be Nat, b be non zero Nat;
assume
A1: a*b < c < a*(b+1); then
reconsider c as non zero Nat;
reconsider a as non zero Nat by A1;
assume not thesis; then
per cases;
suppose a divides c;
then consider k be Nat such that
B1: c = a*k by NAT_D:def 3;
b < k by A1,B1,XREAL_1:64; then
b + 1 <= k by NAT_1:13;
hence contradiction by A1,B1,XREAL_1:64;
end;
suppose
B1: c divides a;
a*b >= a*1 by XREAL_1:64,NAT_1:14; then
c > a by A1,XXREAL_0:2;
hence thesis by B1,NAT_D:7;
end;
end;
theorem MinMax:
for a,b be Real holds
a + b = min(a,b) + max(a,b)
proof
let a,b be Real;
per cases;
suppose a >= b; then
a = max(a,b) & b = min(a,b) by XXREAL_0:def 9,def 10;
hence thesis;
end;
suppose a < b; then
a = min(a,b) & b = max(a,b) by XXREAL_0:def 9,def 10;
hence thesis;
end;
end;
:: max (a*b,a*c) = a*max(b,c) & min (a*b,a*c) = a*min(b,c) by FUZZY_2:41;
:: max (a+b,a+c) = a+max(b,c) & min (a+b,a+c) = a+min(b,c) by FUZZY_2:42;
theorem MM1:
for a,b be non negative Real holds
max(a|^n,b|^n) = (max(a,b))|^n & min (a|^n,b|^n) = (min(a,b))|^n
proof
let a,b be non negative Real;
per cases;
suppose
a >= b; then
a|^n = max(a|^n,b|^n) & b|^n = min(a|^n,b|^n) &
a = max(a,b) & b = min(a,b) by NEWTON02:41,XXREAL_0:def 9,def 10;
hence thesis;
end;
suppose
a < b; then
b|^n = max(a|^n,b|^n) & a|^n = min(a|^n,b|^n) &
b = max(a,b) & a = min(a,b) by NEWTON02:41,XXREAL_0:def 9,def 10;
hence thesis;
end;
end;
theorem
for p be prime Nat holds
a*b = p|^n implies ex k,l be Nat st
a = p|^k & b= p|^l & k+l = n
proof
let p be prime Nat;
assume
A1: a*b = p|^n; then
a divides p|^n; then
consider k be Nat such that
A2: a = p|^k & k <= n by GROUPP_1:2;
b divides p|^n by A1; then
consider l be Nat such that
A3: b = p|^l & l <= n by GROUPP_1:2;
p|^n = p|^(k+l) by NEWTON:8,A1,A2,A3; then
n = k+l by PEPIN:30,Def0;
hence thesis by A2,A3;
end;
:: according to ATP it may be proved by PYTHTRIP:def 1
theorem NTC:
for a,b be non trivial Nat holds
a,b are_coprime implies not a divides b & not b divides a
proof
let a,b be non trivial Nat;
assume a,b are_coprime; then
1 = a gcd (b mod a) & 1 = b gcd (a mod b) by NAT_D:28; then
A3: b mod a <> 0 & a mod b <> 0 by Def0;
a = (a div b)*b + (a mod b) & b = (b div a)*a + (b mod a) by NAT_D:2;
not a = (a div b)*b & not b = (b div a)*a by A3;
hence thesis;
end;
theorem
for a be non trivial Nat, p be prime Nat st p > a holds
not p divides a & not a divides p
proof
let a be non trivial Nat, p be prime Nat;
assume p > a; then
a,p are_coprime by NAT_6:6,NAT_D:7;
hence thesis by NTC;
end;
theorem GCDP:
for p be prime Nat holds
a gcd p = 1 or a gcd p = p
proof
let p be prime Nat;
per cases by NAT_6:6;
suppose p divides a;
hence thesis by NEWTON:49;
end;
suppose
a gcd p = 1;
hence thesis;
end;
end;
theorem
for a be non trivial Nat, p be prime Nat holds
a divides p|^n implies p divides a
proof
let a be non trivial Nat, p be prime Nat;
assume a divides p|^n; then
A1: a gcd p|^n = |.a.| by NEWTON02:3;
per cases by GCDP;
suppose
a gcd p = 1; then
a gcd p|^n = 1 by WSIERP_1:12;
hence thesis by A1,Def0;
end;
suppose a gcd p = p;
hence thesis by INT_2:def 2;
end;
end;
:: Count
theorem SC1:
for a,b be odd Nat, m be even Nat holds
2 |-count (a|^m + b|^m) = 1
proof
let a,b be odd Nat, m be even Nat;
A1: 4 = 2*2 .= 2|^2 by NEWTON:81;
4 divides a|^m - b|^m by NEWTON02:65; then
A2: not 2|^(1+1) divides a|^m + b|^m by A1,NEWTON02:58;
a|^m + b|^m is even; then
2|^1 divides (a|^m + b|^m);
hence thesis by A2,NAT_3:def 7;
end;
LmC1: for a be non zero Nat, p be non trivial Nat holds
(p|^(p |-count a) divides a & not p*p|^(p |-count a) divides a)
proof
let a be non zero Nat, p be non trivial Nat;
a <> 0 & p <> 1 by NAT_2:def 1; then
p |^ (p |-count a) divides a & not p |^ ((p |-count a)+1) divides a
by NAT_3:def 7;
hence thesis by NEWTON:6;
end;
theorem
for a be non zero Nat holds
ex k be odd Nat st a = 2|^(2 |-count a)*k
proof
let a be non zero Nat;
A1: 2 is non trivial; then
consider k such that
A2: a = (2|^(2 |-count a))*k by LmC1,NAT_D:def 3;
not 2*2|^(2 |-count a) divides (2|^(2 |-count a))*k by A1,A2,LmC1; then
k is odd by NEWTON02:2;
hence thesis by A2;
end;
:: must precede definition of |-count for Integers.
theorem
for b be non zero Nat holds
a > b implies ex p be prime Nat st p |-count a > p |-count b
proof
let b be non zero Nat;
assume
A1: a > b; then
reconsider a as non zero Nat;
(for p be prime Nat holds p|-count a <= p|-count b) implies a <= b
proof
assume for p be prime Nat holds p|-count a <= p |-count b; then
for p be Element of NAT st p is prime holds
p|-count a <= p |-count b; then
consider c be Element of NAT such that
B1: b = a*c by NAT_4:20;
c is non zero by B1; then
a*c >= a*1 by NAT_1:14,XREAL_1:64;
hence thesis by B1;
end;
hence thesis by A1;
end;
theorem NAT330:
for a,b,c be Nat st a <> 1 & b <> 0 & c <> 0 &
b > a |-count c holds not a|^b divides c
proof
let a,b,c be Nat;
assume a <> 1 & b <> 0 & c <> 0; then
A2: a|^(a|-count c) divides c & not a|^((a|-count c)+1) divides c
by NAT_3:def 7;
assume b > a |-count c; then
b >= a |-count c + 1 by NAT_1:13; then
consider k be Nat such that
A3: b = (a|-count c + 1) + k by NAT_1:10;
a|^b = a|^(a|-count c + 1)*a|^k by A3,NEWTON:8;
hence thesis by A2,INT29;
end;
theorem CountD:
for b be non zero Integer, a be Integer st |.a.| <> 1 holds
a|^(|.a.| |-count |.b.|) divides b &
not a|^((|.a.||-count |.b.|)+1) divides b
proof
let b be non zero Integer, a be Integer such that
A0: |.a.| <> 1;
reconsider k = |.a.|, l = |.b.| as Nat;
A1: |.a.||^(k |-count l) = |. a|^(k |-count l).| &
|.a.||^((k |-count l) +1) = |.a|^((k |-count l) +1).| by TAYLOR_2:1;
k|^(k |-count l) divides l & not k|^((k |-count l)+1) divides l
by A0,NAT_3:def 7;
hence thesis by A1,INT_2:16;
end;
theorem CountD1:
for b be non zero Integer, a be Integer st |.a.| <> 1 holds
a|^n divides b & not a|^(n+1) divides b implies
n = |.a.| |-count |.b.|
proof
let b be non zero Integer, a be Integer such that
A0: |.a.| <> 1;
reconsider k = |.a.|, l = |.b.| as Nat;
A1: |.a|^n.| = |.a.||^n & |.a|^(n+1).| = |.a.||^(n+1) by TAYLOR_2:1;
assume a|^n divides b & not a|^(n+1) divides b; then
|.a.||^n divides |.b.| & not |.a.||^(n+1) divides |.b.| by A1,INT_2:16;
hence thesis by A0,NAT_3:def 7;
end;
theorem CD:
for b be non zero Nat, a be non trivial Nat holds
a divides b iff a |-count (a gcd b) = 1
proof
let b be non zero Nat, a be non trivial Nat;
reconsider c = a gcd b as non zero Nat;
A1: a > 1 by Def0;
A2: c divides b by INT_2:def 2;
thus a divides b implies a |-count (a gcd b) = 1
proof
assume a divides b; then
a gcd b = |.a.| by NEWTON02:3;
hence thesis by NAT_3:22,Def0;
end;
assume a|-count (a gcd b) = 1; then
a|^1 divides c by A1,NAT_3:def 7;
hence thesis by A2,INT_2:9;
end;
theorem
for b,n be non zero Nat, a be non trivial Nat holds
a |-count (a gcd b) = 1 iff a|^n |-count (a gcd b)|^n = 1
proof
let b,n be non zero Nat, a be non trivial Nat;
a divides b iff a|^n divides b|^n by POWD; then
a |-count (a gcd b) = 1 iff a|^n |-count (a|^n gcd b|^n) = 1 by CD;
hence thesis by NEWTON027;
end;
theorem
for b be non zero Nat, a be non trivial Nat holds
a |-count (a gcd b) = 0 iff not a |-count (a gcd b) = 1
proof
let b be non zero Nat, a be non trivial Nat;
reconsider c = a gcd b as non zero Nat;
a > 1 by Def0; then
L1: a |-count (a gcd b) = 0 iff not a divides (a gcd b) by NAT_3:27;
a gcd b divides b by INT_2:def 2;
hence thesis by CD,INT_2:9,L1;
end;
definition
let a,b be Integer;
func a |-count b -> Nat equals
|.a.| |-count |.b.|;
coherence;
end;
definition
let a be Integer such that
A0: |.a.| <> 1;
let b be non zero Integer;
redefine func a |-count b means :: redefines |-count (NEWTON03, definition)
:Def6:
a|^it divides b & not a|^(it+1) divides b;
compatibility by A0,CountD,CountD1;
end;
theorem NAT328:
for p be prime Nat, a,b be non zero Integer holds
p |-count (a*b) = (p |-count a) + (p |-count b)
proof
let p be prime Nat, a,b be non zero Integer;
reconsider k = |.a.|, l = |.b.| as non zero Nat;
p |-count (a*b) = |.p.| |-count (|.a.|*|.b.|) by COMPLEX1:65
.= |.p.| |-count k + |.p.| |-count l by NAT_3:28;
hence thesis;
end;
theorem Count0:
for a be non trivial Nat, b be non zero Nat holds
a|^(a |-count b) <= b
proof
let a be non trivial Nat, b be non zero Nat;
a <> 1 by Def0; then
a|^(a |-count b) divides b by NAT_3:def 7;
hence thesis by NAT_D:7;
end;
theorem Count1:
for a be non trivial Nat, b be non zero Integer holds
a|^n divides b iff n <= a |-count b
proof
let a be non trivial Nat, b be non zero Integer;
L0: a <> 1 by Def0;
L1: a|^n divides b implies n <= a |-count b
proof
assume
A1: a|^n divides b;
a|^n divides b & not a|^((a |-count b)+1) divides b implies
not a|^((a |-count b)+1) divides a|^n by INT_2:9; then
(a |-count b) + 1 > n by L0,A1,Def6, NEWTON:89;
hence thesis by NAT_1:13;
end;
not a|^(n) divides b implies a |-count b < n
proof
assume
A1: not a|^n divides b;
not a|^n divides b & a|^(a |-count b) divides b implies
not a|^n divides a|^(a |-count b) by INT_2:9;
hence thesis by L0,A1,Def6,NEWTON:89;
end;
hence thesis by L1;
end;
theorem Count2:
for a be non trivial Nat, b be non zero Integer, n be non zero Nat holds
n*(a |-count b) <= a |-count b|^n < n*((a |-count b) + 1)
proof
let a be non trivial Nat, b be non zero Integer, n be non zero Nat;
reconsider k = a |-count b as Nat;
A0: a|^k|^n = a|^(k*n) & a|^(k+1)|^n = a|^((k+1)*n) by NEWTON:9;
a <> 1 by NAT_2:def 1; then
A1: a|^k divides b & not a|^(k+1) divides b by Def6;
a|^k gcd b = |.a|^k.| & a|^(k+1) gcd b <> |.a|^(k+1).|
by A1,NEWTON02:3; then
(a|^k gcd b)|^n = (a|^k)|^n & (a|^(k+1) gcd b)|^n <> (a|^(k+1))|^n
by WSIERP_1:3; then
(a|^k|^n) gcd (b|^n) = |.a|^k|^n.| &
(a|^(k+1)|^n) gcd (b|^n) <> |.a|^(k+1)|^n.| by NEWTON027;
hence thesis by Count1,A0,NEWTON02:3;
end;
theorem
for a be non trivial Nat, b, n be non zero Nat holds
b < a implies a |-count b|^n < n
proof
let a be non trivial Nat, b,n be non zero Nat;
assume
A1: b < a;
b >= 0 + 1 by NAT_1:13; then
A2: a |-count b = 0 by A1,NAT_3:23;
a |-count b|^n < n*((a |-count b)+1) by Count2;
hence thesis by A2;
end;
theorem Count4:
for a be non trivial Nat, b be non zero Nat holds
b < a|^n implies a |-count b < n
proof
let a be non trivial Nat, b be non zero Nat;
assume b < a|^n; then
1*a|^0 divides b & not a|^(0+n) divides b by INT_2:12, NAT_D:7;
hence thesis by Count1;
end;
theorem
for a, b be non zero Nat, n be non trivial Nat holds
(a+b) |-count (a|^n + b|^n) < n
proof
let a,b be non zero Nat, n be non trivial Nat;
reconsider m = n - 1 as non zero Nat;
(a+b)|^1 = a|^1 + b|^1; then
(a+b)|^(1+m) > a|^(1+m) + b|^(1+m) by NEWTON01:18;
hence thesis by Count4;
end;
theorem
for a,b be non zero Nat holds a gcd b = 1 iff
(for c be non trivial Nat holds (c|-count a)*(c|-count b) = 0)
proof
let a,b be non zero Nat;
thus a gcd b = 1 implies
(for c be non trivial Nat holds (c|-count a)*(c|-count b) = 0)
proof
assume a gcd b = 1; then
B1: a,b are_coprime;
for c be non trivial Nat holds (c|-count a)*(c|-count b) = 0
proof
let c be non trivial Nat;
C1: c <> 1 by Def0;
per cases;
suppose
not c divides a; then
c|-count a = 0 by C1,NAT_3:27;
hence thesis;
end;
suppose
c divides a; then
not c divides b by C1,B1,PYTHTRIP:def 1; then
c |-count b = 0 by C1,NAT_3:27;
hence thesis;
end;
end;
hence thesis;
end;
(for c be prime Nat holds (c|-count a)*(c|-count b) = 0) implies a gcd b = 1
proof
assume
B1: for c be prime Nat holds (c|-count a)*(c|-count b) = 0;
for c be prime Nat holds (not c divides a) or (not c divides b)
proof
let c be prime Nat;
C1: c <> 1 by INT_2:def 4;
(c|-count a)*(c|-count b) = 0 by B1; then
((c|-count a) = 0 or (c|-count b) = 0);
hence thesis by C1,NAT_3:27;
end; then
a,b are_coprime by PYTHTRIP:def 2;
hence thesis;
end;
hence thesis;
end;
ABS1: for a,b be Integer holds |.a.| <> |.b.| implies a - b <> 0 & a+b <> 0
proof
let a,b be Integer;
assume
A0: |.a.| <> |.b.|;
per cases by ABSVALUE:1;
suppose
A1: |.a.| = a;
per cases by ABSVALUE:1;
suppose
A2: |.b.| = b;
a <> b & (a <> 0 or b <> 0) by A0;
hence thesis by A1,A2;
end;
suppose
|.b.| = -b;
hence thesis by A0;
end;
end;
suppose
|.a.| = -a;
hence thesis by A0;
end;
end;
theorem
for m be non zero even Nat, a,b be odd Nat st a <> b holds
2 |-count (a|^(2*m) - b|^(2*m)) >= 2 |-count (a|^m - b|^m) + 1
proof
let m be non zero even Nat, a,b be odd Nat such that
A0: a <> b;
reconsider c = a|^(2*m) - b|^(2*m) as non zero Integer by A0,POW1;
reconsider d = a|^m - b|^m as non zero Integer by A0,POW1;
A1: 2 is non trivial;
2 |^(2 |-count d) divides d & not 2 |^((2 |-count d) +1) divides d
by Def6; then
2 |^((2 |-count d) +1) divides c by Even;
hence thesis by A1,Count1;
end;
theorem
for m be non zero even Nat, a,b be odd Nat st a <> b holds
2 |-count (a|^(2*m) - b|^(2*m)) = 2 |-count (a|^m - b|^m) + 1
proof
let m be non zero even Nat, a,b be odd Nat such that
A0: a <> b;
reconsider c = a|^m + b|^m as non zero Nat;
reconsider d = a|^m - b|^m as non zero Integer by A0,POW1;
a|^(2*m) = (a|^m)|^2 & b|^(2*m) = (b|^m)|^2 by NEWTON:9; then
a|^(2*m) - b|^(2*m) = (a|^m - b|^m)*(a|^m + b|^m) by NEWTON01:1; then
2 |-count (a|^(2*m) - b|^(2*m)) = 2 |-count c + 2 |-count d
by NAT328,INT_2:28
.= 2 |-count (a|^m - b|^m) + 1 by SC1;
hence thesis;
end;
theorem
for p be prime Nat, a,b be Integer st |.a.| <> |.b.| holds
p |-count (a|^2 - b|^2) = (p |-count (a-b)) + (p|-count (a+b))
proof
let p be prime Nat, a,b be Integer such that
A1: |.a.| <> |.b.|;
a - b <> 0 & a + b <> 0 by A1,ABS1; then
reconsider t = |.a - b.|, u = |.a + b.| as non zero Nat;
p |-count (a|^2 - b|^2) = p|-count |.(a+b)*(a-b).| by NEWTON01:1
.= p |-count (t*u) by COMPLEX1:65
.= (p |-count |.a-b.|)+ (p|-count |.a+b.|) by NAT_3:28;
hence thesis;
end;
theorem
for p be prime Nat, a,b be Integer st |.a.| <> |.b.| holds
p |-count (a|^3 - b|^3) =
(p |-count (a-b))+ (p|-count (a|^2 + a*b + b|^2))
proof
let p be prime Nat, a,b be Integer such that
A1: |.a.| <> |.b.|;
a - b <> 0 & a+b <> 0 by A1,ABS1; then
reconsider t = |.a - b.| as non zero Nat;
A3: |.a.||^2 = a|^2 & |.b.||^2 = b|^2 by COMPLEX175;
2*|.a.|*|.b.| < |.a.||^2 + |.b.||^2 by A1,NEWTON02:55; then
2*(|.a.|*|.b.|) < a|^2 + b|^2 by A3; then
A4: 2*|.a*b.| < a|^2 + b|^2 by COMPLEX1:65;
2*|.a*b.| >= 1*|.a*b.| by XREAL_1:64; then
A5: a|^2 + b|^2 > |.a*b.| by A4, XXREAL_0:2;
|.-(a*b).| >= -(a*b) by ABSVALUE:4; then
|.(a*b).| >= -(a*b) by COMPLEX1:52; then
a|^2 + b|^2 > -a*b by A5,XXREAL_0:2; then
a|^2 + b|^2 + a*b > -a*b + a*b by XREAL_1:6; then
reconsider u = |.a|^2 + a*b + b|^2.| as non zero Nat;
p |-count (a|^3 - b|^3) = p|-count |.(a|^2 + b|^2 + a*b)*(a-b).| by N3
.= p |-count (t*u) by COMPLEX1:65
.= (p |-count t)+ (p|-count u) by NAT_3:28;
hence thesis;
end;
theorem GL:
for a,b be non zero Nat holds
a/(a gcd b) = (a lcm b)/b
proof
let a,b be non zero Nat;
a/(a gcd b) = (a*b)/(b*(a gcd b)) by XCMPLX_1:91
.= ((a gcd b)*(a lcm b))/(b*(a gcd b)) by NAT_D:29
.= (a lcm b)/b by XCMPLX_1:91;
hence thesis;
end;
theorem LCM2:
for b be non zero Nat holds
a lcm (a*n + b) = (a*n/b + 1)*(a lcm b)
proof
let b be non zero Nat;
per cases;
suppose a is zero;
hence thesis;
end;
suppose
a is non zero; then
reconsider a,b as non zero Nat;
B2: a*(a*n+b) = (a lcm (a*n+b))*(a gcd (a*n+b)) by NAT_D:29
.= (a lcm (a*n+b))*(a gcd b) by NEWTON02:5;
a*a*n + a*b = (a gcd b)*((a*a*n)/(a gcd b)+ (a*b)/(a gcd b))
by XCMPLX_1:114; then
(a lcm (a*n+b)) = ((a*a*n)/(a gcd b)+ (a*b)/(a gcd b)) by B2,XCMPLX_1:5
.= (a*n)*a/(a gcd b) + (a lcm b)*(a gcd b)/(a gcd b) by NAT_D:29
.= (a*n)*a/(a gcd b) + (a lcm b) by XCMPLX_1:89
.= (a*n)*(a/(a gcd b)) + (a lcm b) by XCMPLX_1:74
.= (a*n)*((a lcm b)/b) + (a lcm b) by GL
.= (a*n)/b*(a lcm b) + 1*(a lcm b) by XCMPLX_1:75;
hence thesis;
end;
end;
theorem
for b be non zero Nat holds a lcm ((n*a+1)*b) = (n*a+1)*(a lcm b)
proof
let b be non zero Nat;
a lcm (a*(n*b) + b) = ((a*n)*b/b+1)*(a lcm b) by LCM2;
hence thesis by XCMPLX_1:89;
end;
theorem
for a be non trivial Nat, n,b be non zero Nat holds
a |-count b >= n*(a|^n |-count b)
proof
let a be non trivial Nat, n,b be non zero Nat;
A1: a <> 1 & b <> 0 by Def0;
reconsider k = a|^n as non trivial Nat;
k <> 1 & b <> 0 by Def0; then
k|^(k |-count b) divides b & not k|^((k |-count b)+1) divides b
by NAT_3:def 7; then
a|^(n*(a|^n |-count b)) divides b by NEWTON:9;
hence thesis by A1,NAT330;
end;
theorem NEWTON0258:
for a,b be odd Integer holds
4 divides a-b iff not 4 divides a+b
proof
let a,b be odd Integer;
reconsider t = |.a.| as odd Nat;
reconsider u = |.b.| as odd Nat;
A0: 4 divides t - u iff not 4 divides t + u by NEWTON02:58;
4 divides u - t iff not 4 divides (u + t) by NEWTON02:58; then
A0a: 4 divides u - t iff not 4 divides -(u + t) by INT_2:10;
per cases by ABSVALUE:1;
suppose
A1: |.a.| = a;
then reconsider a as Nat;
per cases by ABSVALUE:1;
suppose
|.b.| = b;
hence thesis by NEWTON02:58,A1;
end;
suppose
|.b.| = -b;
hence thesis by A0,A1;
end;
end;
suppose
A1: |.a.| = -a;
per cases by ABSVALUE:1;
suppose |.b.| = b;
hence thesis by A0a,A1;
end;
suppose
|.b.| = -b;
hence thesis by A0a,A1;
end;
end;
end;
theorem
for a,b be odd Integer holds 2 |-count (a|^2 + b|^2) = 1
proof
let a,b be odd Integer;
reconsider t = a|^2, u = b|^2 as odd Nat;
A2: 2*2 = 2|^2 by NEWTON:81;
2 divides a - b & 2 divides a + b by ABIAN:def 1; then
2*2 divides (a-b)*(a+b) by NAT31; then
4 divides (a|^2 - b|^2) by NEWTON01:1; then
2|^1 divides (a|^2 + b|^2) & not 2|^(1+1) divides (a|^2 + b|^2)
by ABIAN:def 1,A2,NEWTON0258;
hence thesis by NAT_3:def 7;
end;
theorem
for p be prime Nat, a,b be Nat st a <> b holds
p |-count (a + b) >= p |-count (a gcd b)
proof
let p be prime Nat, a,b be Nat such that
A1: a <> b;
A1a: a <> 0 or b <> 0 by A1; then
consider k,l be Integer such that
A2: a = (a gcd b)*k & b = (a gcd b)*l & k,l are_coprime by INT_2:23;
k >= 0 & l >= 0 by A1a,A2; then
k in NAT & l in NAT by INT_1:3; then
reconsider k,l as Nat;
A4: k is non zero or l is non zero by A2;
p |-count (a+b) = p |-count ((k+l)*(a gcd b)) by A2
.= (p |-count (k+l)) + (p|-count (a gcd b)) by A1a,A4,NAT_3:28;
hence thesis by NAT_1:12;
end;
:: p |-count (a + b)
theorem DX:
for a be non zero Integer, b be non trivial Nat, c be Integer holds
a = b|^(b |-count a)*c implies not b divides c
proof
let a be non zero Integer, b be non trivial Nat, c be Integer;
A0: b > 1 by Def0;
assume
A1: a = b|^(b |-count a)*c;
assume not thesis; then
consider d be Integer such that
A2: c = b*d;
a = b|^(b|-count a)*b*d by A1,A2; then
b*b|^(b |-count a) divides a; then
b|^((b |-count a)+1) divides a by NEWTON:6;
hence contradiction by Def6,A0;
end;
registration
let a be non zero Integer, b be non trivial Nat;
cluster a/(b|^(b |-count a)) -> integer;
coherence
proof
b > 1 by Def0; then
b|^(b |-count a) divides a by Def6; then
consider c be Integer such that
A1: a = b|^(b |-count a)*c;
thus thesis by A1,XCMPLX_1:89;
end;
end;
registration
let a be non zero Integer;
cluster a/(2|^(2 |-count a)) -> integer;
coherence
proof
2 is non trivial Nat by Def0;
hence thesis;
end;
cluster a/(2|^(2 |-count a)) -> odd;
coherence
proof
A1: 2 is non trivial Nat by Def0;
a = 2|^(2 |-count a)*(a/(2|^(2 |-count a))) by XCMPLX_1:87;
hence thesis by A1,DX;
end;
end;
theorem NAT327:
for a be non zero Integer, b be non trivial Nat holds
b |-count a = 0 iff not b divides a
proof
let a be non zero Integer, b be non trivial Nat;
reconsider c = |.a.| as non zero Nat;
b > 1 by Def0; then
not b divides |.a.| iff b |-count |.a.| = 0 by NAT_3:27;
hence thesis by INT_2:16;
end;
registration
let a be odd Integer;
cluster 2 |-count a -> zero;
coherence
proof
2 is non trivial & a <> 0 & not 2 divides a;
hence thesis by NAT327;
end;
reduce a/(2|^(2 |-count a)) to a;
reducibility
proof
1*2|^(2 |-count a) = 1;
hence thesis;
end;
end;
theorem NAT332:
for a be prime Nat, b be non zero Integer, c be Nat holds
a |-count (b|^c) = c*(a |-count b)
proof
let a be prime Nat, b be non zero Integer, c be Nat;
a |-count (b|^c) = a |-count (|.b.||^c) by TAYLOR_2:1
.= c*(a|-count |.b.|) by NAT_3:32;
hence thesis;
end;
theorem
for a,b be non zero Nat, n be odd Nat holds
(a|^(n+2)+b|^(n+2))/(a+b) = a|^(n+1)+ b|^(n+1) - a*b*((a|^n+b|^n)/(a+b))
proof
let a,b be non zero Nat, n be odd Nat;
reconsider m = (n-1)/2 as Nat;
a|^((2*m+1)+2) + b|^((2*m+1)+2) =
(a+b)*(a|^((2*m+1)+1) + b|^((2*m+1)+1)) - a*b*(a|^(2*m+1)+ b|^(2*m+1))
by RI3; then
(a|^((2*m+1)+2) + b|^((2*m+1)+2))/(a+b) =
(a+b)*(a|^((2*m+1)+1) + b|^((2*m+1)+1))/(a+b) -
(a*b*(a|^(2*m+1)+ b|^(2*m+1)))/(a+b) by XCMPLX_1:120
.= (a|^((2*m+1)+1) + b|^((2*m+1)+1)) -
((a*b)*(a|^(2*m+1)+ b|^(2*m+1)))/(a+b) by XCMPLX_1:89
.= (a|^((2*m+1)+1) + b|^((2*m+1)+1)) -
(a*b)*((a|^(2*m+1)+ b|^(2*m+1))/(a+b)) by XCMPLX_1:74;
hence thesis;
end;
theorem Odd:
for a,b be odd Integer, n be Nat holds
2 |-count (a|^(2*n+1) - b|^(2*n+1)) = 2 |-count (a-b)
proof
let a,b be odd Integer, n be Nat;
per cases;
suppose a = b;
hence thesis;
end;
suppose
A0: a <> b; then
reconsider c = a - b as non zero Integer;
defpred P[Nat] means
2 |-count (a|^(2*$1+1) - b|^(2*$1+1)) = 2 |-count (a-b);
A1: P[0];
A2: P[k] implies P[k+1]
proof
assume
B0: P[k];
reconsider d = a|^(2*k+1) - b|^(2*k+1) as non zero Integer by A0,POW2;
B1: 2|^(2 |-count c) divides c &
2|^(2 |-count d) divides d by Def6;
reconsider x = d/2|^(2|-count d) as odd Integer;
consider y be Integer such that
B3: c = 2|^(2|-count c)*y by B1;
B5: a|^((2*k+1)+2) - b|^((2*k+1)+2) =
a|^(2*k+1)*(a|^2 - b|^2) + b|^2*(a|^(2*k+1) - b|^(2*k+1)) by RI2
.= a|^(2*k+1)*(a|^2 - b|^2) + b|^2* (2|^(2 |-count (a-b))*x)
by B0,XCMPLX_1:87
.= a|^(2*k+1)*((a+b)*(2|^(2 |-count (a-b))*y)) +
b|^2* 2|^(2 |-count (a-b))*x by B3,NEWTON01:1
.= (a|^(2*k+1)*(a+b)*y + b|^2*x)* 2|^(2 |-count (a-b));
B6: 2 is non trivial;
2 |-count (a|^((2*k+1)+2) - b|^((2*k+1)+2))
= 2 |-count (a|^(2*k+1)*(a+b)*y + b|^2*x) +
2 |-count (2|^(2 |-count (a-b))) by B5,NAT328,INT_2:28
.= 2 |-count c by B6;
hence thesis;
end;
for x holds P[x] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem
for a,b be odd Integer, m be odd Nat holds
2 |-count (a|^m + b|^m) = 2 |-count (a+b)
proof
let a,b be odd Integer, m be odd Nat;
reconsider c = -b as odd Integer;
reconsider n = (m-1)/2 as Nat;
2 |-count (a|^m + (-c)|^m) =
2 |-count (a|^(2*n+1) +(-c|^(2*n+1))) by POWER:2
.= 2 |-count (a|^(2*n+1) - c|^(2*n+1))
.= 2 |-count (a -(-b)) by Odd;
hence thesis;
end;
:: a <> b would not be necessary if 2 |-count 0 is defined
theorem
for a,b be odd Nat st a <> b holds
1 = min (2 |-count (a-b), 2|-count (a+b))
proof
let a,b be odd Nat such that
A0: a <> b;
reconsider k = |.a-b.| as even Nat;
reconsider l = a+b as even Nat;
A1: 2|^2 = 2*2 by NEWTON:81;
A2: 2|^1 divides |.a-b.| & 2|^1 divides (a+b) by ABIAN:def 1;
A3: a - b <> b - b by A0; then
A4: 2 |-count |.a-b.| <> 0 & 2 |-count (a+b) <> 0 by A2,NAT_3:27;
per cases;
suppose
not 4 divides (a - b); then
not |.2|^(1+1).| divides |.a-b.| by A1,INT_2:16; then
1 = 2 |-count |.a-b.| by A2,A3,NAT_3:def 7;
hence thesis by A4,NAT_1:14,XXREAL_0:def 9;
end;
suppose 4 divides (a-b); then
not 2|^(1+1) divides (a+b) by A1,NEWTON02:58; then
2 |-count (a+b) = 1 by A2,NAT_3:def 7;
hence thesis by A4,NAT_1:14,XXREAL_0:def 9;
end;
end;
theorem DL:
for a be non trivial Nat, b,c be non zero Integer holds
a |-count b > a |-count c implies a|^(a |-count c) divides b &
not a|^(a |-count b) divides c
proof
let a be non trivial Nat, b,c be non zero Integer;
A1: a > 1 by Def0;
reconsider n = a |-count b, m = a |-count c as Nat;
assume
A2: a |-count b > a |-count c; then
n >= m+1 by NAT_1:13; then
consider k such that
A3: n = (m+1)+k by NAT_1:10;
not a|^(m+1) divides c & a|^(m+1) divides a|^(m+1)*a|^k by A1,Def6; then
not a|^(m+1)*a|^k divides c by INT_2:9; then
not a|^n divides c & a|^n divides b & a|^m divides a|^n
by NEWTON:8,A3,A1,Def6,A2,NEWTON:89;
hence thesis by INT_2:9;
end;
theorem
for a be non trivial Nat, b,c be non zero Integer holds
a|^(a |-count b) divides c & a|^(a |-count c) divides b
implies a |-count b = a |-count c
proof
let a be non trivial Nat, b,c be non zero Integer;
assume a|^(a |-count b) divides c & a|^(a |-count c) divides b;
then a |-count b >= a |-count c & a |-count b <= a |-count c by DL;
hence thesis by XXREAL_0:1;
end;
theorem PP:
for a,b be Integer, m,n be Nat holds
a|^n divides b & not a|^m divides b implies m > n
proof
let a,b be Integer, m,n be Nat;
assume a|^n divides b & not a|^m divides b; then
not a|^m divides a|^n by INT_2:9;
hence thesis by NEWTON89;
end;
theorem DN:
for a be non trivial Nat, b,c be non zero Integer holds
a |-count b = a |-count c & a|^n divides b implies a|^n divides c
proof
let a be non trivial Nat, b,c be non zero Integer;
A0: a > 1 by Def0;
assume
A1: a |-count b = a |-count c & a|^n divides b;
not a|^((a|-count b)+1) divides b by A0,Def6; then
((a |-count b)+1) > n by A1,PP; then
a |-count b >= n by NAT_1:13; then
A3: a|^n divides a|^(a |-count b) by NEWTON:89;
a|^(a |-count c) divides c by A0,Def6;
hence thesis by A1,A3, INT_2:9;
end;
theorem DIC:
for a be non trivial Nat, b,c be non zero Integer holds
a |-count b = a |-count c iff
(for n be Nat holds a|^n divides b iff a|^n divides c)
proof
let a be non trivial Nat, b,c be non zero Integer;
A1: a > 1 by Def0;
a |-count b <> a |-count c implies (ex n be Nat st
(a|^n divides b & not a|^n divides c) or
(a|^n divides c & not a|^n divides b))
proof
reconsider n = a |-count b, m = a |-count c as Nat;
assume a|-count b <> a |-count c; then
per cases by XXREAL_0:1;
suppose n > m; then
a|^n divides b & not a|^n divides c by DL,A1,Def6;
hence thesis;
end;
suppose n < m; then
m >= n+1 by NAT_1:13; then
a|^(n+1) divides a|^m & a|^m divides c by NEWTON:89,Def6,A1; then
a|^(n+1) divides c & not a|^(n+1) divides b by INT_2:9,A1,Def6;
hence thesis;
end;
end;
hence thesis by DN;
end;
theorem
for a,b be odd Integer st |.a.| <> |.b.| holds
2 |-count (a-b)|^2 <> 2|-count (a+b)|^2 &
2 |-count (a-b)|^2 <> 2|-count a|^2-b|^2
proof
let a,b be odd Integer such that
A1: |.a.| <> |.b.|;
A1a: a - b <> a - a by A1;
reconsider c = a-b as non zero Integer by A1;
reconsider d = a+b as non zero Integer by A1,ABS1;
A2: 2 |-count (a-b)|^2 = 2 |-count c|^2
.= 2*(2 |-count (a-b)) by NAT332,INT_2:28;
A3: 2 |-count (a+b)|^2 = 2 |-count d|^2
.= 2*(2 |-count (a+b)) by NAT332,INT_2:28;
2*2 = 2|^2 by NEWTON:81; then
A6: not (2|^2 divides (a-b) iff 2|^2 divides (a+b)) by NEWTON0258;
a+b <> 0 & 2 is non trivial by A1,ABS1;
hence thesis by A2,A3,A6,A1a,DIC;
end;
:: MOEBIUS1:6, for non prime numbers
theorem MOB16:
for b be non trivial Nat, a be non zero Integer holds
b |-count a <> 0 iff b divides a
proof
let b be non trivial Nat, a be non zero Integer;
b |-count |.a.| <> 0 iff b divides |.a.|
proof
b <> 1 & a <> 0 by NAT_2:def 1;
hence thesis by NAT_3:27;
end;
hence thesis by INT_2:16;
end;
theorem
for b be non trivial Nat, a be non zero Nat holds
(b |-count a) = 0 iff a mod b <> 0
proof
let b be non trivial Nat, a be non zero Nat;
per cases;
suppose
A1: b |-count a <> 0; then
b divides a by MOB16;
hence thesis by A1;
end;
suppose
A1: b |-count a = 0; then
not b divides a by MOB16;
hence thesis by A1,PEPIN:6;
end;
end;
theorem
for p be prime Nat, a be non trivial Nat holds
a |-count p <= 1
proof
let p be prime Nat, a be non trivial Nat;
a > 1 by Def0; then
a |-count p = 0 or a = p by NAT_3:24;
hence thesis by Def0,NAT_3:22;
end;
theorem Count7:
for a,b be non trivial Nat, c be non zero Nat holds
a|^((a |-count b)*(b |-count c)) <= c
proof
let a,b be non trivial Nat, c be non zero Nat;
A1: a|^((a |-count b)*(b |-count c)) =
(a|^(a |-count b))|^(b |-count c) by NEWTON:9;
A2: (a|^(a |-count b))|^(b |-count c) <=
b|^(b |-count c) by Count0,NEWTON02:41;
b|^(b |-count c) <= c by Count0;
hence thesis by A1,A2,XXREAL_0:2;
end;
theorem
for p be prime Nat, a be non trivial Nat, b be non zero Nat holds
a |-count (p|^b) <= b
proof
let p be prime Nat, a be non trivial Nat, b be non zero Nat;
A1: a > 1 by Def0;
per cases;
suppose p = a;
hence thesis by Def0,NAT_3:25;
end;
suppose
p <> a; then
a |-count p = 0 by A1,NAT_3:24; then
not a|^(0+b) divides p|^b by MOB16,WSIERP_1:26;
hence thesis by Count1;
end;
end;
theorem
for p be prime Nat, a be non trivial Nat holds
(p |-count a)*(a |-count p|^n) <= n
proof
let p be prime Nat, a be non trivial Nat;
A1: p > 1 by NAT_4:14;
p|^((p |-count a)*(a |-count p|^n)) <= p|^n by Count7;
hence thesis by A1,PEPIN:66;
end;
theorem
for a,b be non trivial Nat, c be non zero Nat holds
(a |-count b)*(b|-count c) <= (a |-count c)
proof
let a,b be non trivial Nat, c be non zero Nat;
a <> 1 & b <> 1 by Def0; then
A2: a|^(a |-count b) divides b & b|^(b |-count c) divides c &
a|^(a |-count c) divides c
& not a|^((a |-count c)+1) divides c by NAT_3:def 7; then
(a|^(a |-count b))|^(b |-count c) divides c by LmY; then
a|^((a |-count b)*(b |-count c)) divides c by NEWTON:9; then
((a |-count b)*(b |-count c)) < (a |-count c)+1 by A2,LmX;
hence thesis by NAT_1:13;
end;
theorem
for a be non zero Nat, b be odd Nat holds
2 |-count (a*b) = 2 |-count a
proof
let a be non zero Nat, b be odd Nat;
2 |-count (a*b) = (2 |-count a) + (2 |-count b) by INT_2:28,NAT_3:28
.= (2 |-count a) + 0;
hence thesis;
end;
theorem :: NAT_5:1 extended
for a be non trivial Nat holds
a|^(n+1) + a|^n < a|^(n+2)
proof
let a be non trivial Nat;
A0: not (a = 0 or a = 1) by NAT_2:def 1; then
A0a: a >= 2 by NAT_1:23;
A1: a|^(n+1+1) = a*a|^(n+1) by NEWTON:6;
A2: a*a|^(n+1) >= 2*a|^(n+1) by A0,NAT_1:23,XREAL_1:64;
a > 1 by A0a,XXREAL_0:2; then
a*a|^n > 1*a|^n by XREAL_1:68; then
a|^(n+1) > a|^n by NEWTON:6; then
a|^(n+1) + a|^(n+1) > a|^(n+1) + a|^n by XREAL_1:6;
hence thesis by A1,A2,XXREAL_0:2;
end;
theorem LmNT:
for a be non trivial Nat holds
(a+1)|^n + (a+1)|^n < (a+1)|^(n+1)
proof
let a be non trivial Nat;
a <> 0 & a <> 1 by NAT_2:def 1; then
a+1 > 2 by NAT_1:13,23; then
(a+1)*(a+1)|^n > 2*(a+1)|^n by XREAL_1:68;
hence thesis by NEWTON:6;
end;
theorem
for a be non trivial odd Nat holds
a|^n + a|^n < a|^(n+1)
proof
let a be non trivial odd Nat;
a - 1 <> 1 & a - 1 <> 0; then
reconsider b = a-1 as non trivial Nat by NAT_2:def 1;
(b+1)|^n + (b+1)|^n < (b+1)|^(n+1) by LmNT;
hence thesis;
end;
theorem ::: (p|^a)|^c = p|^b implies a divides b contraposed
for p be non trivial Nat holds
not a divides b implies (p|^a)|^c <> p|^b
proof
let p be non trivial Nat;
assume
A1: not a divides b;
A2: p|^(a*c) = p|^b iff (p|^a)|^c = p|^b by NEWTON:9;
p > 1 by Def0;
hence thesis by A1,A2,PEPIN:30;
end;
LmC10: for a be Integer, b be non zero Integer, n be non zero Nat holds
a = b|^n implies (for p be prime Nat holds n divides p |-count a)
proof
let a be Integer, b be non zero Integer, n be non zero Nat;
assume
A1: a = b|^n;
for p be prime Nat holds n divides p |-count a
proof
let p be prime Nat;
p |-count b|^n = n*(p|-count b) by NAT332;
hence thesis by A1;
end;
hence thesis;
end;
theorem
for a,b be non zero Integer, n be non zero Nat holds
(ex p be prime Nat st not n divides p|-count a) implies a <> b|^n by LmC10;
theorem
for a,b be non zero Integer, n be non zero Nat holds
a = b|^n implies (for p be prime Nat holds n divides p |-count a) by LmC10;
theorem
for a,b be positive Real, n be non trivial Nat holds
(a+b)|^n > a|^n + b|^n
proof
let a,b be positive Real, n be non trivial Nat;
reconsider m = n-1 as non zero Nat;
reconsider c = max(a,b), d = min(a,b) as positive Real;
A1: c*c|^m = c|^(m+1) & d*d|^m = d|^(m+1) &
(c+d)*(c+d)|^m = (c+d)|^(m+1) by NEWTON:6;
A2: c|^n = max(a|^n, b|^n) & d|^n = min(a|^n,b|^n) by MM1;
c+d > c+0 & c+d > 0+d by XREAL_1:6; then
(c+d)|^m > c|^m & (c+d)|^m > d|^m by NEWTON02:40; then
c*(c+d)|^m > c*c|^m & d*(c+d)|^m > d*d|^m by XREAL_1:68; then
c*(c+d)|^m > c|^(m+1) & d*(c+d)|^m > d|^(m+1) by NEWTON:6; then
A3: c*(c+d)|^m + d*(c+d)|^m > c|^(m+1)+ d|^(m+1) by XREAL_1:8;
(a+b)|^(m+1) = c*(c+d)|^m + d*(c+d)|^m by A1,MinMax;
hence thesis by A2,A3,MinMax;
end;
theorem
for a,b be non zero Integer, p be odd prime Nat st
|.a.| <> |.b.| & not p divides b holds
p |-count (a|^2 - b|^2) = max (p |-count (a-b), p |-count (a+b))
proof
let a,b be non zero Integer, p be odd prime Nat such that
A1: |.a.| <> |.b.| & not p divides b;
A2: p is non trivial & a-b <> 0 & a+b <> 0 by A1,ABS1;
p divides (a-b) implies not p divides (a+b) by A1,SUD; then
A3: p |-count (a-b) <> 0 implies p |-count (a+b) = 0 by A2,NAT327;
p |-count (a|^2 - b|^2) = p |-count ((a-b)*(a+b)) by NEWTON01:1
.= (p |-count (a-b)) + (p |-count (a+b)) by A2,NAT328;
hence thesis by A3,XXREAL_0:def 10;
end;
theorem
for a be non trivial Nat, b be non zero Integer holds
a |-count (a|^n*b) = n + a|-count b
proof
let a be non trivial Nat, b be non zero Integer;
A0: a|^n*a|^(a |-count b) = a|^((a |-count b)+n) &
a|^n*a|^((a|-count b)+1) = a|^(((a |-count b)+1)+n) by NEWTON:8;
A1: a <> 1 by Def0; then
a|^(a |-count b) divides b &
not a|^((a|-count b)+1) divides b by Def6; then
a|^((a |-count b)+n) divides (a|^n*b) &
not a|^(((a |-count b)+n)+1) divides (a|^n*b) by INT_4:7,A0;
hence thesis by A1,Def6;
end;