:: Fermat's Little Theorem via Divisibility of {N}ewton's Binomial
:: by Rafa{\l} Ziobro
::
:: Received June 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


registration
let a be Complex;
reduce 1 * (a |^ 0) to 1;
reducibility
1 * (a |^ 0) = 1 by NEWTON:4;
end;

registration
let n be non zero Nat;
reduce 0 |^ n to 0 ;
reducibility
0 |^ n = 0 by NEWTON:84;
end;

registration
let a be Nat;
reduce |.a.| to a;
reducibility
|.a.| = a by ABSVALUE:29;
end;

registration
let a be Nat;
reduce a gcd 0 to a;
reducibility
a gcd 0 = a by NEWTON:52;
end;

registration
let t, z be Integer;
reduce (t mod z) mod z to t mod z;
reducibility
(t mod z) mod z = t mod z by NUMERAL2:14;
end;

registration
let t be Integer;
reduce 0 mod t to 0 ;
reducibility
0 mod t = 0 by INT_1:73;
end;

registration
let u, z be Integer;
reduce (0 + (u * z)) mod z to 0 ;
reducibility
(0 + (u * z)) mod z = 0
proof end;
end;

registration
let r be non zero Real;
let n be natural even number ;
cluster r |^ n -> positive ;
coherence
r |^ n is positive
proof end;
end;

:: some remarks on divisibility of the differences of like powers
theorem Th1: :: NEWTON02:1
for t, z being Integer holds t gcd z = (- t) gcd z
proof end;

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
for t, u, v, z being Integer st t divides z & u divides v holds
t * u divides z * v by LmGCD;

theorem Th3: :: NEWTON02:3
for t, z being Integer holds
( t divides z iff t gcd z = |.t.| )
proof end;

theorem :: NEWTON02:4
for t, u, z being Integer holds
( t * u divides z * u iff |.u.| * (t gcd z) = |.u.| * |.t.| )
proof end;

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;

theorem Th5: :: NEWTON02:5
for t, u, z being Integer holds
( (t + (u * z)) gcd z = t gcd z & (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;

theorem Th6: :: NEWTON02:6
for n being Nat
for t being Integer st n > 0 holds
t divides t |^ n
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 Th7: :: NEWTON02:7
for a, b, n being Nat holds (a |^ n) gcd (b |^ n) = (a gcd b) |^ n
proof end;

theorem Th8: :: NEWTON02:8
for a, b being Nat st a > b & a,b are_coprime holds
(a + b) gcd (a - b) <= 2
proof end;

theorem Th9: :: NEWTON02:9
for t, z being Integer holds
( t gcd z is even iff ( t is even & z is even ) )
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) )
proof end;

theorem Th11: :: NEWTON02:11
for n being Nat
for u, z being Integer holds
( u divides (u + z) |^ n iff u divides z |^ 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)
proof end;

theorem :: NEWTON02:13
for n being Nat
for t, u being Integer holds t + u divides ((t + (2 * u)) |^ n) - (u |^ n)
proof end;

theorem Th14: :: NEWTON02:14
for l being Nat
for t, z being Integer st l > 0 & t divides z holds
t divides z |^ l
proof end;

theorem Th15: :: NEWTON02:15
for n being Nat
for t, z being Integer st t divides z holds
t |^ n divides z |^ n
proof end;

theorem :: NEWTON02:16
for n being Nat
for t, z being Integer st n > 0 & not t divides (t + z) |^ n holds
not t divides z
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))
proof end;

theorem Th18: :: NEWTON02:18
for m being Nat
for t, z being Integer holds t - z divides (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))
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))
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))
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 )
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))
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)))
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)))
proof end;

theorem :: NEWTON02:26
for a, x, k being Nat st k > 0 & x divides a + k & x divides a - k holds
x <= 2 * k
proof end;

:: gcd
theorem :: NEWTON02:27
for a, b, k being Nat st k > 0 holds
a gcd b <= a gcd (b * k)
proof end;

theorem :: NEWTON02:28
for a, b, n being Nat st n > 0 holds
(a gcd b) gcd (b |^ n) = a gcd b
proof end;

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

theorem :: NEWTON02:29
for t, z being Integer holds
( t + z,t are_coprime iff t + z,z are_coprime ) by Lm6;

theorem :: NEWTON02:30
for a, b, c, n being Nat st a,b are_coprime & a * b = c |^ n holds
ex k being Nat st k |^ n = a
proof end;

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

theorem Th27: :: NEWTON02:34
for a, b, n being Nat st a,b are_coprime holds
a * b,(a |^ (n + 1)) + (b |^ (n + 1)) are_coprime
proof end;

theorem Th28: :: NEWTON02:35
for a, b, n being Nat st a,b are_coprime holds
a * b,(a |^ (n + 1)) - (b |^ (n + 1)) are_coprime
proof end;

theorem Th29: :: NEWTON02:36
for n being Nat
for q being real number st q > 0 & n > 0 holds
ex r being real number st q = r |^ n
proof end;

theorem :: NEWTON02:37
for a, b, k being Nat st k > 0 & a + b > k & a + b divides k * a holds
not a,b are_coprime
proof end;

theorem :: NEWTON02:38
for n, k being Nat st k > 1 holds
not k divides (k + 1) |^ n
proof end;

theorem :: NEWTON02:39
for a, b, n being Nat st a > 1 & b > 0 & a gcd b = 1 holds
not a divides (a + b) |^ n
proof end;

:: inequalities (see also SERIES_3)
theorem Th40: :: NEWTON02:40
for c being Nat st c > 0 holds
for r, s being non negative Real holds
( r < s iff r |^ c < s |^ c )
proof end;

theorem :: NEWTON02:41
for n being Nat
for r, s being non negative Real st r >= s holds
r |^ n >= s |^ n
proof end;

theorem :: NEWTON02:42
for a, b, n being Nat st a > 0 & n > 0 holds
ex r being real number st (a |^ n) + (b |^ n) = r |^ n by Th29;

theorem :: NEWTON02:43
for n, a being Nat ex b being Nat st
( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) )
proof end;

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

theorem :: NEWTON02:45
for a, b, c being Nat st a + b divides c & a,c are_coprime holds
a,b are_coprime
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 )
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 )
proof end;

theorem :: NEWTON02:48
for a, b being Nat st a is even & a,b are_coprime holds
a - b,a + b are_coprime
proof end;

theorem :: NEWTON02:49
for a, b being Nat st a,b are_coprime holds
a + b,a * b are_coprime
proof end;

theorem Th50: :: NEWTON02:50
for a, b being Nat st not 3 divides a * b holds
3 divides (a + b) * (a - b)
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 ) )
proof end;

theorem :: NEWTON02:52
for a, b being Nat st b |^ 2 = a * (a - b) holds
( 3 divides a & 3 divides b )
proof end;

theorem :: NEWTON02:53
for a, b being Nat st a,b are_coprime holds
not 3 divides ((a + b) * (a - b)) + (a * b)
proof end;

theorem :: NEWTON02:54
for a, b, n being Nat st a > b & a + b >= 2 |^ (n + 1) holds
a > 2 |^ n
proof end;

theorem Th55: :: NEWTON02:55
for a, b being Nat st a <> b holds
(2 * a) * b < (a |^ 2) + (b |^ 2)
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))
proof end;

theorem :: NEWTON02:57
for b being Nat st b > 0 holds
ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) )
proof end;

:: division by 4
theorem Th58: :: NEWTON02:58
for a, b being odd Nat holds
( 4 divides a + b iff not 4 divides a - b )
proof end;

theorem :: NEWTON02:59
for b, c being Nat st (b + c) gcd b = 1 & c is odd holds
((2 * b) + c) gcd c = 1
proof end;

theorem :: NEWTON02:60
for a, b, k being Nat st a + b = (k * a) + (k * b) & a * b > 0 holds
k = 1
proof end;

theorem :: NEWTON02:61
for t, z being Integer st t * z = t + z holds
t = z
proof end;

theorem Th62: :: NEWTON02:62
for n being Nat holds ((2 * n) + 1) |^ 2 = ((4 * n) * (n + 1)) + 1
proof end;

theorem :: NEWTON02:63
for a, b being Nat st a is odd & b is odd holds
8 divides (a |^ 2) - (b |^ 2)
proof end;

Lm60: for a, b, m being odd Nat st 4 divides a + b holds
4 divides (a |^ m) + (b |^ m)
proof end;

theorem Th64: :: NEWTON02:64
for n being Nat
for a, b being odd Nat st 4 divides a - b holds
4 divides (a |^ n) - (b |^ n)
proof end;

theorem Th65: :: NEWTON02:65
for a, b being odd Nat
for m being even Nat 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 )
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 Th67: :: NEWTON02:67
for a, b, n being Nat st a is odd & 2 |^ n divides a * b holds
2 |^ n divides b
proof end;

theorem Th68: :: NEWTON02:68
for a, b, m being odd Nat holds
( 4 divides (a |^ m) + (b |^ m) iff 4 divides a + b )
proof end;

theorem :: NEWTON02:69
for a, b, m being odd Nat holds
( 4 divides a - b iff not 4 divides (a |^ m) + (b |^ m) )
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
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
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 :: NEWTON02:72
for a, b, c, m being Nat st a is odd & b is odd & m is even holds
(a |^ m) + (b |^ m) <> c |^ m
proof end;

theorem Th73: :: NEWTON02:73
for n being Nat
for t, z being Integer st t,z |^ n are_coprime & n > 0 holds
t,z are_coprime
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
proof end;

theorem :: NEWTON02:75
for a, b being Nat st a,b are_coprime holds
a + b,((a |^ 2) + (b |^ 2)) + (a * b) are_coprime
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
proof end;

theorem Th77: :: NEWTON02:77
for a, n, k being Nat holds
( a divides k * ((a * n) + 1) iff a divides k )
proof end;

theorem :: NEWTON02:78
for a, k being Nat
for n being positive Nat holds
( a divides k * ((a |^ n) + 1) iff a divides k )
proof end;

theorem :: NEWTON02:79
for a, b being positive Nat st a mod b = b mod a holds
a = b
proof end;

theorem Th80: :: NEWTON02:80
for a, n, k being Nat holds (k * ((a * n) + 1)) mod a = k mod a
proof end;

theorem Th81: :: NEWTON02:81
for a, k being Nat
for n being positive Nat holds (k * ((a |^ n) + 1)) mod a = k mod a
proof end;

theorem Th82: :: NEWTON02:82
for a, m, k being Nat
for n being positive Nat holds (k * (((a |^ n) + 1) |^ m)) mod a = k mod a
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
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 )
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.| )
proof end;

theorem :: NEWTON02:86
for a being Nat
for t, u being Integer holds (- t) mod a = ((u * a) - (t mod a)) mod a
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;

theorem Th87: :: NEWTON02:87
for t being Integer
for n being odd Nat holds (t |^ n) mod 3 = t mod 3
proof end;

theorem Th88: :: NEWTON02:88
for t, u, z being Integer holds (t + (u mod z)) mod z = (t + u) mod z
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
proof end;

theorem Th90: :: NEWTON02:90
for t being Integer
for k being positive Nat holds
( t mod k = k - 1 iff (t + 1) mod k = 0 )
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:91
for a, b, c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 holds
3 divides (a * b) * c
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
proof end;

theorem :: NEWTON02:93
for n being Nat
for t, z being Integer st 3 divides t - z holds
3 divides (t |^ n) - (z |^ n)
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) )
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:97
for a being Nat holds 6 divides (a |^ 3) - a
proof end;

theorem :: NEWTON02:98
for t being Integer
for a, b, c being odd Nat holds 3 divides ((t |^ a) + (t |^ b)) + (t |^ c)
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 )
proof end;

theorem Th100: :: NEWTON02:100
for t, u, z being Integer st (u + t) + z is even holds
(u * t) * z is even
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
proof end;

theorem :: NEWTON02:102
for m, n being Nat
for t being Integer holds t |^ n,t |^ m are_congruent_mod t - 1
proof end;

theorem Th1: :: NEWTON02:103
for D being set
for f being FinSequence holds
( f is D -valued iff f is FinSequence of D )
proof end;

:: Seg vs Segm
theorem Th2: :: NEWTON02:104
for n, k being Nat holds
( k + 1 in Seg n iff k < n )
proof end;

theorem Th3: :: NEWTON02:105
for n being Nat
for f being FinSequence of REAL holds
( n + 1 <= len f iff n + 1 in dom f )
proof end;

theorem :: NEWTON02:106
for n, k being Nat holds
( k in Segm n iff k + 1 in Seg n ) by Th2, NAT_1:44;

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

theorem Th9: :: NEWTON02:109
for n being Nat
for f being FinSequence of REAL st n in dom f holds
(f | n) . 1 = f . 1
proof end;

theorem Th10: :: NEWTON02:110
for n being Nat
for f being FinSequence of REAL st n in dom f holds
len (f | n) = n
proof end;

registration
let s be real number ;
cluster <*s*> -> REAL -valued ;
coherence
<*s*> is REAL -valued by TOPREALC:19;
end;

registration
let D be set ;
let f be D -valued FinSequence;
let n be Nat;
cluster f | n -> D -valued ;
coherence
f | n is D -valued ;
end;

registration
let D be set ;
let f be FinSequence of D;
let n be Nat;
cluster f /^ n -> D -valued ;
coherence
f /^ n is D -valued ;
end;

theorem :: NEWTON02:111
for n, k being Nat
for f being FinSequence of COMPLEX st k in dom (f | n) holds
k in dom f
proof end;

registration
let n be Nat;
cluster {} /^ n -> empty ;
coherence
{} /^ n is empty
proof end;
end;

registration
let f be FinSequence of REAL ;
let n be Nat;
cluster (f | n) /^ n -> empty ;
coherence
(f | n) /^ n is empty
proof end;
end;

registration
let D be set ;
let f be D -valued FinSequence;
let n be Nat;
cluster f /^ n -> D -valued ;
coherence
f /^ n is D -valued
proof end;
end;

registration
let f be FinSequence of NAT ;
let n be Nat;
cluster f . n -> natural ;
coherence
f . n is natural ;
end;

registration
let f be FinSequence of NAT ;
let n, k be Nat;
cluster (f | n) . k -> natural ;
coherence
(f | n) . k is natural ;
cluster ((f | n) /^ 1) . k -> natural ;
coherence
((f | n) /^ 1) . k is natural ;
end;

theorem Th14: :: NEWTON02:112
for f, F being FinSequence of REAL holds Sum (f ^ F) = (Sum f) + (Sum F)
proof end;

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

theorem :: NEWTON02:116
for n being Nat
for f being FinSequence of REAL st n + 1 = len f holds
f /^ n = <*(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
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
proof end;

:: n choose k
theorem Th21: :: NEWTON02:119
for n, k being Nat st n is prime & k <> 0 & k <> n holds
n divides n choose k
proof end;

:: factorial
theorem Th22: :: NEWTON02:120
for b being Nat st b >= 2 holds
(b + 1) ! > 2 |^ b
proof end;

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 Th23: :: NEWTON02:121
for b being Nat holds
( b > 1 iff b ! > 1 )
proof end;

theorem Th24: :: NEWTON02:122
for b being Nat st b >= 2 holds
b ! < b |^ b
proof end;

theorem :: NEWTON02:123
for b being Nat holds (b + 1) ! >= 2 |^ b
proof end;

theorem :: NEWTON02:124
for b being Nat holds b ! <= b |^ b
proof end;

theorem :: NEWTON02:125
for a, b being Nat st b > 0 & a,b ! are_coprime holds
a,b are_coprime
proof end;

theorem :: NEWTON02:126
for a, b being Nat holds
( not a,(a + b) ! are_coprime or a = 1 or ( a = 0 & ( b = 0 or b = 1 ) ) )
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)
proof end;

:: Newton_Coeff
registration
let n be Nat;
cluster Newton_Coeff n -> non empty ;
coherence
not Newton_Coeff n is empty
proof end;
end;

registration
let n, m be Nat;
cluster (Newton_Coeff n) . m -> natural ;
coherence
(Newton_Coeff n) . m is natural
proof end;
end;

registration
let n be Nat;
cluster Newton_Coeff n -> NAT -valued ;
coherence
Newton_Coeff n is NAT -valued
proof end;
end;

registration
let h be FinSequence of NAT ;
cluster Sum h -> natural ;
coherence
Sum h is natural
proof end;
end;

theorem Th30: :: NEWTON02:128
for n being Nat st n > 0 holds
n in dom (Newton_Coeff n)
proof end;

theorem :: NEWTON02:129
for n being Nat holds Newton_Coeff n is FinSequence of NAT
proof end;

theorem Th32: :: NEWTON02:130
for n being Nat holds (Newton_Coeff n) . (n + 1) = 1
proof end;

theorem Th33: :: NEWTON02:131
for k being Nat holds (Newton_Coeff k) . 1 = 1
proof 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 Th35: :: NEWTON02:133
for n being positive Nat holds Sum (Newton_Coeff n) = (Sum (((Newton_Coeff n) | n) /^ 1)) + 2
proof end;

theorem :: NEWTON02:134
for n being Nat holds Sum (Newton_Coeff n) = (Sum ((Newton_Coeff n) | n)) + 1
proof end;

theorem :: NEWTON02:135
for n being Nat holds len ((Newton_Coeff n) | n) = n
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)
proof end;

theorem Th39: :: NEWTON02:137
for n, k being Nat st n is prime holds
n divides (((Newton_Coeff n) | n) /^ 1) . k
proof end;

theorem Th40: :: NEWTON02:138
for n being prime Nat holds n divides (2 |^ n) - 2
proof end;

registration
let k be positive Nat;
let n be Nat;
cluster (n |^ k) - n -> natural ;
coherence
(n |^ k) - n is natural
proof end;
end;

theorem :: NEWTON02:139
for k, n being prime Nat holds n * k divides ((2 |^ n) - 2) * ((2 |^ k) - 2)
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 )
proof end;

definition
let n be natural number ;
func n \ -> FinSequence of REAL equals :: NEWTON02:def 1
(1,1) In_Power n;
coherence
(1,1) In_Power n is FinSequence of REAL ;
end;

:: deftheorem defines \ NEWTON02:def 1 :
for n being natural number holds n \ = (1,1) In_Power n;

registration
let n be Nat;
identify n \ with Newton_Coeff n;
correctness
compatibility
n \ = Newton_Coeff n;
by NEWTON:31;
identify Newton_Coeff n with n \ ;
correctness
compatibility
Newton_Coeff n = n \ ;
;
end;

:: The use of this registration would make most of the above code unnecessary. I leave it as an illustration.
:: In_Power
theorem Th43: :: NEWTON02:141
for a, b, n being Nat st n > 0 holds
n in dom ((a,b) In_Power n)
proof end;

registration
let a, b, n, m be Nat;
cluster ((a,b) In_Power n) . m -> natural ;
coherence
((a,b) In_Power n) . m is natural
proof end;
end;

registration
let a, b, n be Nat;
cluster (a,b) In_Power n -> NAT -valued ;
coherence
(a,b) In_Power n is NAT -valued
proof end;
end;

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)
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 Th45: :: NEWTON02:143
for a, b, m being Nat st a <> 0 holds
((a,b) In_Power m) . 1 <> 0
proof end;

theorem :: NEWTON02:144
for a, b being Nat
for m being non zero Nat holds
( a = 0 iff ((a,b) In_Power m) . 1 = 0 )
proof end;

theorem :: NEWTON02:145
for a, b, m being Nat st ((a,b) In_Power m) . 1 = 0 holds
m <> 0
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))
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
proof end;

theorem :: NEWTON02:149
for a, b, m being Nat st m > 0 holds
ex k being Nat st ((a,b) In_Power m) . 1 = a * k
proof end;

theorem :: NEWTON02:150
for a, b, k, l being Nat st l > 0 holds
ex x being Nat st ((a,b) In_Power (k + l)) . l = a * x
proof end;

theorem :: NEWTON02:151
for a, b, k, l, n being Nat st n = ((a,b) In_Power (k + l)) . (k + 1) & l > 0 holds
a divides n
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
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))
proof end;

theorem Th56: :: NEWTON02:154
for a being Nat
for n being prime Nat holds n * a divides ((a + 1) |^ n) - ((a |^ n) + 1)
proof end;

theorem :: NEWTON02:155
for a, b being positive Nat holds (2 * a) * b divides ((a + b) |^ 2) - ((a |^ 2) + (b |^ 2)) by Th55, INT_2:28;

theorem Th58: :: NEWTON02:156
for a being Nat
for n being prime Nat holds n divides (a |^ n) - a
proof end;

theorem Th59: :: NEWTON02:157
for a, k being Nat st k + 1 is prime & not k + 1 divides a holds
k + 1 divides (a |^ k) - 1
proof end;

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

theorem :: NEWTON02:159
for a, b being Nat holds
( 163 divides a + b iff 163 divides (a |^ 163) + (b |^ 163) ) by NAT_4:35, Th60;

theorem Th62: :: NEWTON02:160
for a being Nat
for n being prime Nat holds
( n divides a iff n divides a |^ n )
proof end;

theorem Th63: :: NEWTON02:161
for a being Nat
for n being prime Nat holds
( n divides (a |^ n) + 1 iff n divides a + 1 )
proof end;

theorem :: NEWTON02:162
for a, b being Nat
for n being prime Nat holds
( n divides (a |^ n) + (b |^ n) iff n divides (a + b) |^ n ) by Th60, Th62;

theorem :: NEWTON02:163
for a being Nat holds
( 7 divides (a |^ 7) + 1 iff 7 divides a + 1 ) by Th63, NAT_4:26;

theorem :: NEWTON02:164
for a being Nat st not 7 divides a holds
7 divides (a |^ 6) - 1
proof end;

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

theorem :: NEWTON02:170
for a being Nat holds
( 5 divides (a |^ 3) - 1 iff 5 divides a - 1 )
proof end;

theorem Th73: :: NEWTON02:171
for a, n, k being Nat st k + 1 is prime holds
k + 1 divides (a |^ ((n * k) + 1)) - a
proof end;

theorem Th74: :: NEWTON02:172
for a, n being Nat holds 2 divides (a |^ (n + 1)) - a
proof end;

theorem Th75: :: NEWTON02:173
for a, n being Nat holds 3 divides (a |^ ((2 * n) + 1)) - a
proof end;

theorem Th76: :: NEWTON02:174
for a, n being Nat holds 5 divides (a |^ ((4 * n) + 1)) - a
proof end;

theorem Th77: :: NEWTON02:175
for a, n being Nat holds 7 divides (a |^ ((6 * n) + 1)) - a
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
proof end;

theorem :: NEWTON02:177
for a being Nat holds 154 divides (a |^ 61) - a
proof end;

theorem :: NEWTON02:178
for a, n being Nat holds 6 divides (a |^ ((2 * n) + 1)) - a
proof end;

theorem :: NEWTON02:179
for a, n being Nat holds 30 divides (a |^ ((4 * n) + 1)) - a
proof end;

theorem :: NEWTON02:180
for a, n being Nat holds 42 divides (a |^ ((6 * n) + 1)) - a
proof end;

theorem :: NEWTON02:181
for a, k being Nat
for n being prime Nat holds n divides (a |^ (n + k)) - (a |^ (k + 1))
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 )
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 )
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 )
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 )
proof end;

theorem Th88: :: NEWTON02:186
for n being Nat holds
( 2 divides (2 |^ n) - 1 iff n = 0 )
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 )
proof end;

theorem Th90: :: NEWTON02:188
for b being Nat holds
( 3 divides b or 3 divides b - 1 or 3 divides b + 1 )
proof end;

theorem Th91: :: NEWTON02:189
for b, c being Nat st not 3 divides b holds
not 3 divides (b |^ 2) + (c |^ 2)
proof end;

theorem Th92: :: NEWTON02:190
for b being Nat holds
( not 3 divides (b |^ 2) + 1 & not 3 divides (b |^ 2) - 2 )
proof end;

theorem :: NEWTON02:191
for b being Nat holds not 3 divides (((b |^ 3) + (b |^ 2)) - b) + 1
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
proof end;

theorem Th95: :: NEWTON02:193
for b, c being Nat st b,c are_coprime holds
not 3 divides (b |^ 2) + (c |^ 2)
proof end;

theorem Th96: :: NEWTON02:194
for a, n being Nat
for p being prime Nat st p divides a holds
p divides a |^ (n + 1)
proof end;

theorem :: NEWTON02:195
for a, b, c being Nat st b,c are_coprime & (b |^ 2) + (c |^ 2) = a |^ 2 holds
not 3 divides a
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))
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
proof end;

theorem :: NEWTON02:198
for a, b being Nat holds
( 3 divides a * b or 3 divides a + b or 3 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))
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 )
proof end;