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