:: Elementary Number Theory Problems. {P}art {XII}
:: by Adam Grabowski
::
:: Received December 18, 2023
:: Copyright (c) 2023-2024 Association of Mizar Users


theorem SetFor10: :: NUMBER12:1
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10}
proof end;

registration
let m be composite Nat;
let n be non zero Nat;
cluster m * n -> composite ;
coherence
m * n is composite
proof end;
end;

registration
let m, n be non trivial non zero Nat;
cluster m * n -> composite ;
coherence
m * n is composite
proof end;
end;

registration
let r be Real;
cluster r |^ 2 -> non negative ;
coherence
not r |^ 2 is negative
proof end;
end;

registration
let k be Nat;
let n be non trivial non zero Nat;
cluster k + n -> non trivial non zero ;
coherence
( not k + n is trivial & not k + n is zero )
proof end;
end;

registration
let k be Nat;
cluster k + 1 -> non zero ;
coherence
not k + 1 is zero ;
cluster k + 2 -> non trivial non zero ;
coherence
( not k + 2 is trivial & not k + 2 is zero )
proof end;
cluster k + 3 -> non trivial non zero ;
coherence
( not k + 3 is trivial & not k + 3 is zero )
proof end;
end;

theorem Mod22: :: NUMBER12:2
for n being Nat st n mod 11 = 1 & n mod 2 = 1 holds
n mod 22 = 1
proof end;

:: Formalization of Sierpinski Theorem on the
:: Divisors in the Progression of Primes
theorem SierpinskiTh5: :: NUMBER12:3
for m, n, r being Nat st n > 1 & ( for i being Nat st 0 <= i & i < n holds
( (ArProg (m,r)) . i is odd & (ArProg (m,r)) . i is prime ) ) holds
for p being Prime st p < n holds
p divides r
proof end;

:: Prove that there exists an increasing infinite sequence of triangular
:: numbers (i.e. numbers of the form t_n = 1/2 n(n+1), n = 1, 2, ... )
:: such that every two of them are relatively prime.
theorem CoprimeDivides: :: NUMBER12:4
for a, m, n being Nat st a,m are_coprime & n divides a holds
n,m are_coprime
proof end;

theorem Coprime21: :: NUMBER12:5
for a being Nat holds a,(2 * a) + 1 are_coprime
proof end;

theorem Coprime61: :: NUMBER12:6
for a being Nat holds a,(6 * a) + 1 are_coprime
proof end;

theorem Coprime31: :: NUMBER12:7
for a being Nat holds a,(3 * a) + 1 are_coprime
proof end;

theorem ConcatIsIncreasing: :: NUMBER12:8
for f being increasing FinSequence of NAT
for x being Nat st ( for i being Nat st i in dom f holds
f . i < x ) holds
f ^ <*x*> is increasing
proof end;

theorem IncFinNAT: :: NUMBER12:9
for n being Nat holds (Seg 1) --> n is increasing FinSequence of NAT
proof end;

theorem :: NUMBER12:10
for n being Nat ex f being non-empty increasing FinSequence of NAT st
( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms )
proof end;

:: Prove that there exists an increasing infinite sequence of tetrahedral
:: numbers (i.e. numbers of the form T_n = 1/6 n(n+1)(n+2), n = 1, 2, ...),
:: such that every two of them are relatively prime.
definition
let n be Nat;
func Tetrahedron n -> Nat equals :: NUMBER12:def 1
((n * (n + 1)) * (n + 2)) / 6;
coherence
((n * (n + 1)) * (n + 2)) / 6 is Nat
proof end;
end;

:: deftheorem defines Tetrahedron NUMBER12:def 1 :
for n being Nat holds Tetrahedron n = ((n * (n + 1)) * (n + 2)) / 6;

definition
let n be Nat;
attr n is tetrahedral means :: NUMBER12:def 2
 ex k being Nat st n = Tetrahedron k;
end;

:: deftheorem defines tetrahedral NUMBER12:def 2 :
for n being Nat holds
( n is tetrahedral iff ex k being Nat st n = Tetrahedron k );

theorem :: NUMBER12:11
for n being Nat ex f being non-empty increasing FinSequence of NAT st
( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is tetrahedral ) & f is with_all_coprime_terms )
proof end;

:: Prove that (n,2^{2^n} + 1) = 1 for n = 1, 2, ...
theorem T51: :: NUMBER12:12
for n being non zero Nat holds n gcd (Fermat n) = 1
proof end;

theorem :: NUMBER12:13
for n being non zero Nat holds n, Fermat n are_coprime by T51;

:: Prove that there exist infinitely many positive integers n such that
:: (n, 2^n-1) > 1, and find the least of them.
theorem :: NUMBER12:14
for n, k, m being Nat st n divides k * m holds
ex a, b being Nat st
( a divides k & b divides m & n = a * b )
proof end;

theorem :: NUMBER12:15
for A being set st A = { n where n is non zero Nat : n gcd ((2 |^ n) - 1) > 1 } holds
( A is infinite & ( for k being Nat st k in A holds
k >= 6 ) )
proof end;

:: Give a necessary and sufficient condition for an arithmetic progression
:: ak+b (k = 0, 1, 2, ... ) with positive integer a and b to contain
:: infinitely many squares of integers.
theorem :: NUMBER12:16
for a, b being positive Nat
for k, x, m being Nat st (ArProg (b,a)) . k = x ^2 holds
(ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) = ((m * a) + x) ^2
proof end;

theorem Lemma2To57: :: NUMBER12:17
for a, b being positive Nat
for k, x, m being Nat st (ArProg (b,a)) . k = x ^2 holds
(ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) is square
proof end;

theorem LemmaTo57: :: NUMBER12:18
for m, n being non zero Nat st m is_quadratic_residue_mod n holds
ex i being Nat st (ArProg (m,n)) . i is square
proof end;

theorem :: NUMBER12:19
for m, n being non zero Nat
for A being set st A = { i where i is Nat : (ArProg (m,n)) . i is square } holds
( A is infinite iff m is_quadratic_residue_mod n )
proof end;

:: Prove that there is no infinite arithmetic progression formed of
:: different positive integers such that each term is a power of
:: a positive integer with an integer exponent > 1.
theorem SquareNotDiv: :: NUMBER12:20
for k being Nat st k > 1 holds
not k * k divides k
proof end;

registration
cluster Relation-like non-empty NAT -defined REAL -valued Function-like V32( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued increasing AP-like for Element of bool [:NAT,REAL:];
existence
ex b1 being Arithmetic_Progression st
( b1 is non-empty & b1 is natural-valued & b1 is increasing )
proof end;
end;

theorem KeyPerfectPower: :: NUMBER12:21
for n being Nat
for p being Prime st n is perfect_power & p divides n holds
p |^ 2 divides n
proof end;

theorem :: NUMBER12:22
for f being non-empty natural-valued increasing Arithmetic_Progression ex i, fi being Nat st
( fi = f . i & not fi is perfect_power )
proof end;

:: Find an increasing arithmetic progression with ten terms, formed
:: of primes, with the least possible last term.
theorem :: NUMBER12:23
for f being Arithmetic_Progression st ( for i being Nat holds f . i is Prime ) holds
difference f is Integer
proof end;

theorem :: NUMBER12:24
for p, q being Prime holds
( not p - q is odd or p = 2 or q = 2 )
proof end;

registration
let p, q be Prime;
cluster p - q -> integer ;
coherence
p - q is integer ;
end;

registration
let p, q be 2 _greater Prime;
cluster p - q -> even ;
coherence
p - q is even ;
end;

theorem FirstAPPrime: :: NUMBER12:25
for f being increasing Arithmetic_Progression st ( for i being Nat holds f . i is Prime ) holds
f . 1 > 2
proof end;

theorem :: NUMBER12:26
for f being increasing Arithmetic_Progression st ( for i being Nat holds f . i is Prime ) holds
difference f is even Nat
proof end;

theorem Th1990: :: NUMBER12:27
(ArProg (199,210)) . 0 = 199 by NUMBER06:def 4;

theorem Th1991: :: NUMBER12:28
(ArProg (199,210)) . 1 = 409
proof end;

theorem Th1992: :: NUMBER12:29
(ArProg (199,210)) . 2 = 619
proof end;

theorem Th1993: :: NUMBER12:30
(ArProg (199,210)) . 3 = 829
proof end;

theorem Th1994: :: NUMBER12:31
(ArProg (199,210)) . 4 = 1039
proof end;

theorem Th1995: :: NUMBER12:32
(ArProg (199,210)) . 5 = 1249
proof end;

theorem Th1996: :: NUMBER12:33
(ArProg (199,210)) . 6 = 1459
proof end;

theorem Th1997: :: NUMBER12:34
(ArProg (199,210)) . 7 = 1669
proof end;

theorem Th1998: :: NUMBER12:35
(ArProg (199,210)) . 8 = 1879
proof end;

theorem Th1999: :: NUMBER12:36
(ArProg (199,210)) . 9 = 2089
proof end;

:: Hence 2089 is the least possible prime
registration
let f be natural-valued Arithmetic_Progression;
cluster difference f -> integer ;
coherence
difference f is integer
proof end;
end;

theorem Cantor5Div: :: NUMBER12:37
for f being natural-valued increasing Arithmetic_Progression st ( for i being Nat st 0 <= i & i < 10 holds
f . i is odd Prime ) holds
210 divides difference f
proof end;

theorem Cantor5: :: NUMBER12:38
for f being natural-valued increasing Arithmetic_Progression st ( for i being Nat st 0 <= i & i < 10 holds
f . i is odd Prime ) holds
difference f >= 210 by NAT_D:7, Cantor5Div;

theorem Diff210Mod11: :: NUMBER12:39
for f being natural-valued increasing Arithmetic_Progression st ( for i being Nat st 0 <= i & i < 10 holds
f . i is odd Prime ) & difference f = 210 holds
for f0 being Nat st f0 = f . 0 holds
f0 mod 11 = 1
proof end;

theorem Theorem72V1: :: NUMBER12:40
for f being natural-valued increasing Arithmetic_Progression st ( for i being Nat st 0 <= i & i < 10 holds
f . i is odd Prime ) & difference f = 210 holds
f . 0 >= 199
proof end;

theorem :: NUMBER12:41
for f being natural-valued increasing Arithmetic_Progression st ( for i being Nat st 0 <= i & i < 10 holds
f . i is odd Prime ) holds
f . 9 >= 2089
proof end;

theorem RngForArProg: :: NUMBER12:42
rng ((ArProg (199,210)) | 10) = {199,409,619,829,1039,1249,1459,1669,1879,2089}
proof end;

theorem :: NUMBER12:43
card ((rng ((ArProg (199,210)) | 10)) /\ SetPrimes) = 10
proof end;

:: Find all numbers p such that all six numbers p, p+2, p+6, p+8,
:: p+12, and p+14 are primes.
theorem :: NUMBER12:44
for p being Prime st p + 2 is Prime & p + 6 is Prime & p + 8 is Prime & p + 12 is Prime & p + 14 is Prime holds
p = 5
proof end;

:: Prove that there exist infinitely many pairs of different positive
:: integers m and n such that (1) m and n have the same prime divisors, and
:: (2) m + 1 and n + 1 have the same prime divisors.
definition
let n be Integer;
func PrimeDivisors n -> Subset of NAT equals :: NUMBER12:def 3
 { k where k is Prime : k divides n } ;
coherence
{ k where k is Prime : k divides n } is Subset of NAT
proof end;
end;

:: deftheorem defines PrimeDivisors NUMBER12:def 3 :
for n being Integer holds PrimeDivisors n = { k where k is Prime : k divides n } ;

theorem :: NUMBER12:45
for i being Integer holds PrimeDivisors i c= SetPrimes
proof end;

theorem :: NUMBER12:46
for n being non zero Nat holds PrimeDivisors n c= Seg n
proof end;

theorem :: NUMBER12:47
for n being Nat holds PrimeDivisors n c= NatDivisors n
proof end;

theorem DivisorsMulti: :: NUMBER12:48
for a, b being Nat holds PrimeDivisors (a * b) = (PrimeDivisors a) \/ (PrimeDivisors b)
proof end;

LemmaOne: for p being Prime holds PrimeDivisors p = {p}
proof end;

theorem :: NUMBER12:49
for n, a being Nat st n >= 1 holds
PrimeDivisors (a |^ n) = PrimeDivisors a
proof end;

theorem DivK: :: NUMBER12:50
for k being Nat
for p being Prime st k >= 1 holds
PrimeDivisors (p |^ k) = {p}
proof end;

theorem :: NUMBER12:51
PrimeDivisors 1 = {}
proof end;

theorem P136a: :: NUMBER12:52
for k being Nat st k >= 1 holds
PrimeDivisors ((2 |^ k) * ((2 |^ k) - 2)) = {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))
proof end;

theorem P136b: :: NUMBER12:53
for k being Nat st k >= 1 holds
PrimeDivisors ((2 |^ k) - 2) = {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))
proof end;

theorem P136c: :: NUMBER12:54
for k being Nat holds PrimeDivisors (((2 |^ k) * ((2 |^ k) - 2)) + 1) = PrimeDivisors ((2 |^ k) - 1)
proof end;

theorem DivSquare: :: NUMBER12:55
for a being Nat holds PrimeDivisors (a * a) = PrimeDivisors a
proof end;

theorem :: NUMBER12:56
for k, m, n being Nat st k >= 1 & m = (2 |^ k) - 2 & n = (2 |^ k) * ((2 |^ k) - 2) holds
( PrimeDivisors m = PrimeDivisors n & PrimeDivisors (m + 1) = PrimeDivisors (n + 1) )
proof end;

theorem :: NUMBER12:57
( PrimeDivisors 75 = PrimeDivisors 1215 & PrimeDivisors (75 + 1) = PrimeDivisors (1215 + 1) )
proof end;

:: Prove that the equation
:: x / y + y / z + z / x = 1
:: has no solutions in positive integers x, y, z.
theorem Multiply1: :: NUMBER12:58
for x, y, z being positive Real holds ((x / y) * (y / z)) * (z / x) = 1
proof end;

theorem :: NUMBER12:59
for x, y, z being positive Nat holds not ((x / y) + (y / z)) + (z / x) = 1
proof end;

:: Prove that the equation
:: x / y + y / z + z / x = 2
:: has no solutions in positive integers x, y, z.
theorem PositiveRoot: :: NUMBER12:60
for a being positive Real
for n being positive Nat holds n -root a is positive
proof end;

theorem SERIES3: :: NUMBER12:61
for a, b, c being positive Real st ( not a = b or not b = c ) holds
(((a + b) + c) / 3) |^ 3 > (a * b) * c
proof end;

theorem :: NUMBER12:62
for x, y, z being positive Nat holds not ((x / y) + (y / z)) + (z / x) = 2
proof end;

:: Find all solutions in positive integers x, y, z of the equation
:: x / y + y / z + z / x = 3.
theorem :: NUMBER12:63
for x, y, z being positive Nat st ((x / y) + (y / z)) + (z / x) = 3 holds
( x = y & y = z )
proof end;