:: 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 b₁ being set holds
( b₁ = a ^2 iff b₁ = 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 b₁ being Nat holds
( b₁ = a gcd b iff b₁ = |.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 b₁ being Nat holds
( b₁ = a lcm b iff b₁ = |.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 b₁ being odd Nat holds b₁ 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 b₁ being even Nat holds b₁ 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 b₁ being Element of NAT holds b₁ is square

proof end;

end;

registration

cluster prime -> non square for Element of NAT ;

coherence
for b₁ being Element of NAT st b₁ is prime holds
not b₁ 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 b₁ being prime Nat st b₁ 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 b₁ being prime Nat st b₁ is odd ;

proof end;

end;

registration

cluster integer prime -> non square for object ;

coherence
for b₁ being Integer st b₁ is prime holds
not b₁ 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 b₁ being Integer holds b₁ is square by INT_2:28;

end;

registration

cluster natural zero -> trivial for set ;

correctness
coherence
for b₁ being Nat st b₁ is zero holds
b₁ 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 b₁ being Nat st b₁ 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 b₁ being Element of NAT holds b₁ 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 b₁ being square Element of NAT holds b₁ is trivial

proof end;

end;

registration

cluster trivial natural -> square for set ;

coherence
for b₁ being Nat st b₁ is trivial holds
b₁ is square

proof end;

end;

registration

cluster integer non square -> non zero for object ;

coherence
for b₁ being Integer st not b₁ is square holds
not b₁ 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 b₁ being even Nat holds b₁ 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 b₁ being Nat holds
( b₁ = a |-count b iff ( a |^ b₁ divides b & not a |^ (b₁ + 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 b₃ being Nat holds
( b₃ = a |-count b iff ( a |^ b₃ divides b & not a |^ (b₃ + 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;