:: Elementary Number Theory Problems. {P}art {VI}
:: by Adam Grabowski
::
:: Received September 30, 2022
:: Copyright (c) 2022-2024 Association of Mizar Users


theorem LemmaDivides: :: NUMBER06:1
for p being Prime st 3 divides p holds
p = 3 by INT_2:def 4;

registration
cluster non empty non trivial epsilon-transitive epsilon-connected ordinal natural non zero complex V20() integer dim-like prime finite cardinal even non square ext-real positive non negative for set ;
existence
ex b1 being Prime st b1 is even
proof end;
end;

theorem :: NUMBER06:2
for p being even Prime holds p = 2 by INT_2:def 4, ABIAN:def 1;

theorem PQCoprime: :: NUMBER06:3
for p, q being Prime st p <> q holds
p,q are_coprime
proof end;

notation
let f be integer-valued Function;
synonym with_all_coprime_terms f for Chinese_Remainder ;
end;

theorem RestrictedXFin: :: NUMBER06:4
for f being sequence of REAL
for n being Nat holds f | n is XFinSequence
proof end;

definition
let f be real-valued Function;
::$CD 1
attr f is AP-like means :APLikeDef: :: NUMBER06:def 2
 for i, k being Nat st i in dom f & i + 1 in dom f & k in dom f & k + 1 in dom f holds
(f . (i + 1)) - (f . i) = (f . (k + 1)) - (f . k);
end;

:: deftheorem NUMBER06:def 1 :
canceled;

:: deftheorem APLikeDef defines AP-like NUMBER06:def 2 :
for f being real-valued Function holds
( f is AP-like iff for i, k being Nat st i in dom f & i + 1 in dom f & k in dom f & k + 1 in dom f holds
(f . (i + 1)) - (f . i) = (f . (k + 1)) - (f . k) );

definition
let f be real-valued FinSequence;
attr f is fAP-like means :: NUMBER06:def 3
 for i being Nat st i in dom f & i + 1 in dom f & i + 2 in dom f holds
(f . (i + 2)) - (f . (i + 1)) = (f . (i + 1)) - (f . i);
end;

:: deftheorem defines fAP-like NUMBER06:def 3 :
for f being real-valued FinSequence holds
( f is fAP-like iff for i being Nat st i in dom f & i + 1 in dom f & i + 2 in dom f holds
(f . (i + 2)) - (f . (i + 1)) = (f . (i + 1)) - (f . i) );

registration
cluster Relation-like Function-like constant FinSequence-like real-valued -> real-valued fAP-like for set ;
coherence
for b1 being real-valued FinSequence st b1 is constant holds
b1 is fAP-like
proof end;
end;

registration
cluster Function-like constant V45( omega , REAL ) -> AP-like for Element of bool [:omega,REAL:];
coherence
for b1 being sequence of REAL st b1 is constant holds
b1 is AP-like
proof end;
end;

registration
cluster id NAT -> AP-like ;
coherence
id NAT is AP-like
proof end;
end;

registration
cluster id REAL -> AP-like ;
coherence
id REAL is AP-like
proof end;
end;

registration
cluster Relation-like omega -defined REAL -valued non empty Function-like V44( omega ) V45( omega , REAL ) complex-valued ext-real-valued real-valued AP-like for Element of bool [:omega,REAL:];
existence
ex b1 being sequence of REAL st b1 is AP-like
proof end;
end;

:: if not constant, it should be either increasing or decreasing
registration
cluster Relation-like REAL -valued Function-like complex-valued ext-real-valued real-valued AP-like for set ;
existence
ex b1 being real-valued Function st b1 is AP-like
proof end;
end;

registration
cluster Relation-like INT -valued Sequence-like Function-like finite complex-valued ext-real-valued real-valued rational-valued integer-valued AP-like for set ;
existence
ex b1 being real-valued integer-valued XFinSequence st b1 is AP-like
proof end;
end;

registration
let f be real-valued AP-like Function;
let n be Nat;
cluster f | n -> AP-like ;
coherence
f | n is AP-like
proof end;
end;

definition
mode Arithmetic_Progression is AP-like sequence of REAL;
end;

:: Constructor for arithmetic progressions
definition
let a, r be Real;
:: Constructor for arithmetic progressions
func ArProg (a,r) -> sequence of REAL means :ArDefRec: :: NUMBER06:def 4
( it . 0 = a & ( for i being Nat holds it . (i + 1) = (it . i) + r ) );
correctness
existence
ex b1 being sequence of REAL st
( b1 . 0 = a & ( for i being Nat holds b1 . (i + 1) = (b1 . i) + r ) );
uniqueness
for b1, b2 being sequence of REAL st b1 . 0 = a & ( for i being Nat holds b1 . (i + 1) = (b1 . i) + r ) & b2 . 0 = a & ( for i being Nat holds b2 . (i + 1) = (b2 . i) + r ) holds
b1 = b2;
proof end;
end;

:: deftheorem ArDefRec defines ArProg NUMBER06:def 4 :
for a, r being Real
for b3 being sequence of REAL holds
( b3 = ArProg (a,r) iff ( b3 . 0 = a & ( for i being Nat holds b3 . (i + 1) = (b3 . i) + r ) ) );

registration
let a, r be Real;
cluster ArProg (a,r) -> AP-like ;
coherence
ArProg (a,r) is AP-like
proof end;
end;

theorem LemmaDiffConst: :: NUMBER06:5
for f being Arithmetic_Progression
for i being Nat holds (f . (i + 1)) - (f . i) = (f . 1) - (f . 0)
proof end;

definition
let f be Arithmetic_Progression;
func difference f -> Real equals :: NUMBER06:def 5
(f . 1) - (f . 0);
coherence
(f . 1) - (f . 0) is Real ;
end;

:: deftheorem defines difference NUMBER06:def 5 :
for f being Arithmetic_Progression holds difference f = (f . 1) - (f . 0);

theorem APAsArProg: :: NUMBER06:6
for f being Arithmetic_Progression holds f = ArProg ((f . 0),(difference f))
proof end;

:: Lemma stating that for every AP-like you can get ArProg
theorem ArDefNth: :: NUMBER06:7
for a, r being Real
for i being Nat holds (ArProg (a,r)) . i = a + (i * r)
proof end;

registration
let a, r be Integer;
cluster ArProg (a,r) -> integer-valued ;
coherence
ArProg (a,r) is integer-valued
proof end;
end;

registration
cluster Relation-like omega -defined REAL -valued non empty Function-like V44( omega ) V45( omega , REAL ) complex-valued ext-real-valued real-valued integer-valued AP-like for Element of bool [:omega,REAL:];
existence
ex b1 being Arithmetic_Progression st b1 is integer-valued
proof end;
end;

registration
let a be Integer;
let r be non zero Integer;
cluster ArProg (a,r) -> non constant ;
coherence
not ArProg (a,r) is constant
proof end;
end;

registration
let a be Real;
let r be positive Real;
cluster ArProg (a,r) -> increasing ;
coherence
ArProg (a,r) is increasing
proof end;
end;

registration
let a be Real;
let r be non positive Real;
cluster ArProg (a,r) -> non-increasing ;
coherence
ArProg (a,r) is non-increasing
proof end;
end;

registration
let a be Real;
let r be negative Real;
cluster ArProg (a,r) -> decreasing ;
coherence
ArProg (a,r) is decreasing
proof end;
end;

registration
let a be Real;
let r be non negative Real;
cluster ArProg (a,r) -> non-decreasing ;
coherence
ArProg (a,r) is non-decreasing
proof end;
end;

registration
let a be Real;
cluster ArProg (a,0) -> constant ;
coherence
ArProg (a,0) is constant
proof end;
end;

registration
cluster Relation-like omega -defined REAL -valued non empty Function-like constant V44( omega ) V45( omega , REAL ) complex-valued ext-real-valued real-valued AP-like for Element of bool [:omega,REAL:];
existence
ex b1 being Arithmetic_Progression st b1 is constant
proof end;
end;

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

registration
let f be increasing Arithmetic_Progression;
cluster difference f -> positive ;
coherence
difference f is positive
proof end;
end;

registration
let f be decreasing Arithmetic_Progression;
cluster difference f -> negative ;
coherence
difference f is negative
proof end;
end;

registration
let f be non-increasing Arithmetic_Progression;
cluster difference f -> non positive ;
coherence
not difference f is positive
proof end;
end;

registration
let f be non-decreasing Arithmetic_Progression;
cluster difference f -> non negative ;
coherence
not difference f is negative
proof end;
end;

registration
let f be constant Arithmetic_Progression;
cluster difference f -> zero ;
coherence
difference f is zero
proof end;
end;

theorem LemmaIntProg: :: NUMBER06:8
for f being Arithmetic_Progression st ex i being Nat st
( f . i is Integer & difference f is Integer ) holds
f is integer-valued
proof end;

:: Prove that Fibonacci's sequence (defined by conditions u_1 = u_2 = 1,
:: u_{n+2} = u_n + u_{n+1}, n = 1,2,...) contains an infinite increasing
:: sequence such that every two terms of this sequence are relatively prime.
definition
let n be Nat;
attr n is Fibonacci means :: NUMBER06:def 6
 ex k being Nat st n = Fib k;
end;

:: deftheorem defines Fibonacci NUMBER06:def 6 :
for n being Nat holds
( n is Fibonacci iff ex k being Nat st n = Fib k );

registration
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like finite cardinal ext-real non negative Fibonacci for set ;
existence
ex b1 being Nat st b1 is Fibonacci
proof end;
end;

::: restated for non zero Fibonacci
theorem FibGe2: :: NUMBER06:9
for n being Nat st Fib n > 1 holds
n > 2
proof end;

theorem LemmaFib0: :: NUMBER06:10
for k being Nat st k > 0 holds
Fib k > 0
proof end;

theorem FiboLeq: :: NUMBER06:11
for k, m being Nat st Fib k < Fib (m + 1) & 1 < k holds
Fib k <= Fib m
proof end;

Th46: for k, n being Nat st k <> 1 & k < n holds
Fib k < Fib n
proof end;

theorem Th48: :: NUMBER06:12
for k, n being Nat st k <> 1 & n <> 1 & Fib k = Fib n holds
k = n
proof end;

theorem FibGe2a: :: NUMBER06:13
for n being Nat st n > 2 holds
Fib n >= 2
proof end;

theorem FibGe3: :: NUMBER06:14
for n being Nat st n > 3 holds
Fib n >= 3
proof end;

theorem LemmaGe1: :: NUMBER06:15
for m, n being Nat st m < n & m > 3 holds
(Fib n) - (Fib m) > 1
proof end;

theorem LemmaGe2a: :: NUMBER06:16
for m, n being Nat st m < n & m > 4 holds
(Fib n) - (Fib m) > 2
proof end;

definition
let f be sequence of REAL;
attr f is Fibonacci-valued means :: NUMBER06:def 7
 for n being Nat ex fn being Nat st
( fn = f . n & fn is Fibonacci );
end;

:: deftheorem defines Fibonacci-valued NUMBER06:def 7 :
for f being sequence of REAL holds
( f is Fibonacci-valued iff for n being Nat ex fn being Nat st
( fn = f . n & fn is Fibonacci ) );

registration
cluster Function-like V45( omega , REAL ) Fibonacci-valued -> integer-valued for Element of bool [:omega,REAL:];
coherence
for b1 being sequence of REAL st b1 is Fibonacci-valued holds
b1 is integer-valued
proof end;
end;

registration
cluster Relation-like omega -defined REAL -valued non empty Function-like V44( omega ) V45( omega , REAL ) complex-valued ext-real-valued real-valued Fibonacci-valued for Element of bool [:omega,REAL:];
existence
ex b1 being sequence of REAL st b1 is Fibonacci-valued
proof end;
end;

registration
let n be Nat;
cluster Fib n -> Fibonacci ;
coherence
Fib n is Fibonacci ;
end;

theorem Problem50: :: NUMBER06:17
ex f being Fibonacci-valued sequence of REAL st
( f is increasing & f is with_all_coprime_terms )
proof end;

registration
cluster Relation-like omega -defined REAL -valued non empty Function-like V44( omega ) V45( omega , REAL ) complex-valued ext-real-valued real-valued rational-valued integer-valued increasing with_all_coprime_terms Fibonacci-valued for Element of bool [:omega,REAL:];
existence
ex b1 being integer-valued sequence of REAL st
( b1 is Fibonacci-valued & b1 is increasing & b1 is with_all_coprime_terms ) by Problem50;
end;

theorem ThreeConsecutive: :: NUMBER06:18
for n being Nat holds
( 3 divides n or 3 divides n + 1 or 3 divides n + 2 )
proof end;

theorem :: NUMBER06:19
for n being Nat holds
( 4 divides n or 4 divides n + 1 or 4 divides n + 2 or 4 divides n + 3 )
proof end;

theorem LemmaCong: :: NUMBER06:20
for n, k, l being Nat holds
( 3 divides n + l iff 3 divides (n + l) + (3 * k) )
proof end;

definition
let f be Function;
attr f is triangular-valued means :: NUMBER06:def 8
 for n being object holds f . n is triangular ;
end;

:: deftheorem defines triangular-valued NUMBER06:def 8 :
for f being Function holds
( f is triangular-valued iff for n being object holds f . n is triangular );

registration
cluster triangular -> integer for set ;
coherence
for b1 being number st b1 is triangular holds
b1 is integer ;
end;

registration
cluster Function-like V45( omega , REAL ) triangular-valued -> integer-valued for Element of bool [:omega,REAL:];
coherence
for b1 being sequence of REAL st b1 is triangular-valued holds
b1 is integer-valued
proof end;
end;

registration
cluster Relation-like omega -defined REAL -valued non empty Function-like V44( omega ) V45( omega , REAL ) complex-valued ext-real-valued real-valued rational-valued integer-valued triangular-valued for Element of bool [:omega,REAL:];
existence
ex b1 being integer-valued sequence of REAL st b1 is triangular-valued
proof end;
end;

registration
cluster <*0*> -> triangular-valued for FinSequence;
coherence
for b1 being FinSequence st b1 = <*0*> holds
b1 is triangular-valued
proof end;
end;

:: Prove that there exist arbitrarily long arithmetic progressions formed
:: of different positive integers such that every two terms of these
:: progressions are relatively prime.
theorem LemmaFor52: :: NUMBER06:21
for m, k, l being Nat st k <> l & 1 <= k & k <= m & 1 <= l & l <= m holds
((m !) * k) + 1,((m !) * l) + 1 are_coprime
proof end;

theorem :: NUMBER06:22
for n being Nat ex f being integer-valued AP-like XFinSequence st
( dom f >= n & f is with_all_coprime_terms )
proof end;

:: Prove that there exist infinitely many triplets of
:: positive integers x,y,z st x(x+1), y(y+1), z(z+1) form
:: an increasing arithmetic progression.
definition
let x, y, z be Real;
pred x,y,z form_an_AP means :: NUMBER06:def 9
y - x = z - y;
end;

:: deftheorem defines form_an_AP NUMBER06:def 9 :
for x, y, z being Real holds
( x,y,z form_an_AP iff y - x = z - y );

theorem :: NUMBER06:23
for x, y, z being Nat st y = (5 * x) + 2 & z = (7 * x) + 3 holds
( x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP & x < y & y < z )
proof end;

theorem :: NUMBER06:24
{ <*x,y,z*> where x, y, z is Real : x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP } is infinite
proof end;

:: Find all rectangular triangles with integer sides forming
:: an arithmetic progression.
theorem :: NUMBER06:25
for a, b, c being Nat st (a ^2) + (b ^2) = c ^2 & a,b,c form_an_AP holds
ex i being Integer st
( a = 3 * i & b = 4 * i & c = 5 * i )
proof end;

:: Find an increasing arithmetic progression with the least possible
:: difference, formed of positive integers and containing no triangular number.
registration
let k be Nat;
cluster Triangle ((4 * k) + 1) -> odd ;
coherence
not Triangle ((4 * k) + 1) is even
proof end;
end;

registration
let k be Nat;
cluster Triangle (4 * k) -> even ;
coherence
Triangle (4 * k) is even
proof end;
end;

theorem Divides3Triangle2: :: NUMBER06:26
for n being Nat holds 3 divides Triangle ((3 * n) + 2)
proof end;

theorem Divides3Triangle: :: NUMBER06:27
for n being Nat holds 3 divides Triangle (3 * n)
proof end;

theorem Not3DividesTriangle: :: NUMBER06:28
for n being Nat holds 3 divides (Triangle ((3 * n) + 1)) - 1
proof end;

theorem Lemma3ArProg: :: NUMBER06:29
for i being Nat holds not 3 divides (ArProg (2,3)) . i
proof end;

theorem :: NUMBER06:30
{ i where i is Nat : (ArProg (0,1)) . i is triangular } is infinite
proof end;

theorem :: NUMBER06:31
{ i where i is Nat : (ArProg (0,2)) . i is triangular } is infinite
proof end;

theorem :: NUMBER06:32
{ i where i is Nat : (ArProg (1,2)) . i is triangular } is infinite
proof end;

theorem LemmaBono: :: NUMBER06:33
for i being Nat holds not 3 divides ((ArProg (2,3)) . i) - 1
proof end;

theorem :: NUMBER06:34
for i being Nat holds not (ArProg (2,3)) . i is triangular
proof end;

:: Prove that there are no four consecutive positive integers such that
:: each of them is a power of a positive integer with an integer exponent > 1.
definition
let n be Nat;
:: Prove that there are no four consecutive positive integers such that
:: each of them is a power of a positive integer with an integer exponent > 1.
attr n is perfect_power means :PerPowDef: :: NUMBER06:def 10
 ex x, k being Nat st
( k > 1 & n = x |^ k );
end;

:: deftheorem PerPowDef defines perfect_power NUMBER06:def 10 :
for n being Nat holds
( n is perfect_power iff ex x, k being Nat st
( k > 1 & n = x |^ k ) );

theorem :: NUMBER06:35
ex n being Nat st
( n is perfect_power & n + 1 is perfect_power )
proof end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like finite cardinal even ext-real non negative perfect_power for set ;
existence
ex b1 being Nat st
( b1 is even & b1 is perfect_power )
proof end;
end;

theorem FourDivPower: :: NUMBER06:36
for n being even Nat
for k being Nat st k > 1 holds
4 divides n |^ k
proof end;

theorem FourPerfectPower: :: NUMBER06:37
for n being even perfect_power Nat holds 4 divides n
proof end;

theorem Four2NotPerfect: :: NUMBER06:38
for k being Nat holds not (4 * k) + 2 is perfect_power
proof end;

theorem PrimesNotPowers: :: NUMBER06:39
for p being Prime holds not p is perfect_power
proof end;

registration
cluster natural prime -> non perfect_power for set ;
coherence
for b1 being Nat st b1 is prime holds
not b1 is perfect_power by PrimesNotPowers;
end;

registration
cluster natural square -> perfect_power for set ;
coherence
for b1 being Nat st b1 is square holds
b1 is perfect_power
proof end;
end;

theorem :: NUMBER06:40
for n being Nat holds
( not n is perfect_power or not n + 1 is perfect_power or not n + 2 is perfect_power or not n + 3 is perfect_power )
proof end;

:: Find all increasing arithmetic progressions formed of three terms
:: of the Fibonacci sequence (see Problem 50), and prove that there are no
:: increasing arithmetic progressions formed of four terms of this sequence.
theorem Problem64Part1: :: NUMBER06:41
for k, l, m being Nat st 0 < k & k < l & l < m & ( not k = 2 or not l = 3 or not m = 4 ) & ( not k = 1 or not l = 4 or not m = 5 ) & (Fib m) - (Fib l) = (Fib l) - (Fib k) & (Fib l) - (Fib k) > 0 holds
( l > 2 & k = l - 2 & m = l + 1 )
proof end;

theorem :: NUMBER06:42
(Fib 1) - (Fib 0) <> (Fib 2) - (Fib 1) by FIB_NUM2:21, PRE_FF:1;

theorem :: NUMBER06:43
(Fib 1) - (Fib 0) = (Fib 3) - (Fib 1) by FIB_NUM2:22, PRE_FF:1;

theorem :: NUMBER06:44
(Fib 2) - (Fib 0) = (Fib 3) - (Fib 2) by FIB_NUM2:21, FIB_NUM2:22, PRE_FF:1;

theorem :: NUMBER06:45
(Fib 3) - (Fib 2) = (Fib 4) - (Fib 3) by FIB_NUM2:23, FIB_NUM2:22, FIB_NUM2:21;

theorem Fib5: :: NUMBER06:46
Fib 5 = 5
proof end;

theorem :: NUMBER06:47
(Fib 5) - (Fib 4) = (Fib 4) - (Fib 1) by FIB_NUM2:23, PRE_FF:1, Fib5;

theorem :: NUMBER06:48
for k, l, m, n being Nat holds
( not 0 < k or not k < l or not l < m or not m < n or not (Fib m) - (Fib l) = (Fib l) - (Fib k) or not (Fib l) - (Fib k) = (Fib n) - (Fib m) or not (Fib l) - (Fib k) > 0 )
proof end;

:: Find all arithmetic progressions with difference 10 formed of more
:: than two primes.
theorem :: NUMBER06:49
for f being Arithmetic_Progression
for p1, p2, p3 being Prime st difference f = 10 & ex i being Nat st
( p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) holds
p1 = 3
proof end;

theorem :: NUMBER06:50
for f being Arithmetic_Progression holds
( not difference f = 10 or for p1, p2, p3, p4 being Prime
for i being Nat holds
( not p1,p2,p3,p4 are_mutually_distinct or not p1 = f . i or not p2 = f . (i + 1) or not p3 = f . (i + 2) or not p4 = f . (i + 3) ) )
proof end;

:: Find all arithmetic progressions with difference 100 formed of more
:: than two primes.
theorem :: NUMBER06:51
for f being Arithmetic_Progression holds
( not difference f = 100 or for p1, p2, p3 being Prime
for i being Nat holds
( not p1,p2,p3 are_mutually_distinct or not p1 = f . i or not p2 = f . (i + 1) or not p3 = f . (i + 2) ) )
proof end;

theorem :: NUMBER06:52
for f being Arithmetic_Progression holds
( not difference f = 1000 or for p1, p2, p3 being Prime
for i being Nat holds
( not p1,p2,p3 are_mutually_distinct or not p1 = f . i or not p2 = f . (i + 1) or not p3 = f . (i + 2) ) )
proof end;

:: Give an example of an infinite increasing arithmetic progression formed
:: of positive integers such that no term of this progression can be
:: represented as a sum or a difference of two primes.
definition
let k be Integer;
attr k is not_representable_by_sum_or_difference_of_two_primes means :: NUMBER06:def 11
 for p1, p2 being Prime holds
( not k = p1 + p2 & not k = p1 - p2 );
end;

:: deftheorem defines not_representable_by_sum_or_difference_of_two_primes NUMBER06:def 11 :
for k being Integer holds
( k is not_representable_by_sum_or_difference_of_two_primes iff for p1, p2 being Prime holds
( not k = p1 + p2 & not k = p1 - p2 ) );

definition
let f be integer-valued sequence of REAL;
attr f is with_terms_not_representable_by_sum_or_diff_of_two_primes means :: NUMBER06:def 12
 for i being Nat holds f . i is not_representable_by_sum_or_difference_of_two_primes ;
end;

:: deftheorem defines with_terms_not_representable_by_sum_or_diff_of_two_primes NUMBER06:def 12 :
for f being integer-valued sequence of REAL holds
( f is with_terms_not_representable_by_sum_or_diff_of_two_primes iff for i being Nat holds f . i is not_representable_by_sum_or_difference_of_two_primes );

theorem Lemma30kOdd: :: NUMBER06:53
for k being Integer holds (30 * k) + 7 is odd
proof end;

theorem Lemma73: :: NUMBER06:54
for k being Nat st k >= 1 holds
(30 * k) + 7 is not_representable_by_sum_or_difference_of_two_primes
proof end;

registration
cluster ArProg (37,30) -> with_terms_not_representable_by_sum_or_diff_of_two_primes ;
coherence
ArProg (37,30) is with_terms_not_representable_by_sum_or_diff_of_two_primes
proof end;
end;