:: 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)))

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)))

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)))

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;

:: deftheorem Def0 defines trivial NEWTON03:def 1 :

for a being Nat holds

( a is trivial iff a <= 1 );

for a being Nat holds

( a is trivial iff a <= 1 );

definition

let a be Complex;

correctness

coherence

a ^2 is set ;

compatibility

for b_{1} being set holds

( b_{1} = a ^2 iff b_{1} = a |^ 2 );

by NEWTON:81;

end;
correctness

coherence

a ^2 is set ;

compatibility

for b

( b

by NEWTON:81;

definition

let a, b be Integer;

correctness

coherence

a gcd b is Nat;

compatibility

for b_{1} being Nat holds

( b_{1} = a gcd b iff b_{1} = |.a.| gcd |.b.| );

by INT_2:34;

correctness

coherence

a lcm b is Nat;

compatibility

for b_{1} being Nat holds

( b_{1} = a lcm b iff b_{1} = |.a.| lcm |.b.| );

by INT_2:33;

end;
correctness

coherence

a gcd b is Nat;

compatibility

for b

( b

by INT_2:34;

correctness

coherence

a lcm b is Nat;

compatibility

for b

( b

by INT_2:33;

:: deftheorem Def2 defines lcm NEWTON03:def 4 :

for a, b being Integer holds a lcm b = |.a.| lcm |.b.|;

for a, b being Integer holds a lcm b = |.a.| lcm |.b.|;

registration

let a, b be positive Real;

coherence

max (a,b) is positive by XXREAL_0:def 10;

coherence

min (a,b) is positive by XXREAL_0:def 9;

end;
coherence

max (a,b) is positive by XXREAL_0:def 10;

coherence

min (a,b) is positive by XXREAL_0:def 9;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let a, b be Integer;

correctness

reducibility

a gcd (a gcd b) = a gcd b;

reducibility

a lcm (a lcm b) = a lcm b;

end;
correctness

reducibility

a gcd (a gcd b) = a gcd b;

proof end;

correctness reducibility

a lcm (a lcm b) = a lcm b;

proof end;

registration
end;

registration
end;

registration
end;

registration

not for b_{1} being odd Nat holds b_{1} is trivial

not for b_{1} being even Nat holds b_{1} is trivial
end;

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

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

proof end;

registration
end;

registration
end;

registration

not for b_{1} being Element of NAT holds b_{1} is square
end;

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

proof end;

registration
end;

registration

existence

ex b_{1} being prime Nat st b_{1} is even ;

existence

ex b_{1} being prime Nat st b_{1} is odd ;

end;

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

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

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

ex b_{1} being Nat st b_{1} is square
end;

cluster epsilon-transitive epsilon-connected ordinal natural V31() integer dim-like complex ext-real non negative square for set ;

existence ex b

proof end;

registration

not for b_{1} being Element of NAT holds b_{1} is zero
by INT_2:28;

not for b_{1} being square Element of NAT holds b_{1} is trivial
end;

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

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

proof end;

registration
end;

registration
end;

registration

let a, b be Nat;

reducibility

(a * b) lcm a = a * b

(a gcd b) lcm b = b by NEWTON:53;

reducibility

a gcd (a lcm b) = a by NEWTON:54;

end;
reducibility

(a * b) lcm a = a * b

proof end;

reducibility (a gcd b) lcm b = b by NEWTON:53;

reducibility

a gcd (a lcm b) = a by NEWTON:54;

registration

let a, b be square Element of NAT ;

coherence

a gcd b is square

a lcm b is square

end;
coherence

a gcd b is square

proof end;

coherence a lcm b is square

proof end;

registration

let a, b be square Integer;

coherence

a gcd b is square

a lcm b is square

end;
coherence

a gcd b is square

proof end;

coherence a lcm b is square

proof end;

:: deftheorem Def3 defines odd NEWTON03:def 5 :

for t being Integer holds

( not t is odd iff not t gcd 2 = 1 );

for t being Integer holds

( not t is odd iff not t gcd 2 = 1 );

registration
end;

registration
end;

registration

let t, z be even Integer;

correctness

coherence

not t + z is odd ;

;

correctness

coherence

not t - z is odd ;

;

correctness

coherence

not t * z is odd ;

;

end;
correctness

coherence

not t + z is odd ;

;

correctness

coherence

not t - z is odd ;

;

correctness

coherence

not t * z is odd ;

;

registration

let t, z be odd Integer;

coherence

not t + z is odd ;

coherence

not t - z is odd ;

coherence

t * z is odd ;

end;
coherence

not t + z is odd ;

coherence

not t - z is odd ;

coherence

t * z is odd ;

registration

let t be odd Integer;

let z be even Integer;

coherence

t + z is odd ;

coherence

t - z is odd ;

coherence

not t * z is odd ;

end;
let z be even Integer;

coherence

t + z is odd ;

coherence

t - z is odd ;

coherence

not t * z is odd ;

registration
end;

registration
end;

registration
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 object ;

let b be non square Element of NAT ;

coherence

not a * b is square ;

end;
let b be non square Element of NAT ;

coherence

not a * b is square ;

registration

let a be non zero square Integer;

let n, m be Nat;

coherence

not (a |^ n) + (a |^ m) is square

end;
let n, m be Nat;

coherence

not (a |^ n) + (a |^ m) is square

proof end;

registration

let a be non zero square Element of NAT ;

let n, m be Nat;

coherence

not (a |^ n) + (a |^ m) is square ;

end;
let n, m be Nat;

coherence

not (a |^ n) + (a |^ m) is square ;

registration
end;

registration
end;

registration
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
end;

registration

let a, b be Integer;

let n, m be Nat;

not (((a |^ n) + (b |^ n)) * ((a |^ m) - (b |^ m))) + (((a |^ m) + (b |^ m)) * ((a |^ n) - (b |^ n))) is odd

not (((a |^ n) + (b |^ n)) * ((a |^ m) + (b |^ m))) + (((a |^ m) - (b |^ m)) * ((a |^ n) - (b |^ n))) is odd

end;
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;

registration
end;

registration
end;

registration

let b be non zero Nat;

let a, c be non trivial Nat;

reducibility

c |-count (c |^ (a |-count b)) = a |-count b by Def0, NAT_3:25;

end;
let a, c be non trivial Nat;

reducibility

c |-count (c |^ (a |-count b)) = a |-count b by Def0, NAT_3:25;

registration

let a, b be non zero Integer;

coherence

a / (a gcd b) is integer

(a lcm b) / b is integer

(a lcm b) / (a gcd b) is integer

end;
coherence

a / (a gcd b) is integer

proof end;

coherence (a lcm b) / b is integer

proof end;

coherence (a lcm b) / (a gcd b) is integer

proof end;

registration

not for b_{1} being even Nat holds b_{1} is zero
end;

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

proof end;

registration

let a be even Integer;

let n be non zero Nat;

coherence

not a * n is odd ;

coherence

not a |^ n is odd ;

end;
let n be non zero Nat;

coherence

not a * n is odd ;

coherence

not a |^ n is odd ;

registration
end;

registration

let a be non negative Real;

let n be non zero Nat;

reducibility

n -root (a |^ n) = a

(n -root a) |^ n = a

end;
let n be non zero Nat;

reducibility

n -root (a |^ n) = a

proof end;

reducibility (n -root a) |^ n = a

proof end;

:: solvable by ATP, yet not by verifier

:: Roots

:: see PEPIN:30;

:: see PEPIN:30;

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) ) )

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

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 :: 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

for a, p being Integer st p |^ ((2 * n) + k) divides a |^ 2 holds

p |^ n divides a

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))

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))

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))

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 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

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

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

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: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

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))

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 )

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;

:: 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;

:: 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 )

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 )

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 :: 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 )

for p being prime Nat st p > a holds

( not p divides a & not a divides 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

for a being non trivial Nat

for p being prime Nat st a divides p |^ n holds

p divides a

proof end;

:: Count

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;

:: 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

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 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 )

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.|

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 )

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 )

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 )

for a being non trivial Nat holds

( a |-count (a gcd b) = 0 iff not a |-count (a gcd b) = 1 )

proof end;

:: deftheorem defines |-count NEWTON03:def 6 :

for a, b being Integer holds a |-count b = |.a.| |-count |.b.|;

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;

for b_{1} being Nat holds

( b_{1} = a |-count b iff ( a |^ b_{1} divides b & not a |^ (b_{1} + 1) divides b ) )
by A0, CountD, CountD1;

end;
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 ( a |^ it divides b & not a |^ (it + 1) divides b );

for b

( b

:: deftheorem Def6 defines |-count NEWTON03:def 7 :

for a being Integer st |.a.| <> 1 holds

for b being non zero Integer

for b_{3} being Nat holds

( b_{3} = a |-count b iff ( a |^ b_{3} divides b & not a |^ (b_{3} + 1) divides b ) );

for a being Integer st |.a.| <> 1 holds

for b being non zero Integer

for b

( 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)

for a, b being non zero Integer holds p |-count (a * b) = (p |-count a) + (p |-count 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 )

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) )

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 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

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

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 )

( 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

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

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))

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)))

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 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)

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)

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)

for n, b being non zero Nat holds a |-count b >= n * ((a |^ n) |-count 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

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;

coherence

a / (b |^ (b |-count a)) is integer

end;
let b be non trivial Nat;

coherence

a / (b |^ (b |-count a)) is integer

proof end;

registration

let a be non zero Integer;

coherence

a / (2 |^ (2 |-count a)) is integer

a / (2 |^ (2 |-count a)) is odd

end;
coherence

a / (2 |^ (2 |-count a)) is integer

proof end;

coherence a / (2 |^ (2 |-count a)) is odd

proof 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 )

for b being non trivial Nat holds

( b |-count a = 0 iff not b divides a )

proof end;

registration

let a be odd Integer;

coherence

2 |-count a is zero

a / (2 |^ (2 |-count a)) = a

end;
coherence

2 |-count a is zero

proof end;

reducibility a / (2 |^ (2 |-count a)) = a

proof 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)

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)))

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)

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)

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 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 )

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

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 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

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 ) )

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) )

( 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 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

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

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

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

for c being non zero Nat holds (a |-count b) * (b |-count c) <= a |-count c

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)

for a being non trivial Nat holds ((a + 1) |^ n) + ((a + 1) |^ n) < (a + 1) |^ (n + 1)

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

theorem :: NEWTON03:102

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)))

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)

for a being non trivial Nat

for b being non zero Integer holds a |-count ((a |^ n) * b) = n + (a |-count b)

proof end;