:: by Rafa{\l} Ziobro

::

:: Received June 30, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

registration
end;

registration
end;

:: some remarks on divisibility of the differences of like powers

LmGCD: for a, b, c, d being Integer st b divides a & d divides c holds

b * d divides a * c

proof end;

::see also NAT_3:1

theorem :: NEWTON02:2

Lm0c: for a, b being Nat

for u being Integer holds (a + (u * b)) gcd b = a gcd b

proof end;

Lm0d: for t, u, z being Integer holds (t + (u * z)) gcd z = t gcd z

proof end;

Lm1: for a, b, n, k being Nat st b > 0 & k > 0 & a + b > k & a + b divides k * (a |^ n) holds

not a,b are_coprime

proof end;

Lm2: for x being Nat

for t, z being Integer st t divides ((t + z) |^ x) - (z |^ x) holds

t divides (((t + z) |^ x) * z) - (z |^ (x + 1))

proof end;

Lm5a: for a, b being Nat st a is odd & a gcd b = 1 holds

a gcd (2 * b) = 1

proof end;

Lm5b: for a, b being Nat st a is even & a gcd b = 1 holds

a gcd (2 * b) = 2

proof end;

Lm5: for b, c being Nat st b,c are_coprime holds

((2 * b) + c) gcd c <= 2

proof end;

Lm6: for a, b, k, l being Nat st a > 0 & a = (a gcd b) * k & b = (a gcd b) * l holds

k gcd l = 1

proof end;

theorem Th10: :: NEWTON02:10

for n being Nat

for t, z being Integer holds

( t divides ((t + z) |^ n) - (z |^ n) & z divides ((t + z) |^ n) - (t |^ n) )

for t, z being Integer holds

( t divides ((t + z) |^ n) - (z |^ n) & z divides ((t + z) |^ n) - (t |^ n) )

proof end;

theorem :: NEWTON02:12

for n being Nat

for t, z being Integer st t divides (t + z) |^ n holds

t divides ((t + z) |^ n) + (z |^ n)

for t, z being Integer st t divides (t + z) |^ n holds

t divides ((t + z) |^ n) + (z |^ n)

proof end;

theorem Th17: :: NEWTON02:17

for m being Nat

for t, z being Integer st m > 0 holds

t * z divides ((t + z) |^ m) - ((t |^ m) + (z |^ m))

for t, z being Integer st m > 0 holds

t * z divides ((t + z) |^ m) - ((t |^ m) + (z |^ m))

proof end;

theorem Th19: :: NEWTON02:19

for n being Nat

for t, z being Integer st n > 0 holds

t * z divides ((t - z) |^ n) - ((t |^ n) + ((- z) |^ n))

for t, z being Integer st n > 0 holds

t * z divides ((t - z) |^ n) - ((t |^ n) + ((- z) |^ n))

proof end;

theorem Th20: :: NEWTON02:20

for n being Nat

for t, z being Integer holds t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))

for t, z being Integer holds t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))

proof end;

theorem :: NEWTON02:21

for n being Nat

for t, z being Integer st n > 0 holds

t divides ((t + z) |^ n) + ((t |^ n) - (z |^ n))

for t, z being Integer st n > 0 holds

t divides ((t + z) |^ n) + ((t |^ n) - (z |^ n))

proof end;

theorem Th22: :: NEWTON02:22

for t, u, z being Integer st u divides t + z & u divides t - z holds

( u divides 2 * t & u divides 2 * z )

( u divides 2 * t & u divides 2 * z )

proof end;

theorem :: NEWTON02:23

for n being Nat

for t, z being Integer holds t * z divides ((t + z) |^ (2 * n)) - ((t - z) |^ (2 * n))

for t, z being Integer holds t * z divides ((t + z) |^ (2 * n)) - ((t - z) |^ (2 * n))

proof end;

theorem :: NEWTON02:24

for n being Nat

for t, z being Integer st n > 0 holds

t * z divides ((t - z) |^ (2 * n)) - ((t |^ (2 * n)) + (z |^ (2 * n)))

for t, z being Integer st n > 0 holds

t * z divides ((t - z) |^ (2 * n)) - ((t |^ (2 * n)) + (z |^ (2 * n)))

proof end;

theorem :: NEWTON02:25

for n being Nat

for t, z being Integer holds t * z divides ((t - z) |^ ((2 * n) + 1)) - ((t |^ ((2 * n) + 1)) - (z |^ ((2 * n) + 1)))

for t, z being Integer holds t * z divides ((t - z) |^ ((2 * n) + 1)) - ((t |^ ((2 * n) + 1)) - (z |^ ((2 * n) + 1)))

proof end;

:: gcd

Lm6: for t, z being Integer st t + z,z are_coprime holds

t + z,t are_coprime

proof end;

theorem :: NEWTON02:29

theorem Th31: :: NEWTON02:31

for n, a, b being Nat st a,b are_coprime & a + b > 2 holds

( a + b divides (a |^ n) + (b |^ n) iff not a + b divides (a |^ n) - (b |^ n) )

( a + b divides (a |^ n) + (b |^ n) iff not a + b divides (a |^ n) - (b |^ n) )

proof end;

theorem :: NEWTON02:32

for a, b, n being Nat st a,b are_coprime & a + b > 2 & n is odd holds

not a + b divides (a |^ n) - (b |^ n)

not a + b divides (a |^ n) - (b |^ n)

proof end;

theorem :: NEWTON02:33

for a, b, n being Nat st a,b are_coprime & a + b > 2 & n is even holds

not a + b divides (a |^ n) + (b |^ n)

not a + b divides (a |^ n) + (b |^ n)

proof end;

:: inequalities (see also SERIES_3)

theorem :: NEWTON02:42

theorem :: NEWTON02:44

for a, b, n being Nat st n > 0 & a > b & a,b are_coprime holds

((a |^ n) + (b |^ n)) gcd ((a |^ n) - (b |^ n)) <= 2

((a |^ n) + (b |^ n)) gcd ((a |^ n) - (b |^ n)) <= 2

proof end;

Lm20: for t, u being Integer st t is even & t,u are_coprime holds

u is odd

proof end;

theorem :: NEWTON02:46

for t, u, z being Integer st t,z are_coprime & t,u are_coprime & t is even holds

( u + z is even & u - z is even & u * z is odd )

( u + z is even & u - z is even & u * z is odd )

proof end;

theorem :: NEWTON02:47

for a, b, c, n being Nat st a,b are_coprime & c is even & (a |^ n) + (b |^ n) = c |^ n holds

( a + b is even & a - b is even )

( a + b is even & a - b is even )

proof end;

Lm33: for a, b being Nat st 3 divides ((a + b) * (a - b)) + (a * b) holds

3 divides a

proof end;

Lm34: for a, b being Nat st 3 divides ((a + b) * (a - b)) + (a * b) holds

3 divides b

proof end;

theorem Th51: :: NEWTON02:51

for a, b being Nat holds

( 3 divides ((a + b) * (a - b)) + (a * b) iff ( 3 divides a & 3 divides b ) )

( 3 divides ((a + b) * (a - b)) + (a * b) iff ( 3 divides a & 3 divides b ) )

proof end;

theorem :: NEWTON02:56

for a, b, n being Nat st n > 0 & a <> b holds

(2 * (a |^ n)) * (b |^ n) < (a |^ (2 * n)) + (b |^ (2 * n))

(2 * (a |^ n)) * (b |^ n) < (a |^ (2 * n)) + (b |^ (2 * n))

proof end;

:: division by 4

Lm60: for a, b, m being odd Nat st 4 divides a + b holds

4 divides (a |^ m) + (b |^ m)

proof end;

theorem :: NEWTON02:66

for t being Integer st t is even & not 4 divides t holds

ex u being Integer st

( u = t / 2 & u is odd )

ex u being Integer st

( u = t / 2 & u is odd )

proof end;

Lm63: for a being Nat st a is even & not 4 divides a holds

ex b being Nat st

( b = a / 2 & b is odd )

proof end;

theorem :: NEWTON02:70

for a, b, c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 holds

ex t being Integer st b |^ 2 = ((2 * a) + t) * t

ex t being Integer st b |^ 2 = ((2 * a) + t) * t

proof end;

theorem :: NEWTON02:71

for a, b being Nat

for t being Integer st b |^ 2 = ((2 * a) + t) * t holds

ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

for t being Integer st b |^ 2 = ((2 * a) + t) * t holds

ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

proof end;

Lm40: for a, b, c being Nat st a is odd & b is odd holds

(a |^ 2) + (b |^ 2) <> c |^ 2

proof end;

theorem Th74: :: NEWTON02:74

for a, b, n being Nat st a,b are_coprime holds

((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) gcd n

((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) gcd n

proof end;

theorem :: NEWTON02:76

for a, b, n being Nat st a,b are_coprime holds

((a - b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) + (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) + (((n - 2) * a) * b)) gcd n

((a - b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) + (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) + (((n - 2) * a) * b)) gcd n

proof end;

theorem Th83: :: NEWTON02:83

for a, b, c, m, l being Nat

for n being positive Nat holds ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = (b + c) mod a

for n being positive Nat holds ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = (b + c) mod a

proof end;

theorem :: NEWTON02:84

for b, c, m, l being Nat

for a, n being positive Nat holds

( a divides (b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l)) iff a divides b + c )

for a, n being positive Nat holds

( a divides (b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l)) iff a divides b + c )

proof end;

theorem :: NEWTON02:85

for a being Nat

for t being Integer holds

( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )

for t being Integer holds

( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )

proof end;

Lm3: for t being Integer holds

( t mod 3 = 0 or t mod 3 = 1 or t mod 3 = 2 )

proof end;

LmMod: for n being odd Nat holds (2 |^ n) mod 3 = 2

proof end;

LmSum: for a, b, c being Nat holds ((a + b) - c) mod 3 = (((a mod 3) + (b mod 3)) + (2 * (c mod 3))) mod 3

proof end;

theorem Th89: :: NEWTON02:89

for a, b, c being Nat

for n being odd Nat holds ((a + b) - c) mod 3 = (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3

for n being odd Nat holds ((a + b) - c) mod 3 = (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3

proof end;

LmABC: for t, u, z being Integer holds

( not 3 divides (u + t) + z or 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

proof end;

LmAB3: for t, u, z being Integer holds

( not u + t = z or 3 divides (u * t) * z or 3 divides u - t )

proof end;

theorem :: NEWTON02:92

for t, z being Integer

for a, n being non zero Nat st t mod a = z mod a holds

(t |^ n) mod a = (z |^ n) mod a

for a, n being non zero Nat st t mod a = z mod a holds

(t |^ n) mod a = (z |^ n) mod a

proof end;

theorem :: NEWTON02:94

for a, b, c being Nat

for n being odd Nat holds

( 3 divides (a + b) - c iff 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) )

for n being odd Nat holds

( 3 divides (a + b) - c iff 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) )

proof end;

theorem :: NEWTON02:95

for t, u, z being Integer holds ((t + u) - z) |^ 2,((t |^ 2) + (u |^ 2)) + (z |^ 2) are_congruent_mod 2

proof end;

LmTUZ: for t, u, z being Integer holds ((t + u) + z) |^ 3,((t |^ 3) + (u |^ 3)) + (z |^ 3) are_congruent_mod 3

proof end;

theorem :: NEWTON02:96

for t, u, z being Integer holds ((t + u) - z) |^ 3,((t |^ 3) + (u |^ 3)) - (z |^ 3) are_congruent_mod 3

proof end;

theorem :: NEWTON02:99

for m being Nat holds

( (2 |^ m) - 1 divides (2 |^ ((2 * m) + 1)) - 2 & (2 |^ m) + 1 divides (2 |^ ((2 * m) + 1)) - 2 )

( (2 |^ m) - 1 divides (2 |^ ((2 * m) + 1)) - 2 & (2 |^ m) + 1 divides (2 |^ ((2 * m) + 1)) - 2 )

proof end;

theorem :: NEWTON02:101

for n being Nat

for t, u, z being Integer st (t |^ n) + (u |^ n) = z |^ n holds

2 |^ n divides ((t * u) * z) |^ n

for t, u, z being Integer st (t |^ n) + (u |^ n) = z |^ n holds

2 |^ n divides ((t * u) * z) |^ n

proof end;

:: Seg vs Segm

theorem :: NEWTON02:106

theorem Th7: :: NEWTON02:107

for m, n being Nat

for f being FinSequence of REAL st n in dom f & 1 <= m & m <= n holds

f . m = (f | n) . m

for f being FinSequence of REAL st n in dom f & 1 <= m & m <= n holds

f . m = (f | n) . m

proof end;

theorem :: NEWTON02:108

for n being Nat

for f being FinSequence of REAL

for D being set st f is FinSequence of D holds

( f | n is FinSequence of D & f /^ n is FinSequence of D )

for f being FinSequence of REAL

for D being set st f is FinSequence of D holds

( f | n is FinSequence of D & f /^ n is FinSequence of D )

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let f be FinSequence of NAT ;

let n, k be Nat;

coherence

(f | n) . k is natural ;

coherence

((f | n) /^ 1) . k is natural ;

end;
let n, k be Nat;

coherence

(f | n) . k is natural ;

coherence

((f | n) /^ 1) . k is natural ;

theorem Th15: :: NEWTON02:113

for n, k being Nat

for f being FinSequence of REAL st k in dom (f /^ n) & n in dom f holds

n + k in dom f

for f being FinSequence of REAL st k in dom (f /^ n) & n in dom f holds

n + k in dom f

proof end;

theorem Th16: :: NEWTON02:114

for n being Nat

for f being FinSequence of REAL

for k being positive Nat st n + k in dom f holds

k in dom (f /^ n)

for f being FinSequence of REAL

for k being positive Nat st n + k in dom f holds

k in dom (f /^ n)

proof end;

theorem Th17: :: NEWTON02:115

for f being FinSequence of REAL

for n being positive Nat st n + 1 = len f holds

Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1))

for n being positive Nat st n + 1 = len f holds

Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1))

proof end;

theorem :: NEWTON02:117

for n being Nat

for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds

len ((f | n) /^ 1) <= (len f) - 1

for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds

len ((f | n) /^ 1) <= (len f) - 1

proof end;

theorem Th20: :: NEWTON02:118

for n being Nat

for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds

len ((f | n) /^ 1) < n

for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds

len ((f | n) /^ 1) < n

proof end;

:: n choose k

:: factorial

Lm3: for c being Nat

for b being positive Nat holds b divides (b + c) !

proof end;

Lm4: for a, b being positive Nat st a,b ! are_coprime holds

a,b are_coprime

proof end;

theorem Th29: :: NEWTON02:127

for m being Nat

for f being FinSequence of REAL

for n being Nat st n in dom f & m in dom ((f | n) /^ 1) holds

((f | n) /^ 1) . m = f . (m + 1)

for f being FinSequence of REAL

for n being Nat st n in dom f & m in dom ((f | n) /^ 1) holds

((f | n) /^ 1) . m = f . (m + 1)

proof end;

:: Newton_Coeff

registration
end;

theorem Th34: :: NEWTON02:132

for n being positive Nat holds Sum (Newton_Coeff n) = ((Sum (((Newton_Coeff n) | n) /^ 1)) + ((Newton_Coeff n) . 1)) + ((Newton_Coeff n) . (n + 1))

proof end;

theorem Th38: :: NEWTON02:136

for m, n being Nat st m in dom (((Newton_Coeff n) | n) /^ 1) holds

(((Newton_Coeff n) | n) /^ 1) . m = (Newton_Coeff n) . (m + 1)

(((Newton_Coeff n) | n) /^ 1) . m = (Newton_Coeff n) . (m + 1)

proof end;

theorem :: NEWTON02:140

for k being Nat

for n being odd Prime st n = (2 * k) + 1 holds

( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 )

for n being odd Prime st n = (2 * k) + 1 holds

( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 )

proof end;

registration

let n be Nat;

correctness

compatibility

n \ = Newton_Coeff n;

by NEWTON:31;

correctness

compatibility

Newton_Coeff n = n \ ;

;

end;
correctness

compatibility

n \ = Newton_Coeff n;

by NEWTON:31;

correctness

compatibility

Newton_Coeff n = n \ ;

;

:: The use of this registration would make most of the above code unnecessary. I leave it as an illustration.

:: In_Power

:: In_Power

Lm1: for a, b, k, l being Nat holds ((a,b) In_Power (k + l)) . (k + 1) = (((k + l) choose k) * (a |^ l)) * (b |^ k)

proof end;

theorem :: NEWTON02:142

for a, b, k, l being Nat st k + l is prime & k > 0 & l > 0 holds

k + l divides ((a,b) In_Power (k + l)) . (k + 1)

k + l divides ((a,b) In_Power (k + l)) . (k + 1)

proof end;

Lm5: for a, b, m, n being Nat st m in dom ((((a,b) In_Power n) | n) /^ 1) holds

((((a,b) In_Power n) | n) /^ 1) . m = ((a,b) In_Power n) . (m + 1)

proof end;

theorem Th48: :: NEWTON02:146

for a, b being Nat

for m being positive Nat holds Sum ((a,b) In_Power m) = ((a |^ m) + (b |^ m)) + (Sum ((((a,b) In_Power m) | m) /^ 1))

for m being positive Nat holds Sum ((a,b) In_Power m) = ((a |^ m) + (b |^ m)) + (Sum ((((a,b) In_Power m) | m) /^ 1))

proof end;

theorem :: NEWTON02:147

for a, b, m, n being Nat holds Sum ((a,b) In_Power (m + n)) = (Sum ((a,b) In_Power m)) * (Sum ((a,b) In_Power n))

proof end;

theorem Th50: :: NEWTON02:148

for a, b, k, l being Nat st l > 0 holds

ex x being Nat st ((a,b) In_Power (k + l)) . (k + 1) = a * x

ex x being Nat st ((a,b) In_Power (k + l)) . (k + 1) = a * x

proof end;

theorem Th54: :: NEWTON02:152

for k being Nat

for n being prime Nat

for a, b being positive Nat holds (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k

for n being prime Nat

for a, b being positive Nat holds (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k

proof end;

theorem Th55: :: NEWTON02:153

for n being prime Nat

for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ n) - ((a |^ n) + (b |^ n))

for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ n) - ((a |^ n) + (b |^ n))

proof end;

theorem :: NEWTON02:155

theorem Th60: :: NEWTON02:158

for a, b being Nat

for n being prime Nat holds

( n divides a + b iff n divides (a |^ n) + (b |^ n) )

for n being prime Nat holds

( n divides a + b iff n divides (a |^ n) + (b |^ n) )

proof end;

theorem :: NEWTON02:159

theorem :: NEWTON02:162

theorem :: NEWTON02:163

theorem :: NEWTON02:165

for k being Nat

for n being prime Nat

for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k)

for n being prime Nat

for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k)

proof end;

theorem :: NEWTON02:166

for t being Integer

for n being prime Nat

for a, b being positive Nat st (n * a) * b divides ((a + t) |^ n) - ((a |^ n) + (b |^ n)) holds

(n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n)

for n being prime Nat

for a, b being positive Nat st (n * a) * b divides ((a + t) |^ n) - ((a |^ n) + (b |^ n)) holds

(n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n)

proof end;

theorem :: NEWTON02:167

for n being prime Nat

for a, b, c being positive Nat st (n * a) * b divides c - b holds

(n * a) * b divides ((a |^ n) + (b |^ n)) - ((a + c) |^ n)

for a, b, c being positive Nat st (n * a) * b divides c - b holds

(n * a) * b divides ((a |^ n) + (b |^ n)) - ((a + c) |^ n)

proof end;

theorem Th70: :: NEWTON02:168

for a, n being Nat

for p being prime Nat holds

( not p = (2 * n) + 1 or p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 )

for p being prime Nat holds

( not p = (2 * n) + 1 or p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 )

proof end;

theorem :: NEWTON02:169

for a being Nat

for p being prime Nat st not p divides a holds

ex n being Nat st

( p divides (a |^ n) - 1 & 0 < n & n < p )

for p being prime Nat st not p divides a holds

ex n being Nat st

( p divides (a |^ n) - 1 & 0 < n & n < p )

proof end;

theorem Th78: :: NEWTON02:176

for a, k, l being Nat st k <> l & k + 1 is odd & k + 1 is prime & l + 1 is odd & l + 1 is prime holds

(2 * (k + 1)) * (l + 1) divides (a |^ ((k * l) + 1)) - a

(2 * (k + 1)) * (l + 1) divides (a |^ ((k * l) + 1)) - a

proof end;

theorem Th84: :: NEWTON02:182

for a, n being Nat st (2 * n) + 1 is prime holds

for k being Nat st 2 * n > k & k > 1 holds

( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k )

for k being Nat st 2 * n > k & k > 1 holds

( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k )

proof end;

theorem Th85: :: NEWTON02:183

for a being Nat holds

( not 5 divides (a |^ 2) - 2 & not 5 divides (a |^ 2) + 2 & not 5 divides (a |^ 2) - 3 & not 5 divides (a |^ 2) + 3 )

( not 5 divides (a |^ 2) - 2 & not 5 divides (a |^ 2) + 2 & not 5 divides (a |^ 2) - 3 & not 5 divides (a |^ 2) + 3 )

proof end;

:: Pythagorean triples

theorem :: NEWTON02:184

for a, b, c being Nat holds

( not (a |^ 2) + (b |^ 2) = c |^ 2 or 5 divides a or 5 divides b or 5 divides c )

( not (a |^ 2) + (b |^ 2) = c |^ 2 or 5 divides a or 5 divides b or 5 divides c )

proof end;

theorem Th87: :: NEWTON02:185

for a being Nat holds

( not 7 divides (a |^ 3) - 2 & not 7 divides (a |^ 3) + 2 & not 7 divides (a |^ 3) - 3 & not 7 divides (a |^ 3) + 3 & not 7 divides (a |^ 3) - 4 & not 7 divides (a |^ 3) + 4 & not 7 divides (a |^ 3) - 5 & not 7 divides (a |^ 3) + 5 )

( not 7 divides (a |^ 3) - 2 & not 7 divides (a |^ 3) + 2 & not 7 divides (a |^ 3) - 3 & not 7 divides (a |^ 3) + 3 & not 7 divides (a |^ 3) - 4 & not 7 divides (a |^ 3) + 4 & not 7 divides (a |^ 3) - 5 & not 7 divides (a |^ 3) + 5 )

proof end;

theorem :: NEWTON02:187

for n, k, l being Nat holds

( not 2 |^ (k + l) divides (2 |^ (n + k)) - (2 |^ k) or l = 0 or n = 0 )

( not 2 |^ (k + l) divides (2 |^ (n + k)) - (2 |^ k) or l = 0 or n = 0 )

proof end;

theorem Th94: :: NEWTON02:192

for b, c being Nat

for a being positive Nat st b,c are_coprime & a + 1 divides b holds

not a + 1 divides c

for a being positive Nat st b,c are_coprime & a + 1 divides b holds

not a + 1 divides c

proof end;

theorem Th98: :: NEWTON02:196

for a, b, n being Nat

for p being prime Nat st p divides a + b holds

p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1))

for p being prime Nat st p divides a + b holds

p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1))

proof end;

theorem :: NEWTON02:197

for a, b, n being Nat

for p being prime Nat st not p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) & p divides (a |^ 2) - (b |^ 2) holds

p divides a - b

for p being prime Nat st not p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) & p divides (a |^ 2) - (b |^ 2) holds

p divides a - b

proof end;

theorem :: NEWTON02:199

for a, b, n being Nat st not 3 divides a & not 3 divides b & not 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) holds

3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))

3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))

proof end;

theorem :: NEWTON02:200

for a, b, c being Nat holds

( not (a |^ 3) + (b |^ 3) = c |^ 3 or 7 divides a or 7 divides b or 7 divides c )

( not (a |^ 3) + (b |^ 3) = c |^ 3 or 7 divides a or 7 divides b or 7 divides c )

proof end;