:: Prime Factorization of Sums and Differences of Two Like Powers
:: by Rafa{\l} Ziobro
::
:: Received June 30, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users


theorem :: NEWTON03:1
for k, n being Nat
for a1, b1 being Complex holds (a1 |^ (n + k)) + (b1 |^ (n + k)) = ((a1 |^ n) * ((a1 |^ k) + (b1 |^ k))) + ((b1 |^ k) * ((b1 |^ n) - (a1 |^ n)))
proof end;

theorem RI2: :: NEWTON03:2
for k, n being Nat
for a1, b1 being Complex holds (a1 |^ (n + k)) - (b1 |^ (n + k)) = ((a1 |^ n) * ((a1 |^ k) - (b1 |^ k))) + ((b1 |^ k) * ((a1 |^ n) - (b1 |^ n)))
proof end;

theorem RI3: :: NEWTON03:3
for m being Nat
for a1, b1 being Complex holds (a1 |^ (m + 2)) + (b1 |^ (m + 2)) = ((a1 + b1) * ((a1 |^ (m + 1)) + (b1 |^ (m + 1)))) - ((a1 * b1) * ((a1 |^ m) + (b1 |^ m)))
proof end;

definition
let a be Nat;
redefine attr a is trivial means :Def0: :: NEWTON03:def 1
a <= 1;
compatibility
( a is trivial iff a <= 1 )
proof end;
end;

:: deftheorem Def0 defines trivial NEWTON03:def 1 :
for a being Nat holds
( a is trivial iff a <= 1 );

definition
let a be Complex;
:: original: ^2
redefine func a ^2 -> set equals :: NEWTON03:def 2
a |^ 2;
correctness
coherence
a ^2 is set ;
compatibility
for b1 being set holds
( b1 = a ^2 iff b1 = a |^ 2 );
by NEWTON:81;
end;

:: deftheorem defines ^2 NEWTON03:def 2 :
for a being Complex holds a ^2 = a |^ 2;

definition
let a, b be Integer;
:: original: gcd
redefine func a gcd b -> Nat equals :: NEWTON03:def 3
|.a.| gcd |.b.|;
correctness
coherence
a gcd b is Nat;
compatibility
for b1 being Nat holds
( b1 = a gcd b iff b1 = |.a.| gcd |.b.| );
by INT_2:34;
:: original: lcm
redefine func a lcm b -> Nat equals :Def2: :: NEWTON03:def 4
|.a.| lcm |.b.|;
correctness
coherence
a lcm b is Nat;
compatibility
for b1 being Nat holds
( b1 = a lcm b iff b1 = |.a.| lcm |.b.| );
by INT_2:33;
end;

:: deftheorem defines gcd NEWTON03:def 3 :
for a, b being Integer holds a gcd b = |.a.| gcd |.b.|;

:: deftheorem Def2 defines lcm NEWTON03:def 4 :
for a, b being Integer holds a lcm b = |.a.| lcm |.b.|;

registration
let a, b be positive Real;
cluster max (a,b) -> positive ;
coherence
max (a,b) is positive by XXREAL_0:def 10;
cluster min (a,b) -> positive ;
coherence
min (a,b) is positive by XXREAL_0:def 9;
end;

registration
let a be non zero Integer;
let b be Integer;
cluster a gcd b -> non zero ;
coherence
not a gcd b is zero by INT_2:5;
end;

registration
let a be non zero Complex;
let n be Nat;
cluster a |^ n -> non zero ;
coherence
not a |^ n is zero by PREPOWER:5;
end;

registration
let a be non trivial Nat;
let n be non zero Nat;
cluster a |^ n -> non trivial ;
coherence
not a |^ n is trivial
proof end;
end;

registration
let a be Integer;
cluster K200(a) -> natural ;
coherence
|.a.| is natural ;
end;

registration
let a be even Integer;
cluster K200(a) -> even ;
coherence
not |.a.| is odd
proof end;
end;

registration
let a be Nat;
reduce a lcm a to a;
reducibility
a lcm a = a by NAT_D:31;
reduce a gcd a to a;
reducibility
a gcd a = a by NAT_D:32;
end;

registration
let a be non zero Integer;
let b be Integer;
cluster a gcd b -> positive ;
coherence
a gcd b is positive ;
end;

registration
let a, b be Integer;
reduce a gcd (a gcd b) to a gcd b;
correctness
reducibility
a gcd (a gcd b) = a gcd b;
proof end;
reduce a lcm (a lcm b) to a lcm b;
correctness
reducibility
a lcm (a lcm b) = a lcm b;
proof end;
end;

registration
let a be Integer;
reduce a gcd 1 to 1;
reducibility
a gcd 1 = 1
proof end;
reduce (a + 1) gcd a to 1;
reducibility
(a + 1) gcd a = 1
proof end;
end;

theorem NEWTON027: :: NEWTON03:4
for n being Nat
for t, z being Integer holds (t |^ n) gcd (z |^ n) = (t gcd z) |^ n
proof end;

registration
let a be Integer;
let n be Nat;
reduce ((a + 1) |^ n) gcd (a |^ n) to 1;
reducibility
((a + 1) |^ n) gcd (a |^ n) = 1
proof end;
end;

registration
let a1, b1 be Complex;
reduce (a1 |^ 0) - (b1 |^ 0) to 0 ;
reducibility
(a1 |^ 0) - (b1 |^ 0) = 0
proof end;
end;

registration
let a be non negative Real;
let n be Nat;
cluster a |^ n -> non negative ;
coherence
not a |^ n is negative
proof end;
end;

registration
cluster V1() non trivial epsilon-transitive epsilon-connected ordinal natural non zero V31() integer dim-like odd complex ext-real positive non negative for set ;
existence
not for b1 being odd Nat holds b1 is trivial
proof end;
cluster non trivial epsilon-transitive epsilon-connected ordinal natural V31() integer dim-like even complex ext-real non negative for set ;
existence
not for b1 being even Nat holds b1 is trivial
proof end;
end;

registration
let a be positive Real;
let n be Nat;
cluster a |^ n -> positive ;
coherence
a |^ n is positive ;
end;

registration
let a be Integer;
cluster a * a -> square ;
coherence
a * a is square
proof end;
cluster a / a -> square ;
coherence
a / a is square
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural V31() integer dim-like complex ext-real non negative non square for Element of NAT ;
existence
not for b1 being Element of NAT holds b1 is square
proof end;
end;

registration
cluster prime -> non square for Element of NAT ;
coherence
for b1 being Element of NAT st b1 is prime holds
not b1 is square ;
end;

registration
cluster V1() non trivial epsilon-transitive epsilon-connected ordinal natural non zero V31() integer dim-like even complex ext-real positive non negative prime for set ;
correctness
existence
ex b1 being prime Nat st b1 is even ;
proof end;
cluster V1() non trivial epsilon-transitive epsilon-connected ordinal natural non zero V31() integer dim-like odd complex ext-real positive non negative prime for set ;
correctness
existence
ex b1 being prime Nat st b1 is odd ;
proof end;
end;

registration
cluster integer prime -> non square for object ;
coherence
for b1 being Integer st b1 is prime holds
not b1 is square
proof end;
end;

registration
let a be square Element of NAT ;
cluster sqrt a -> natural ;
coherence
sqrt a is natural
proof end;
end;

registration
let a be Integer;
cluster a |^ 2 -> square ;
coherence
a |^ 2 is square
proof end;
cluster a * a -> square ;
coherence
a * a is square ;
end;

registration
cluster V31() integer complex ext-real non square for object ;
existence
not for b1 being Integer holds b1 is square by INT_2:28;
end;

registration
cluster natural zero -> trivial for set ;
correctness
coherence
for b1 being Nat st b1 is zero holds
b1 is trivial ;
;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural V31() integer dim-like complex ext-real non negative square for set ;
existence
ex b1 being Nat st b1 is square
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural non zero V31() integer dim-like complex ext-real non negative for Element of NAT ;
existence
not for b1 being Element of NAT holds b1 is zero by INT_2:28;
cluster non trivial epsilon-transitive epsilon-connected ordinal natural V31() integer dim-like complex ext-real non negative square for Element of NAT ;
existence
not for b1 being square Element of NAT holds b1 is trivial
proof end;
end;

registration
cluster trivial natural -> square for set ;
coherence
for b1 being Nat st b1 is trivial holds
b1 is square
proof end;
end;

registration
cluster integer non square -> non zero for object ;
coherence
for b1 being Integer st not b1 is square holds
not b1 is zero ;
end;

theorem NAT31: :: NEWTON03:5
for a, b, c, d being Integer st a divides b & c divides d holds
a * c divides b * d
proof end;

theorem LCM1: :: NEWTON03:6
for a, b being Integer holds
( a divides b iff a lcm b = |.b.| )
proof end;

registration
let a be Integer;
reduce a lcm 0 to 0 ;
reducibility
a lcm 0 = 0 by INT_2:4;
end;

registration
let a be Nat;
reduce a lcm 1 to a;
reducibility
a lcm 1 = a by NEWTON:46;
end;

registration
let a, b be Nat;
reduce (a * b) lcm a to a * b;
reducibility
(a * b) lcm a = a * b
proof end;
reduce (a gcd b) lcm b to b;
reducibility
(a gcd b) lcm b = b by NEWTON:53;
reduce a gcd (a lcm b) to a;
reducibility
a gcd (a lcm b) = a by NEWTON:54;
end;

theorem NATD29: :: NEWTON03:7
for a, b being Integer holds |.(a * b).| = (a gcd b) * (a lcm b)
proof end;

theorem LmLCM: :: NEWTON03:8
for n being Nat
for a, b being Integer holds (a |^ n) lcm (b |^ n) = (a lcm b) |^ n
proof end;

registration
let a, b be square Element of NAT ;
cluster a gcd b -> square ;
coherence
a gcd b is square
proof end;
cluster a lcm b -> square ;
coherence
a lcm b is square
proof end;
end;

registration
let a, b be square Integer;
cluster a gcd b -> square ;
coherence
a gcd b is square
proof end;
cluster a lcm b -> square ;
coherence
a lcm b is square
proof end;
end;

theorem ODD: :: NEWTON03:9
for t being Integer holds
( t is odd iff t gcd 2 = 1 )
proof end;

definition
let t be Integer;
redefine attr t is even means :Def3: :: NEWTON03:def 5
 not t gcd 2 = 1;
compatibility
( not t is odd iff not t gcd 2 = 1 ) by ODD;
end;

:: deftheorem Def3 defines odd NEWTON03:def 5 :
for t being Integer holds
( not t is odd iff not t gcd 2 = 1 );

registration
let a be odd Integer;
cluster K200(a) -> odd ;
coherence
|.a.| is odd
proof end;
cluster - a -> odd ;
coherence
- a is odd
proof end;
end;

registration
let a, b be even Integer;
cluster a gcd b -> even ;
coherence
not a gcd b is odd by NEWTON02:9;
end;

registration
let a be Integer;
let b be odd Integer;
cluster a gcd b -> odd ;
coherence
a gcd b is odd by NEWTON02:9;
end;

registration
let a be Nat;
reduce |.(- a).| to a;
reducibility
|.(- a).| = a
proof end;
end;

registration
let t, z be even Integer;
cluster t + z -> even ;
correctness
coherence
not t + z is odd ;
;
cluster t - z -> even ;
correctness
coherence
not t - z is odd ;
;
cluster t * z -> even ;
correctness
coherence
not t * z is odd ;
;
end;

registration
let t, z be odd Integer;
cluster t + z -> even ;
coherence
not t + z is odd ;
cluster t - z -> even ;
coherence
not t - z is odd ;
cluster t * z -> odd ;
coherence
t * z is odd ;
end;

registration
let t be odd Integer;
let z be even Integer;
cluster t + z -> odd ;
coherence
t + z is odd ;
cluster t - z -> odd ;
coherence
t - z is odd ;
cluster t * z -> even ;
coherence
not t * z is odd ;
end;

theorem PT1: :: NEWTON03:10
for a being non zero square Integer
for b being Integer st a * b is square holds
b is square
proof end;

registration
let a be square Element of NAT ;
let n be Nat;
cluster a |^ n -> square ;
coherence
a |^ n is square
proof end;
end;

registration
let a be square Integer;
let n be Nat;
cluster a |^ n -> square ;
coherence
a |^ n is square
proof end;
end;

registration
let a be non zero square Integer;
let b be non square Integer;
cluster a * b -> non square ;
coherence
not a * b is square by PT1;
end;

registration
let a be Element of NAT ;
let b be even Nat;
cluster a |^ b -> square ;
coherence
a |^ b is square
proof end;
end;

registration
let a be non square Element of NAT ;
let b be odd Nat;
cluster a |^ b -> non square ;
coherence
not a |^ b is square
proof end;
end;

LmNAT: for a, n being Nat
for x being non negative Real st a |^ n < x |^ n & x |^ n < (a + 1) |^ n holds
not x is Nat
proof end;

registration
let a be non zero square Integer;
cluster a + 1 -> non square ;
coherence
not a + 1 is square
proof end;
end;

registration
let a be non zero square Element of NAT ;
cluster a + 1 -> non square ;
coherence
not a + 1 is square ;
end;

registration
let a be non zero square object ;
let b be non square Element of NAT ;
cluster a * b -> non square ;
coherence
not a * b is square ;
end;

registration
let a be non zero square Integer;
let n, m be Nat;
cluster (a |^ n) + (a |^ m) -> non square ;
coherence
not (a |^ n) + (a |^ m) is square
proof end;
end;

registration
let a be non zero square Element of NAT ;
let n, m be Nat;
cluster (a |^ n) + (a |^ m) -> non square ;
coherence
not (a |^ n) + (a |^ m) is square ;
end;

registration
let a be non zero square Integer;
let p be prime Nat;
cluster p * a -> non square ;
coherence
not p * a is square ;
end;

registration
let a be non trivial Element of NAT ;
cluster a - 1 -> non zero ;
coherence
not a - 1 is zero ;
end;

registration
let q be square Integer;
cluster K200(q) -> square ;
coherence
|.q.| is square ;
end;

registration
let x be non zero Integer;
cluster K200(x) -> non zero ;
coherence
not |.x.| is zero by COMPLEX1:47;
end;

registration
let a be non trivial square Element of NAT ;
cluster a - 1 -> non square ;
coherence
not a - 1 is square
proof end;
end;

LmN30: for a, b being non square Element of NAT st a,b are_coprime holds
not a * b is square
proof end;

COMPLEX175: for a being Integer holds |.a.| |^ 2 = a |^ 2
proof end;

registration
let a be non trivial Element of NAT ;
cluster a * (a - 1) -> non square ;
coherence
not a * (a - 1) is square
proof end;
end;

registration
let a, b be Integer;
let n, m be Nat;
cluster (((a |^ n) + (b |^ n)) * ((a |^ m) - (b |^ m))) + (((a |^ m) + (b |^ m)) * ((a |^ n) - (b |^ n))) -> even ;
coherence
not (((a |^ n) + (b |^ n)) * ((a |^ m) - (b |^ m))) + (((a |^ m) + (b |^ m)) * ((a |^ n) - (b |^ n))) is odd
proof end;
cluster (((a |^ n) + (b |^ n)) * ((a |^ m) + (b |^ m))) + (((a |^ m) - (b |^ m)) * ((a |^ n) - (b |^ n))) -> even ;
coherence
not (((a |^ n) + (b |^ n)) * ((a |^ m) + (b |^ m))) + (((a |^ m) - (b |^ m)) * ((a |^ n) - (b |^ n))) is odd
proof end;
end;

registration
let a be even Integer;
cluster a / 2 -> integer ;
coherence
a / 2 is integer
proof end;
end;

registration
let a, b be non zero Nat;
cluster a + b -> non trivial ;
coherence
not a + b is trivial
proof end;
end;

registration
let b be non zero Nat;
let a, c be non trivial Nat;
reduce c |-count (c |^ (a |-count b)) to a |-count b;
reducibility
c |-count (c |^ (a |-count b)) = a |-count b by Def0, NAT_3:25;
end;

registration
let a, b be non zero Integer;
cluster a / (a gcd b) -> integer ;
coherence
a / (a gcd b) is integer
proof end;
cluster (a lcm b) / b -> integer ;
coherence
(a lcm b) / b is integer
proof end;
cluster (a lcm b) / (a gcd b) -> integer ;
coherence
(a lcm b) / (a gcd b) is integer
proof end;
end;

registration
let a be even Integer;
reduce a gcd 2 to 2;
reducibility
a gcd 2 = 2
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural non zero V31() integer dim-like even complex ext-real non negative for set ;
existence
not for b1 being even Nat holds b1 is zero
proof end;
end;

registration
let a be even Integer;
let n be non zero Nat;
cluster a * n -> even ;
coherence
not a * n is odd ;
cluster a |^ n -> even ;
coherence
not a |^ n is odd ;
end;

registration
let a be Integer;
let n be zero Nat;
cluster a * n -> even ;
coherence
not a * n is odd ;
cluster a |^ n -> odd ;
coherence
a |^ n is odd
proof end;
end;

registration
let a be Element of NAT ;
reduce |.a.| to a;
reducibility
|.a.| = a ;
end;

registration
let a be non negative Real;
let n be non zero Nat;
reduce n -root (a |^ n) to a;
reducibility
n -root (a |^ n) = a
proof end;
reduce (n -root a) |^ n to a;
reducibility
(n -root a) |^ n = a
proof end;
end;

:: solvable by ATP, yet not by verifier
theorem INT29: :: NEWTON03:11
for a, b, c being Nat st not a divides b holds
not a * c divides b
proof end;

:: Roots
:: see PEPIN:30;
theorem POW1: :: NEWTON03:12
for a, b being non negative Real
for n being positive Nat holds
( a |^ n = b |^ n iff a = b )
proof end;

registration
let a be Real;
let n be even Nat;
cluster a |^ n -> non negative ;
coherence
not a |^ n is negative
proof end;
end;

registration
let a be negative Real;
let n be odd Nat;
cluster a |^ n -> negative ;
coherence
a |^ n is negative
proof end;
end;

theorem POW2: :: NEWTON03:13
for a, b being Real
for n being odd Nat holds
( a |^ n = b |^ n iff a = b )
proof end;

theorem :: NEWTON03:14
for c, a, b being Nat st a,b are_coprime holds
for n being 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 end;

:: DIVISION
theorem POWD: :: NEWTON03:15
for n being non zero Nat
for a, b being Integer holds
( b |^ n divides a |^ n iff b divides a )
proof end;

theorem NEWTON89: :: NEWTON03:16
for a being Integer
for m, n being Nat st m >= n holds
a |^ n divides a |^ m
proof end;

LmX: for m, n being Nat
for a, b being Integer st a |^ m divides b & not a |^ n divides b holds
n > m
proof end;

theorem LmY: :: NEWTON03:17
for c, m being Nat
for a, b being Integer st a divides b & b |^ m divides c holds
a |^ m divides c
proof end;

theorem :: NEWTON03:18
for k, n being Nat
for a, p being Integer st p |^ ((2 * n) + k) divides a |^ 2 holds
p |^ n divides a
proof end;

theorem :: NEWTON03:19
for a, b being odd square Element of NAT holds 8 divides a - b
proof end;

theorem :: NEWTON03:20
for n being Nat
for a, b being odd Nat st 4 divides a - b holds
not 4 divides (a |^ n) + (b |^ n)
proof end;

theorem :: NEWTON03:21
for n being Nat
for a, b being odd Nat st 4 divides (a |^ n) + (b |^ n) holds
not 4 divides (a |^ (2 * n)) + (b |^ (2 * n))
proof end;

theorem :: NEWTON03:22
for n being Nat
for a, b being odd Nat st 4 divides (a |^ n) - (b |^ n) holds
not 4 divides (a |^ (2 * n)) + (b |^ (2 * n))
proof end;

theorem Even: :: NEWTON03:23
for m, n being Nat
for a, b being odd Nat st 2 |^ m divides (a |^ n) - (b |^ n) holds
2 |^ (m + 1) divides (a |^ (2 * n)) - (b |^ (2 * n))
proof end;

theorem N3: :: NEWTON03:24
for a1, b1 being Complex holds (a1 |^ 3) - (b1 |^ 3) = (a1 - b1) * (((a1 |^ 2) + (b1 |^ 2)) + (a1 * b1))
proof end;

:: por NEWTON02:196;
theorem :: NEWTON03:25
for a, b being Nat
for n being odd Nat holds
( 3 divides (a |^ n) + (b |^ n) iff 3 divides a + b )
proof end;

theorem D3: :: NEWTON03:26
for a, b, n being Nat
for c being Integer st c divides a - b holds
c divides (a |^ n) - (b |^ n)
proof end;

theorem :: NEWTON03:27
for a, b being Nat
for n being odd Nat holds
( 3 divides (a |^ n) - (b |^ n) iff 3 divides a - b )
proof end;

theorem :: NEWTON03:28
for a, b, n being Nat holds a |^ n,(a - b) |^ n are_congruent_mod b
proof end;

theorem :: NEWTON03:29
for a being non trivial Nat ex n being prime Nat st n divides a
proof end;

theorem PSQ: :: NEWTON03:30
for k being Nat
for p being prime Nat st p divides (p + (k + 1)) * (p - (k + 1)) holds
k + 1 >= p
proof end;

theorem :: NEWTON03:31
for p being prime Nat
for k being non zero Nat st k < p holds
not p divides (p |^ 2) - (k |^ 2)
proof end;

theorem SUD: :: NEWTON03:32
for a, b being Integer
for p being odd prime Nat st not p divides b & p divides a - b holds
not p divides a + b
proof end;

LmSQ: for p being prime Nat
for k being square Nat st p divides k holds
p ^2 divides k
proof end;

theorem :: NEWTON03:33
for a being non zero square Element of NAT
for p being prime Nat st p divides a holds
not a + p is square
proof end;

theorem :: NEWTON03:34
for a being non zero square Element of NAT
for p being prime Nat st a + p is square holds
p = (2 * (sqrt a)) + 1
proof end;

NAT517: for c, a, b being Nat st a,b are_coprime holds
c gcd (a * b) = (c gcd a) * (c gcd b)
proof end;

theorem :: NEWTON03:35
for a, b, c being Integer st a,b are_coprime holds
c gcd (a * b) = (c gcd a) * (c gcd b)
proof end;

theorem :: NEWTON03:36
for a, n being Nat
for p being prime Nat st a divides p |^ n holds
ex k being Nat st a = p |^ k
proof end;

theorem :: NEWTON03:37
for a, b being non zero Nat
for p being prime Nat st a + b = p holds
a,b are_coprime
proof end;

theorem :: NEWTON03:38
for n being Nat
for a, b being non zero Nat
for p being prime Nat st (a |^ n) + (b |^ n) = p |^ n holds
a,b are_coprime
proof end;

theorem :: NEWTON03:39
for c, k being Nat
for a, b being non zero Nat st c >= a + b holds
(c |^ (k + 1)) * (a + b) > (a |^ (k + 2)) + (b |^ (k + 2))
proof end;

theorem :: NEWTON03:40
for a, c being Nat
for b being non zero Nat st a * b < c & c < a * (b + 1) holds
( not a divides c & not c divides a )
proof end;

theorem MinMax: :: NEWTON03:41
for a, b being Real holds a + b = (min (a,b)) + (max (a,b))
proof 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: :: NEWTON03:42
for n being Nat
for a, b being non negative Real holds
( max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n & min ((a |^ n),(b |^ n)) = (min (a,b)) |^ n )
proof end;

theorem :: NEWTON03:43
for a, b, n being Nat
for p being prime Nat st a * b = p |^ n holds
ex k, l being Nat st
( a = p |^ k & b = p |^ l & k + l = n )
proof end;

:: according to ATP it may be proved by PYTHTRIP:def 1
theorem NTC: :: NEWTON03:44
for a, b being non trivial Nat st a,b are_coprime holds
( not a divides b & not b divides a )
proof end;

theorem :: NEWTON03:45
for a being non trivial Nat
for p being prime Nat st p > a holds
( not p divides a & not a divides p )
proof end;

theorem GCDP: :: NEWTON03:46
for a being Nat
for p being prime Nat holds
( a gcd p = 1 or a gcd p = p )
proof end;

theorem :: NEWTON03:47
for n being Nat
for a being non trivial Nat
for p being prime Nat st a divides p |^ n holds
p divides a
proof end;

:: Count
theorem SC1: :: NEWTON03:48
for a, b being odd Nat
for m being even Nat holds 2 |-count ((a |^ m) + (b |^ m)) = 1
proof end;

LmC1: for a being non zero Nat
for p being non trivial Nat holds
( p |^ (p |-count a) divides a & not p * (p |^ (p |-count a)) divides a )
proof end;

theorem :: NEWTON03:49
for a being non zero Nat ex k being odd Nat st a = (2 |^ (2 |-count a)) * k
proof end;

:: must precede definition of |-count for Integers.
theorem :: NEWTON03:50
for a being Nat
for b being non zero Nat st a > b holds
ex p being prime Nat st p |-count a > p |-count b
proof end;

theorem NAT330: :: NEWTON03:51
for a, b, c being Nat st a <> 1 & b <> 0 & c <> 0 & b > a |-count c holds
not a |^ b divides c
proof end;

theorem CountD: :: NEWTON03:52
for b being non zero Integer
for a being Integer st |.a.| <> 1 holds
( a |^ (|.a.| |-count |.b.|) divides b & not a |^ ((|.a.| |-count |.b.|) + 1) divides b )
proof end;

theorem CountD1: :: NEWTON03:53
for n being Nat
for b being non zero Integer
for a being Integer st |.a.| <> 1 & a |^ n divides b & not a |^ (n + 1) divides b holds
n = |.a.| |-count |.b.|
proof end;

theorem CD: :: NEWTON03:54
for b being non zero Nat
for a being non trivial Nat holds
( a divides b iff a |-count (a gcd b) = 1 )
proof end;

theorem :: NEWTON03:55
for b, n being non zero Nat
for a being non trivial Nat holds
( a |-count (a gcd b) = 1 iff (a |^ n) |-count ((a gcd b) |^ n) = 1 )
proof end;

theorem :: NEWTON03:56
for b being non zero Nat
for a being non trivial Nat holds
( a |-count (a gcd b) = 0 iff not a |-count (a gcd b) = 1 )
proof end;

definition
let a, b be Integer;
func a |-count b -> Nat equals :: NEWTON03:def 6
|.a.| |-count |.b.|;
coherence
|.a.| |-count |.b.| is Nat ;
end;

:: deftheorem defines |-count NEWTON03:def 6 :
for a, b being Integer holds a |-count b = |.a.| |-count |.b.|;

definition
let a be Integer;
assume A0: |.a.| <> 1 ;
let b be non zero Integer;
redefine func a |-count b means :Def6: :: NEWTON03:def 7
( a |^ it divides b & not a |^ (it + 1) divides b );
compatibility
for b1 being Nat holds
( b1 = a |-count b iff ( a |^ b1 divides b & not a |^ (b1 + 1) divides b ) ) by A0, CountD, CountD1;
end;

:: deftheorem Def6 defines |-count NEWTON03:def 7 :
for a being Integer st |.a.| <> 1 holds
for b being non zero Integer
for b3 being Nat holds
( b3 = a |-count b iff ( a |^ b3 divides b & not a |^ (b3 + 1) divides b ) );

theorem NAT328: :: NEWTON03:57
for p being prime Nat
for a, b being non zero Integer holds p |-count (a * b) = (p |-count a) + (p |-count b)
proof end;

theorem Count0: :: NEWTON03:58
for a being non trivial Nat
for b being non zero Nat holds a |^ (a |-count b) <= b
proof end;

theorem Count1: :: NEWTON03:59
for n being Nat
for a being non trivial Nat
for b being non zero Integer holds
( a |^ n divides b iff n <= a |-count b )
proof end;

theorem Count2: :: NEWTON03:60
for a being non trivial Nat
for b being non zero Integer
for n being non zero Nat holds
( n * (a |-count b) <= a |-count (b |^ n) & a |-count (b |^ n) < n * ((a |-count b) + 1) )
proof end;

theorem :: NEWTON03:61
for a being non trivial Nat
for b, n being non zero Nat st b < a holds
a |-count (b |^ n) < n
proof end;

theorem Count4: :: NEWTON03:62
for n being Nat
for a being non trivial Nat
for b being non zero Nat st b < a |^ n holds
a |-count b < n
proof end;

theorem :: NEWTON03:63
for a, b being non zero Nat
for n being non trivial Nat holds (a + b) |-count ((a |^ n) + (b |^ n)) < n
proof end;

theorem :: NEWTON03:64
for a, b being non zero Nat holds
( a gcd b = 1 iff for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 )
proof end;

ABS1: for a, b being Integer st |.a.| <> |.b.| holds
( a - b <> 0 & a + b <> 0 )
proof end;

theorem :: NEWTON03:65
for m being non zero even Nat
for a, b being odd Nat st a <> b holds
2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) >= (2 |-count ((a |^ m) - (b |^ m))) + 1
proof end;

theorem :: NEWTON03:66
for m being non zero even Nat
for a, b being odd Nat st a <> b holds
2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count ((a |^ m) - (b |^ m))) + 1
proof end;

theorem :: NEWTON03:67
for p being prime Nat
for a, b being Integer st |.a.| <> |.b.| holds
p |-count ((a |^ 2) - (b |^ 2)) = (p |-count (a - b)) + (p |-count (a + b))
proof end;

theorem :: NEWTON03:68
for p being prime Nat
for a, b being Integer st |.a.| <> |.b.| holds
p |-count ((a |^ 3) - (b |^ 3)) = (p |-count (a - b)) + (p |-count (((a |^ 2) + (a * b)) + (b |^ 2)))
proof end;

theorem GL: :: NEWTON03:69
for a, b being non zero Nat holds a / (a gcd b) = (a lcm b) / b
proof end;

theorem LCM2: :: NEWTON03:70
for a, n being Nat
for b being non zero Nat holds a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b)
proof end;

theorem :: NEWTON03:71
for a, n being Nat
for b being non zero Nat holds a lcm (((n * a) + 1) * b) = ((n * a) + 1) * (a lcm b)
proof end;

theorem :: NEWTON03:72
for a being non trivial Nat
for n, b being non zero Nat holds a |-count b >= n * ((a |^ n) |-count b)
proof end;

theorem NEWTON0258: :: NEWTON03:73
for a, b being odd Integer holds
( 4 divides a - b iff not 4 divides a + b )
proof end;

theorem :: NEWTON03:74
for a, b being odd Integer holds 2 |-count ((a |^ 2) + (b |^ 2)) = 1
proof end;

theorem :: NEWTON03:75
for p being prime Nat
for a, b being Nat st a <> b holds
p |-count (a + b) >= p |-count (a gcd b)
proof end;

:: p |-count (a + b)
theorem DX: :: NEWTON03:76
for a being non zero Integer
for b being non trivial Nat
for c being Integer st a = (b |^ (b |-count a)) * c holds
not b divides c
proof end;

registration
let a be non zero Integer;
let b be non trivial Nat;
cluster a / (b |^ (b |-count a)) -> integer ;
coherence
a / (b |^ (b |-count a)) is integer
proof end;
end;

registration
let a be non zero Integer;
cluster a / (2 |^ (2 |-count a)) -> integer ;
coherence
a / (2 |^ (2 |-count a)) is integer
proof end;
cluster a / (2 |^ (2 |-count a)) -> odd ;
coherence
a / (2 |^ (2 |-count a)) is odd
proof end;
end;

theorem NAT327: :: NEWTON03:77
for a being non zero Integer
for b being non trivial Nat holds
( b |-count a = 0 iff not b divides a )
proof end;

registration
let a be odd Integer;
cluster 2 |-count a -> zero ;
coherence
2 |-count a is zero
proof end;
reduce a / (2 |^ (2 |-count a)) to a;
reducibility
a / (2 |^ (2 |-count a)) = a
proof end;
end;

theorem NAT332: :: NEWTON03:78
for a being prime Nat
for b being non zero Integer
for c being Nat holds a |-count (b |^ c) = c * (a |-count b)
proof end;

theorem :: NEWTON03:79
for a, b being non zero Nat
for n being 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 end;

theorem Odd: :: NEWTON03:80
for a, b being odd Integer
for n being Nat holds 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b)
proof end;

theorem :: NEWTON03:81
for a, b being odd Integer
for m being odd Nat holds 2 |-count ((a |^ m) + (b |^ m)) = 2 |-count (a + b)
proof end;

:: a <> b would not be necessary if 2 |-count 0 is defined
theorem :: NEWTON03:82
for a, b being odd Nat st a <> b holds
1 = min ((2 |-count (a - b)),(2 |-count (a + b)))
proof end;

theorem DL: :: NEWTON03:83
for a being non trivial Nat
for b, c being non zero Integer st a |-count b > a |-count c holds
( a |^ (a |-count c) divides b & not a |^ (a |-count b) divides c )
proof end;

theorem :: NEWTON03:84
for a being non trivial Nat
for b, c being non zero Integer st a |^ (a |-count b) divides c & a |^ (a |-count c) divides b holds
a |-count b = a |-count c
proof end;

theorem PP: :: NEWTON03:85
for a, b being Integer
for m, n being Nat st a |^ n divides b & not a |^ m divides b holds
m > n
proof end;

theorem DN: :: NEWTON03:86
for n being Nat
for a being non trivial Nat
for b, c being non zero Integer st a |-count b = a |-count c & a |^ n divides b holds
a |^ n divides c
proof end;

theorem DIC: :: NEWTON03:87
for a being non trivial Nat
for b, c being non zero Integer holds
( a |-count b = a |-count c iff for n being Nat holds
( a |^ n divides b iff a |^ n divides c ) )
proof end;

theorem :: NEWTON03:88
for a, b being 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 end;

:: MOEBIUS1:6, for non prime numbers
theorem MOB16: :: NEWTON03:89
for b being non trivial Nat
for a being non zero Integer holds
( b |-count a <> 0 iff b divides a )
proof end;

theorem :: NEWTON03:90
for b being non trivial Nat
for a being non zero Nat holds
( b |-count a = 0 iff a mod b <> 0 )
proof end;

theorem :: NEWTON03:91
for p being prime Nat
for a being non trivial Nat holds a |-count p <= 1
proof end;

theorem Count7: :: NEWTON03:92
for a, b being non trivial Nat
for c being non zero Nat holds a |^ ((a |-count b) * (b |-count c)) <= c
proof end;

theorem :: NEWTON03:93
for p being prime Nat
for a being non trivial Nat
for b being non zero Nat holds a |-count (p |^ b) <= b
proof end;

theorem :: NEWTON03:94
for n being Nat
for p being prime Nat
for a being non trivial Nat holds (p |-count a) * (a |-count (p |^ n)) <= n
proof end;

theorem :: NEWTON03:95
for a, b being non trivial Nat
for c being non zero Nat holds (a |-count b) * (b |-count c) <= a |-count c
proof end;

theorem :: NEWTON03:96
for a being non zero Nat
for b being odd Nat holds 2 |-count (a * b) = 2 |-count a
proof end;

theorem :: NEWTON03:97
for n being Nat
for a being non trivial Nat holds (a |^ (n + 1)) + (a |^ n) < a |^ (n + 2)
proof end;

theorem LmNT: :: NEWTON03:98
for n being Nat
for a being non trivial Nat holds ((a + 1) |^ n) + ((a + 1) |^ n) < (a + 1) |^ (n + 1)
proof end;

theorem :: NEWTON03:99
for n being Nat
for a being non trivial odd Nat holds (a |^ n) + (a |^ n) < a |^ (n + 1)
proof end;

theorem :: NEWTON03:100
for a, b, c being Nat
for p being non trivial Nat st not a divides b holds
(p |^ a) |^ c <> p |^ b
proof end;

LmC10: for a being Integer
for b being non zero Integer
for n being non zero Nat st a = b |^ n holds
for p being prime Nat holds n divides p |-count a
proof end;

theorem :: NEWTON03:101
for a, b being non zero Integer
for n being non zero Nat st not for p being prime Nat holds n divides p |-count a holds
a <> b |^ n by LmC10;

theorem :: NEWTON03:102
for a, b being non zero Integer
for n being non zero Nat st a = b |^ n holds
for p being prime Nat holds n divides p |-count a by LmC10;

theorem :: NEWTON03:103
for a, b being positive Real
for n being non trivial Nat holds (a + b) |^ n > (a |^ n) + (b |^ n)
proof end;

theorem :: NEWTON03:104
for a, b being non zero Integer
for p being 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 end;

theorem :: NEWTON03:105
for n being Nat
for a being non trivial Nat
for b being non zero Integer holds a |-count ((a |^ n) * b) = n + (a |-count b)
proof end;