:: Elementary Number Theory Problems. {P}art {X}
:: by Artur Korni{\l}owicz
::
:: Received November 21, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

Lm1: 2 |^ 2 = 2 * 2
by NEWTON:81;

Lm2: 2 |^ 3 = (2 * 2) * 2
by POLYEQ_5:2;

theorem Th1: :: NUMBER10:1

for i, j being natural Number st i < j holds
ex k being positive Nat st j = i + k

proof end;

theorem Th2: :: NUMBER10:2

for f being integer-valued positive-yielding FinSequence holds Product f >= 1

proof end;

theorem Th3: :: NUMBER10:3

for m, n being Nat st m >= 2 & n >= 2 holds
m * n is composite

proof end;

theorem Th4: :: NUMBER10:4

for n being Nat
for p being Prime st not p divides n holds
n,p are_coprime

proof end;

theorem Th5: :: NUMBER10:5

for p being Prime holds (- 1) mod p = p - 1

proof end;

definition

let r, s be Complex;

pred r,s are_twin means :: NUMBER10:def 1
|.(s - r).| = 2;

irreflexivity
for r being Complex holds not |.(r - r).| = 2 by COMPLEX1:44;
symmetry
for r, s being Complex st |.(s - r).| = 2 holds
|.(r - s).| = 2 by COMPLEX1:60;

end;

:: deftheorem defines are_twin NUMBER10:def 1 :
for r, s being Complex holds
( r,s are_twin iff |.(s - r).| = 2 );

notation

let r, s be Complex;
antonym r,s are_not_twin for r,s are_twin ;

end;

theorem Th6: :: NUMBER10:6

for r, s being Real st r <= s holds
( r,s are_twin iff s - r = 2 )

proof end;

definition

let n be Nat;

func <=6n+1 n -> Subset of NAT equals :: NUMBER10:def 2
{ a where a is Nat : a <= (6 * n) + 1 } ;

coherence
{ a where a is Nat : a <= (6 * n) + 1 } is Subset of NAT

proof end;

end;

:: deftheorem defines <=6n+1 NUMBER10:def 2 :
for n being Nat holds <=6n+1 n = { a where a is Nat : a <= (6 * n) + 1 } ;

theorem Th7: :: NUMBER10:7

for a, n being Nat holds
( a <= (6 * n) + 1 iff a in <=6n+1 n )

proof end;

theorem Th8: :: NUMBER10:8

for n being Nat holds <=6n+1 n c= Segm ((6 * n) + 2)

proof end;

registration

let n be Nat;

cluster <=6n+1 n -> non empty finite ;

coherence
( not <=6n+1 n is empty & <=6n+1 n is finite )

proof end;

end;

theorem Th9: :: NUMBER10:9

for m, n being Nat st m <= n holds
<=6n+1 m c= <=6n+1 n

proof end;

theorem Th10: :: NUMBER10:10

for m, n being Nat st m < n holds
<=6n+1 m c< <=6n+1 n

proof end;

theorem :: NUMBER10:11

for m, n being Nat st <=6n+1 m = <=6n+1 n holds
m = n

proof end;

theorem Th12: :: NUMBER10:12

for n being non zero Nat holds 2 in (<=6n+1 n) /\ SetPrimes

proof end;

theorem :: NUMBER10:13

for n being non zero Nat holds 3 in (<=6n+1 n) /\ SetPrimes

proof end;

theorem :: NUMBER10:14

for n being non zero Nat holds 5 in (<=6n+1 n) /\ SetPrimes

proof end;

theorem :: NUMBER10:15

for n being non zero Nat holds 7 in (<=6n+1 n) /\ SetPrimes

proof end;

registration

let n be non zero Nat;

cluster (<=6n+1 n) /\ SetPrimes -> non empty ;

coherence
not (<=6n+1 n) /\ SetPrimes is empty by Th12;

end;

definition

let n be non zero Nat;

func LP<=6n+1 n -> Prime equals :: NUMBER10:def 3
max ((<=6n+1 n) /\ SetPrimes);

coherence
max ((<=6n+1 n) /\ SetPrimes) is Prime

proof end;

end;

:: deftheorem defines LP<=6n+1 NUMBER10:def 3 :
for n being non zero Nat holds LP<=6n+1 n = max ((<=6n+1 n) /\ SetPrimes);

theorem Th16: :: NUMBER10:16

for m, n being non zero Nat st m <= n holds
LP<=6n+1 m <= LP<=6n+1 n

proof end;

theorem :: NUMBER10:17

LP<=6n+1 20 = LP<=6n+1 19

proof end;

theorem :: NUMBER10:18

<=6n+1 1 = {0,1,2,3,4,5,6,7}

proof end;

theorem :: NUMBER10:19

LP<=6n+1 1 = 7

proof end;

theorem Th20: :: NUMBER10:20

for m, n being Nat st primenumber m = primenumber n holds
m = n

proof end;

definition

let p be Nat;
assume A1: p is prime ;

func primeindex p -> Element of NAT means :Def4: :: NUMBER10:def 4
primenumber it = p;

existence
ex b₁ being Element of NAT st primenumber b₁ = p

proof end;

uniqueness
for b₁, b₂ being Element of NAT st primenumber b₁ = p & primenumber b₂ = p holds
b₁ = b₂ by Th20;

end;

:: deftheorem Def4 defines primeindex NUMBER10:def 4 :
for p being Nat st p is prime holds
for b₂ being Element of NAT holds
( b₂ = primeindex p iff primenumber b₂ = p );

theorem :: NUMBER10:21

for p, q being Prime st primeindex p = primeindex q holds
p = q

proof end;

theorem :: NUMBER10:22

primeindex 2 = 0 by Def4, MOEBIUS2:8;

theorem :: NUMBER10:23

primeindex 3 = 1 by Def4, MOEBIUS2:10;

theorem :: NUMBER10:24

primeindex 5 = 2 by Def4, MOEBIUS2:12;

theorem :: NUMBER10:25

primeindex 7 = 3 by Def4, MOEBIUS2:15;

theorem :: NUMBER10:26

primeindex 11 = 4 by Def4, MOEBIUS2:17;

theorem :: NUMBER10:27

primeindex 13 = 5 by Def4, MOEBIUS2:19;

theorem Th28: :: NUMBER10:28

for n being Nat
for p being Prime st n > 0 holds
p < primenumber (n + (primeindex p))

proof end;

theorem Th29: :: NUMBER10:29

for n being non zero Nat holds primenumber (1 + (primeindex (LP<=6n+1 n))) >= (6 * n) + 5

proof end;

theorem Th30: :: NUMBER10:30

for n being non zero Nat holds (primenumber (1 + (primeindex (LP<=6n+1 n)))) - (LP<=6n+1 n) >= 4

proof end;

theorem Th31: :: NUMBER10:31

for n being non zero Nat holds LP<=6n+1 n, primenumber (1 + (primeindex (LP<=6n+1 n))) are_not_twin

proof end;

theorem Th32: :: NUMBER10:32

for m being non zero Nat st (6 * m) + 1 is prime holds
(6 * m) + 1 = LP<=6n+1 m

proof end;

theorem Th33: :: NUMBER10:33

for m, n being non zero Nat st (6 * n) + 1 is prime & m < n holds
LP<=6n+1 m < LP<=6n+1 n

proof end;

theorem Th34: :: NUMBER10:34

for m, n being non zero Nat st (6 * m) + 1 is prime & (6 * n) + 1 is prime & LP<=6n+1 m = LP<=6n+1 n holds
m = n

proof end;

definition

func 6n+1_Primes -> Subset of NAT equals :: NUMBER10:def 5
{ ((6 * n) + 1) where n is Nat : (6 * n) + 1 is prime } ;

coherence
{ ((6 * n) + 1) where n is Nat : (6 * n) + 1 is prime } is Subset of NAT

proof end;

end;

:: deftheorem defines 6n+1_Primes NUMBER10:def 5 :
6n+1_Primes = { ((6 * n) + 1) where n is Nat : (6 * n) + 1 is prime } ;

registration

cluster 6n+1_Primes -> with_non-empty_elements ;

coherence
6n+1_Primes is with_non-empty_elements

proof end;

end;

theorem :: NUMBER10:35

6n+1_Primes c= SetPrimes

proof end;

registration

cluster 6n+1_Primes -> infinite ;

coherence
not 6n+1_Primes is finite

proof end;

end;

:: Problem 84

theorem :: NUMBER10:36

{ [p,q] where p, q is Prime : p,q are_not_twin } is infinite

proof end;

definition

let c be Complex;

attr c is a_product_of_three_different_primes means :: NUMBER10:def 6
ex p, q, r being Prime st
( p,q,r are_mutually_distinct & c = (p * q) * r );

end;

:: deftheorem defines a_product_of_three_different_primes NUMBER10:def 6 :
for c being Complex holds
( c is a_product_of_three_different_primes iff ex p, q, r being Prime st
( p,q,r are_mutually_distinct & c = (p * q) * r ) );

theorem Th37: :: NUMBER10:37

for n being Nat st n > 4 holds
ex k being Nat st
( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) )

proof end;

reconsider p2 = 2 as Prime by XPRIMES1:2;

reconsider p3 = 3 as Prime by XPRIMES1:3;

reconsider p5 = 5 as Prime by XPRIMES1:5;

:: Problem 94 a

theorem :: NUMBER10:38

for n being Nat st n > 4 holds
ex m being Nat st
( n < m & m < 2 * n & m is_a_product_of_two_different_primes )

proof end;

:: Problem 94 b

theorem :: NUMBER10:39

for n being Nat st n > 15 holds
ex m being Nat st
( n < m & m < 2 * n & m is a_product_of_three_different_primes )

proof end;

theorem Th40: :: NUMBER10:40

for n being Nat holds 5 divides (2 |^ ((4 * n) + 2)) + 1

proof end;

registration

let n be Nat;

cluster (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) -> natural ;

coherence
(1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is natural

proof end;

end;

:: Problem 99

theorem :: NUMBER10:41

for n being Nat st n > 1 holds
(1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is composite

proof end;

Lm3: for x, y being Integer holds
( not x * y = 8 or ( x = 1 & y = 8 ) or ( x = 2 & y = 4 ) or ( x = 4 & y = 2 ) or ( x = 8 & y = 1 ) or ( x = - 1 & y = - 8 ) or ( x = - 2 & y = - 4 ) or ( x = - 4 & y = - 2 ) or ( x = - 8 & y = - 1 ) )

proof end;

Lm4: for x, y being Integer holds
( not x * y = - 8 or ( x = 1 & y = - 8 ) or ( x = 2 & y = - 4 ) or ( x = 4 & y = - 2 ) or ( x = 8 & y = - 1 ) or ( x = - 1 & y = 8 ) or ( x = - 2 & y = 4 ) or ( x = - 4 & y = 2 ) or ( x = - 8 & y = 1 ) )

proof end;

Lm5: for x, y being Integer holds
( not x * y = 4 or ( x = 1 & y = 4 ) or ( x = 2 & y = 2 ) or ( x = 4 & y = 1 ) or ( x = - 1 & y = - 4 ) or ( x = - 2 & y = - 2 ) or ( x = - 4 & y = - 1 ) )

proof end;

Lm6: for x, y being Integer holds
( not x * y = - 4 or ( x = 1 & y = - 4 ) or ( x = 2 & y = - 2 ) or ( x = 4 & y = - 1 ) or ( x = - 1 & y = 4 ) or ( x = - 2 & y = 2 ) or ( x = - 4 & y = 1 ) )

proof end;

Lm7: for x, y being Integer holds
( not x * y = 2 or ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) )

proof end;

Lm8: for x, y being Integer holds
( not x * y = - 2 or ( x = 1 & y = - 2 ) or ( x = 2 & y = - 1 ) or ( x = - 1 & y = 2 ) or ( x = - 2 & y = 1 ) )

proof end;

Lm9: ( (2 * 0) - 1 is odd & (2 * 1) - 1 is odd )
;

Lm10: ( 2 * 1 is even & 2 * (- 1) is even & 2 * 2 is even & 2 * (- 2) is even & 2 * (- 4) is even )
;

Lm11: for x, y, z being even Integer holds
( not (x * y) * z = 8 or ( x = 2 & y = 2 & z = 2 ) or ( x = - 2 & y = - 2 & z = 2 ) or ( x = - 2 & y = 2 & z = - 2 ) or ( x = 2 & y = - 2 & z = - 2 ) )

proof end;

Lm12: for x being even Integer
for y, z being odd Integer holds
( not (x * y) * z = 8 or ( x = 8 & y = 1 & z = 1 ) or ( x = 8 & y = - 1 & z = - 1 ) or ( x = - 8 & y = 1 & z = - 1 ) or ( x = - 8 & y = - 1 & z = 1 ) )

proof end;

:: Problem 170

theorem :: NUMBER10:42

{ [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } = {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]}

proof end;

:: Problem 173

theorem :: NUMBER10:43

for m, n being positive Nat ex a, b, c being Integer st { [x,y] where x, y is Nat : (a * x) + (b * y) = c } = {[m,n]}

proof end;

theorem Th44: :: NUMBER10:44

for m being positive Nat holds card { [x,y] where x, y is positive Nat : x + y = m + 1 } = m

proof end;

:: Problem 174

theorem :: NUMBER10:45

for m being positive Nat ex a, b, c being positive Nat st card { [x,y] where x, y is positive Nat : (a * x) + (b * y) = c } = m

proof end;

:: Problem 175

theorem :: NUMBER10:46

for m being positive Nat holds card { [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } = m

proof end;

definition

let b, e be Real;
let n be Nat;

func powersFS (b,e,n) -> FinSequence of REAL means :Def7: :: NUMBER10:def 7
( len it = n & ( for i being Nat st 1 <= i & i <= n holds
it . i = (b + i) to_power e ) );

existence
ex b₁ being FinSequence of REAL st
( len b₁ = n & ( for i being Nat st 1 <= i & i <= n holds
b₁ . i = (b + i) to_power e ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = n & ( for i being Nat st 1 <= i & i <= n holds
b₁ . i = (b + i) to_power e ) & len b₂ = n & ( for i being Nat st 1 <= i & i <= n holds
b₂ . i = (b + i) to_power e ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines powersFS NUMBER10:def 7 :
for b, e being Real
for n being Nat
for b₄ being FinSequence of REAL holds
( b₄ = powersFS (b,e,n) iff ( len b₄ = n & ( for i being Nat st 1 <= i & i <= n holds
b₄ . i = (b + i) to_power e ) ) );

theorem Th47: :: NUMBER10:47

for k being Nat
for r being Real holds powersFS ((- (k + 1)),r,(2 * (k + 1))) = (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>

proof end;

theorem Th48: :: NUMBER10:48

for r being Real
for k being positive Nat holds powersFS ((- (k + 1)),r,((2 * (k + 1)) - 1)) = (<*((- k) to_power r)*> ^ (powersFS ((- k),r,((2 * k) - 1)))) ^ <*(k to_power r)*>

proof end;

theorem Th49: :: NUMBER10:49

for k being Nat holds Sum (powersFS ((- k),3,(2 * k))) = k |^ 3

proof end;

theorem Th50: :: NUMBER10:50

for k being positive Nat holds Sum (powersFS ((- k),3,((2 * k) - 1))) = 0

proof end;

:: Problem 177

theorem :: NUMBER10:51

for n being positive Nat ex x being Integer ex y being Nat st Sum (powersFS (x,3,n)) = y |^ 3

proof end;

:: Problem 179

theorem :: NUMBER10:52

for x being Real holds
( ((((x + 1) |^ 3) + ((x + 2) |^ 3)) + ((x + 3) |^ 3)) + ((x + 4) |^ 3) = (x + 10) |^ 3 iff x = 10 )

proof end;

:: Problem 186

theorem :: NUMBER10:53

{ [x,y] where x, y is positive Nat : (2 |^ x) + 1 = y ^2 } = {[3,3]}

proof end;

:: Problem 187

theorem :: NUMBER10:54

{ [x,y] where x, y is positive Nat : (2 |^ x) - 1 = y ^2 } = {[1,1]}

proof end;

theorem Th55: :: NUMBER10:55

{ [x,y] where x, y is positive Nat : ((((2 * x) + 1) ^2) - (2 * (y ^2))) + 1 = 0 } is infinite

proof end;

:: Problem 189

theorem :: NUMBER10:56

{ [x,y] where x, y is positive Nat : (x ^2) + ((x + 1) ^2) = y ^2 } is infinite

proof end;

theorem Th57: :: NUMBER10:57

{ [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } is infinite

proof end;

Lm13: now :: thesis: for x, y being Complex holds (((x + 1) |^ 3) - (x |^ 3)) - (y ^2) = (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1

let x, y be Complex; :: thesis: (((x + 1) |^ 3) - (x |^ 3)) - (y ^2) = (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1
( (x + 1) |^ 3 = ((x + 1) * (x + 1)) * (x + 1) & x |^ 3 = (x * x) * x ) by POLYEQ_5:2;
hence (((x + 1) |^ 3) - (x |^ 3)) - (y ^2) = (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 ; :: thesis: verum

end;

:: Problem 190

theorem :: NUMBER10:58

{ [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } is infinite

proof end;

Lm14: for n being Nat holds
( ((2 * n) ^2) mod 8 = 0 or ((2 * n) ^2) mod 8 = 4 )

proof end;

Lm15: for i being Integer holds
( ((2 * i) ^2) mod 8 = 0 or ((2 * i) ^2) mod 8 = 4 )

proof end;

theorem Th59: :: NUMBER10:59

for i being Integer holds
( not i is even or (i ^2) mod 8 = 0 or (i ^2) mod 8 = 4 )

proof end;

Lm16: for i being Integer holds (((2 * i) + 1) ^2) mod 8 = 1

proof end;

theorem Th60: :: NUMBER10:60

for i being Integer st i is odd holds
(i ^2) mod 8 = 1

proof end;

theorem :: NUMBER10:61

for i being Integer holds
( (i ^2) mod 8 = 0 or (i ^2) mod 8 = 1 or (i ^2) mod 8 = 4 ) by Th59, Th60;

Lm17: for a, b, k being Nat
for p being Prime st p = (4 * k) + 3 & p divides (a ^2) + (b ^2) holds
( p divides a & p divides b )

proof end;

theorem Th62: :: NUMBER10:62

for k being Nat
for i, j being Integer
for p being Prime st p = (4 * k) + 3 & p divides (i ^2) + (j ^2) holds
( p divides i & p divides j )

proof end;

Lm18: now :: thesis: for n being Nat
for i being Integer st (4 * n) + 3 is prime holds
not (4 * n) + 3 divides (i ^2) + (1 ^2)

let n be Nat; :: thesis: for i being Integer st (4 * n) + 3 is prime holds
not (4 * n) + 3 divides (i ^2) + (1 ^2)
let i be Integer; :: thesis: ( (4 * n) + 3 is prime implies not (4 * n) + 3 divides (i ^2) + (1 ^2) )
assume A1: (4 * n) + 3 is prime ; :: thesis: not (4 * n) + 3 divides (i ^2) + (1 ^2)
assume (4 * n) + 3 divides (i ^2) + (1 ^2) ; :: thesis: contradiction
then (4 * n) + 3 divides 1 by A1, Th62;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

:: Problem 193

theorem :: NUMBER10:63

for x, y being Integer holds (x |^ 2) - (y |^ 3) <> 7

proof end;

Lm19: now :: thesis: for i being Integer holds ((2 * i) |^ 3) mod 8 = 0

let i be Integer; :: thesis: ((2 * i) |^ 3) mod 8 = 0
(2 * i) |^ 3 = ((2 * i) * (2 * i)) * (2 * i) by POLYEQ_5:2
.= (8 * ((i * i) * i)) + 0 ;
hence ((2 * i) |^ 3) mod 8 = 0 ; :: thesis: verum

end;

:: Problem 194

theorem :: NUMBER10:64

for x, y being Integer
for c being odd Nat holds (x |^ 2) - (y |^ 3) <> ((2 * c) |^ 3) - 1

proof end;

registration

let f, g be positive-yielding FinSequence;

cluster f ^ g -> positive-yielding ;

coherence
f ^ g is positive-yielding

proof end;

end;

registration

let x be positive Real;

cluster <*x*> -> positive-yielding ;

coherence
<*x*> is positive-yielding

proof end;

end;

registration

let x, y be positive Real;

cluster <*x,y*> -> positive-yielding ;

coherence
<*x,y*> is positive-yielding ;

end;

:: Problem 197

theorem :: NUMBER10:65

for n being Nat st n > 0 holds
ex f being positive-yielding FinSequence of NAT st
( len f = n & Sum f = Product f )

proof end;

theorem :: NUMBER10:66

for x, y being positive Nat st y * ((3 * y) - 1) = x * (x + 1) holds
Polygon (3,x) = Polygon (5,y) ;

theorem Th67: :: NUMBER10:67

for m, n being positive Nat
for s being natural Number st Polygon (s,m) = Polygon (s,n) & s >= 2 holds
m = n

proof end;

theorem Th68: :: NUMBER10:68

{ [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } is infinite

proof end;

Lm20: not 1 / 3 is integer
by NAT_D:33;

:: Problem 199

theorem :: NUMBER10:69

{ n where n is 3 -gonal Nat : n is 5 -gonal } is infinite

proof end;