:: Some Remarkable Identities Involving Numbers
:: by Rafa{\l} Ziobro
::
:: Received September 5, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


registration
let u, v be even Integer;
cluster u - v -> even ;
coherence
u - v is even
proof end;
end;

registration
let u be odd Integer;
let k be Nat;
cluster u |^ k -> odd ;
coherence
not u |^ k is even
proof end;
end;

registration
let k be positive Nat;
let u be even Integer;
cluster u |^ k -> even ;
coherence
u |^ k is even
proof end;
end;

Lm10: for a1, b1 being Complex holds (a1 + b1) |^ 2 = ((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2)
proof end;

theorem Th1: :: NEWTON01:1
for a1, b1 being Complex holds (a1 |^ 2) - (b1 |^ 2) = (a1 - b1) * (a1 + b1)
proof end;

theorem Th2: :: NEWTON01:2
for a1 being Complex holds (((2 * a1) + 1) |^ 2) + (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) = (((2 * (a1 |^ 2)) + (2 * a1)) + 1) |^ 2
proof end;

theorem :: NEWTON01:3
for a1, b1 being Complex holds ((a1 |^ 2) + (a1 * b1)) + (b1 |^ 2) = ((3 * ((a1 + b1) |^ 2)) + ((a1 - b1) |^ 2)) / 4
proof end;

theorem :: NEWTON01:4
for a being Nat st a is odd holds
ex b being Nat st (a |^ 2) + (b |^ 2) = (b + 1) |^ 2
proof end;

theorem Th5: :: NEWTON01:5
for m, n being Nat
for a1, b1 being Complex holds ((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) - (b1 |^ n))) + (((a1 |^ n) + (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2 = (a1 |^ (m + n)) - (b1 |^ (m + n))
proof end;

Lm0: for a, b, c being Nat holds (a |^ 0) + (b |^ 0) > c |^ 0
proof end;

theorem Th6: :: NEWTON01:6
for a, b, c, m being Nat st (a |^ m) + (b |^ m) <= c |^ m holds
a <= c
proof end;

theorem :: NEWTON01:7
for n being Nat
for a1, b1, c1 being Complex st (a1 + b1) |^ (n + 1) = ((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1) holds
(a1 + b1) |^ (n + 2) = ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1))))
proof end;

theorem Th8: :: NEWTON01:8
for m, n being Nat
for a1, b1 being Complex holds ((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) + (b1 |^ n))) + (((a1 |^ n) - (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2 = (a1 |^ (m + n)) + (b1 |^ (m + n))
proof end;

Lm3a: for a, b, n being Nat st a <= b holds
a |^ n <= b |^ n
proof end;

Lm4a: for a, b, n being Nat st a |^ n > b |^ n holds
a |^ (n + 1) > b |^ (n + 1)
proof end;

Lm5c: for a, b, m being Nat st b > 0 holds
a < a + (b |^ m)
proof end;

Lm5d: for a, b, x, m being Nat st (a + x) |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 holds
x > 0
proof end;

theorem Th9: :: NEWTON01:9
for m being Nat
for a1, b1 being Complex holds (a1 |^ (m + 1)) + (b1 |^ (m + 1)) = ((((a1 |^ m) + (b1 |^ m)) * (a1 + b1)) + ((a1 - b1) * ((a1 |^ m) - (b1 |^ m)))) / 2
proof end;

theorem Th10: :: NEWTON01:10
for a, b, m being Nat holds (a - b) * ((a |^ m) - (b |^ m)) >= 0
proof end;

theorem :: NEWTON01:11
for a, b, m being Nat holds (a |^ (m + 1)) + (b |^ (m + 1)) >= (((a |^ m) + (b |^ m)) * (a + b)) / 2
proof end;

theorem :: NEWTON01:12
for a, b, c, m being Nat st (a |^ m) + (b |^ m) <= c |^ m holds
ex x being Nat st (a |^ m) + (b |^ m) <= (a + x) |^ m
proof end;

theorem Th13: :: NEWTON01:13
for m being Nat
for a1, b1 being Complex holds (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 |^ m) - (b1 |^ m)))) / 2
proof end;

Lm16: for m being Nat
for t being Integer
for a1, b1 being Complex st (a1 |^ m) - (b1 |^ m) = (a1 - b1) * t holds
(a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2
proof end;

Lm17: for m being Nat
for t being Integer
for a1, b1 being Complex st (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2 & a1 + b1 <> 0 holds
(a1 |^ m) - (b1 |^ m) = (a1 - b1) * t
proof end;

theorem Th14: :: NEWTON01:14
for a, b, m being Nat
for t being Integer holds
( (a |^ (m + 1)) - (b |^ (m + 1)) = ((a - b) * (((t * (a + b)) + (a |^ m)) + (b |^ m))) / 2 iff (a |^ m) - (b |^ m) = (a - b) * t )
proof end;

theorem :: NEWTON01:15
for n being Nat
for c1 being Complex holds ((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) = c1 |^ (n + 1)
proof end;

Lm18d: for n being Nat
for u, v being Integer st n > 0 & u - v is odd holds
( u + v is odd & (u |^ n) - (v |^ n) is odd & (u |^ n) + (v |^ n) is odd )
proof end;

Lm18e: for n being Nat
for u, v being Integer st u - v is even holds
( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
proof end;

theorem :: NEWTON01:16
for a, b being Nat holds (a |^ 3) - (b |^ 3) = ((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2
proof end;

theorem Th17: :: NEWTON01:17
for a, b, c, m being Nat st c |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 holds
c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))
proof end;

theorem Th18: :: NEWTON01:18
for a, b, c, k, m being Nat st c |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 & k > 0 holds
c |^ (k + m) > (a |^ (k + m)) + (b |^ (k + m))
proof end;

theorem :: NEWTON01:19
for a, b, c, k, m being Nat st c |^ m >= (a |^ m) + (b |^ m) holds
c |^ (k + m) >= (a |^ (k + m)) + (b |^ (k + m))
proof end;

Lm28: for a, b, c, m being Nat st c |^ m > (a |^ m) + (b |^ m) & a > 0 holds
c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))
proof end;

Lm29: for a, b, c, m being Nat st c |^ m > (a |^ m) + (b |^ m) holds
c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))
proof end;

theorem :: NEWTON01:20
for a, b, c, k, n being Nat st c |^ n > (a |^ n) + (b |^ n) holds
c |^ (k + n) > (a |^ (k + n)) + (b |^ (k + n))
proof end;

theorem Th21: :: NEWTON01:21
for m being Nat
for a1, b1 being Complex holds (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))
proof end;

theorem :: NEWTON01:22
for m being Nat
for a1, b1 being Complex holds (a1 |^ (m + 2)) + (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) - (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) + (b1 |^ m)))
proof end;

theorem :: NEWTON01:23
for a, b, c, m being Nat holds
( (a |^ ((2 * m) + 2)) - (b |^ ((2 * m) + 2)) = (((a |^ 2) - (b |^ 2)) * (((c * ((a |^ 2) + (b |^ 2))) + (a |^ (2 * m))) + (b |^ (2 * m)))) / 2 iff (a |^ (2 * m)) - (b |^ (2 * m)) = ((a |^ 2) - (b |^ 2)) * c )
proof end;

theorem :: NEWTON01:24
for m being Nat
for a1, b1 being Complex holds (a1 |^ ((2 * m) + 3)) + (b1 |^ ((2 * m) + 3)) = (((a1 |^ ((2 * m) + 2)) + (b1 |^ ((2 * m) + 2))) * (a1 + b1)) - ((a1 * b1) * ((a1 |^ ((2 * m) + 1)) + (b1 |^ ((2 * m) + 1))))
proof end;

theorem :: NEWTON01:25
for k, m being Nat
for a1, b1 being Complex st (a1 |^ m) - (b1 |^ m) = (a1 - b1) * k holds
(a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1)
proof end;

theorem :: NEWTON01:26
for k, m being Nat
for a1, b1 being Complex st (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1) & a1 * b1 <> 0 holds
(a1 |^ m) - (b1 |^ m) = (a1 - b1) * k
proof end;

Lm56a: for a, b, n being Nat st n > 1 & b > 0 & a > b holds
((a |^ n) + (b |^ n)) * (a - b) < (a |^ (n + 1)) - (b |^ (n + 1))
proof end;

Lm57: for a, b, n being Nat st n > 0 & a > b holds
((a |^ n) - (b |^ n)) * (a + b) >= (a |^ (n + 1)) - (b |^ (n + 1))
proof end;

Lm57d: for a, b, n being Nat st b > 0 & a > b & ((a |^ n) - (b |^ n)) * (a + b) = ((a |^ n) + (b |^ n)) * (a - b) holds
n = 1
proof end;

theorem :: NEWTON01:27
for a, b, n being Nat st b > 0 & a > b holds
( ((a |^ n) - (b |^ n)) * (a + b) = ((a |^ n) + (b |^ n)) * (a - b) iff n = 1 ) by Lm57d;

theorem :: NEWTON01:28
for a, b, n being Nat st n > 1 & b > 0 & a > b holds
((a |^ n) - (b |^ n)) * (a + b) > (a |^ (n + 1)) - (b |^ (n + 1))
proof end;

theorem :: NEWTON01:29
for a, b, n being Nat st n > 0 & a > b holds
((a |^ n) + (b |^ n)) * (a - b) <= (a |^ (n + 1)) - (b |^ (n + 1))
proof end;

Lm18b: for a, b being Nat holds a - b divides (a |^ 0) - (b |^ 0)
proof end;

Lm18f: for a, b, n being Nat st n > 0 & a - b divides (a |^ n) - (b |^ n) holds
a - b divides (a |^ (n + 1)) - (b |^ (n + 1))
proof end;

Lm46: for a, m being Nat st m > 0 holds
2 * a divides (a |^ m) + (a |^ m)
proof end;

theorem Th29: :: NEWTON01:30
for p, q, z, u, v being Integer st p + q divides (p * u) + (q * v) holds
p + q divides (p * (u + z)) + (q * (v + z))
proof end;

theorem :: NEWTON01:31
for p, q, t, z being Integer holds p + q divides (p * ((t * (p + q)) + z)) + (q * z)
proof end;

theorem Th31: :: NEWTON01:32
for p, q, t, u, v being Integer st p + q divides u - v holds
p + q divides (p * (u + t)) + (q * (v + t))
proof end;

theorem Th32: :: NEWTON01:33
for a, b, n being Nat holds a - b divides (a |^ n) - (b |^ n)
proof end;

theorem Th33: :: NEWTON01:34
for a, b, m being Nat holds (a |^ 2) - (b |^ 2) divides (a |^ (2 * m)) - (b |^ (2 * m))
proof end;

theorem Th34: :: NEWTON01:35
for a, b, m being Nat holds a + b divides (a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))
proof end;

Lm44: for a, b being Nat holds a + b divides (a |^ 2) - (b |^ 2)
proof end;

theorem :: NEWTON01:36
for a, b, m being Nat holds a + b divides (a |^ (2 * m)) - (b |^ (2 * m))
proof end;

theorem :: NEWTON01:37
for a, b, n being Nat st a + b divides (a |^ n) - (b |^ n) holds
a + b divides (a |^ (n + 1)) + (b |^ (n + 1))
proof end;

theorem :: NEWTON01:38
for a, b, n being Nat holds
( a + b divides (a |^ n) + (b |^ n) or a + b divides (a |^ n) - (b |^ n) )
proof end;

theorem :: NEWTON01:39
for a, b, c, n being Nat st a >= b & (c |^ n) - (b |^ n) = a |^ n holds
( (c - b) gcd (a |^ n) = c - b & (c - a) gcd (b |^ n) = c - a )
proof end;

theorem :: NEWTON01:40
for a, b, c, d being Nat st a,b are_coprime & a + b divides (a * c) + (b * d) holds
a + b divides c - d
proof end;

theorem Th40: :: NEWTON01:41
for a, b, c, d being Nat st a * b,c * d are_coprime holds
a,c are_coprime
proof end;

Lm53: for a, b, k, m being Nat st a |^ (k + 1),b |^ (m + 1) are_coprime holds
a,b are_coprime
proof end;

Lm58: for a, b, c, n being Nat st a > 0 & b > 0 & (a |^ n) + (b |^ n) = c |^ n holds
ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l )
proof end;

Lm59: for j, k, l, m being Nat st (j |^ (m + 1)) + (k |^ (m + 1)) = l |^ (m + 1) & j,k are_coprime holds
j,l are_coprime
proof end;

theorem Th41: :: NEWTON01:42
for a, b, c, n being Nat st a > 0 & b > 0 & (a |^ n) + (b |^ n) = c |^ n holds
ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & j,l are_coprime & k,l are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l )
proof end;

Lm60: for a, b, n being Nat st a = 1 holds
(a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2)
proof end;

theorem :: NEWTON01:43
for a, b, n being Nat st a > 0 holds
(a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2)
proof end;

Lm61: for a1, b1, c1, d1 being Complex st a1 + (b1 |^ 2) = c1 |^ 2 holds
(a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2) = (2 * d1) * (b1 - c1)
proof end;

theorem :: NEWTON01:44
for a, b, c, x being Nat st x > 0 & b < c & a + (b |^ 2) = c |^ 2 holds
a + ((b + x) |^ 2) < (c + x) |^ 2
proof end;

theorem Th44: :: NEWTON01:45
for a, b, c being Nat
for q being Integer st q < 0 & b < c & (a |^ 2) + (b |^ 2) = c |^ 2 holds
(a |^ 2) + ((b + q) |^ 2) > (c + q) |^ 2
proof end;

theorem :: NEWTON01:46
for a, b, x being Nat st x > 0 & (a |^ 2) + (b |^ 2) = (b + 1) |^ 2 holds
(a |^ 2) + ((b - x) |^ 2) > ((b + 1) - x) |^ 2
proof end;

theorem Th46: :: NEWTON01:47
for a, x being Nat st a >= 1 & ((a + 1) |^ 2) + (((a + 1) + x) |^ 2) <= (((a + 1) + x) + 1) |^ 2 holds
(a |^ 2) + ((a + x) |^ 2) < ((a + x) + 1) |^ 2
proof end;

theorem Th47: :: NEWTON01:48
for a, x, l being Nat st a >= 1 & (a |^ 2) + ((a + x) |^ 2) >= ((a + x) + 1) |^ 2 holds
(((a + l) + 1) |^ 2) + ((((a + l) + 1) + x) |^ 2) > ((((a + l) + 1) + x) + 1) |^ 2
proof end;

Lm120: for a being Nat st (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 holds
a >= 3
proof end;

theorem :: NEWTON01:49
for a being Nat holds
( a >= 3 iff (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 )
proof end;

theorem :: NEWTON01:50
for m being Nat holds (2 |^ (3 + m)) + (2 |^ (3 + m)) < 3 |^ (3 + m)
proof end;