:: Elementary Number Theory Problems. Part {XIV} -- Diophantine Equations
:: by Artur Korni{\l}owicz
::
:: Received October 22, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

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

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

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

Lm4: 2 |^ 8 = ((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER02:4;

Lm5: 1 mod 3 = 1
by NAT_D:24;

Lm6: ((1 * 3) + 1) mod 3 = 1 mod 3
by NAT_D:21;

registration

let a, b, c be Integer;

reduce In ([a,b,c],[:INT,INT,INT:]) to [a,b,c];

reducibility
In ([a,b,c],[:INT,INT,INT:]) = [a,b,c]

proof end;

end;

theorem :: NUMBER14:1

for a, b being Real st 0 <= a & a < b holds
|.a.| < |.b.|

proof end;

theorem Th2: :: NUMBER14:2

for a, b being Real st b < a & a <= 0 holds
|.a.| < |.b.|

proof end;

theorem :: NUMBER14:3

for i, j, z being Integer st j <> 0 & z = i / j holds
z divides i

proof end;

theorem Th4: :: NUMBER14:4

for i, j being Integer holds
( i divides j iff i divides |.j.| )

proof end;

theorem :: NUMBER14:5

for i, j being Integer holds
( i divides j iff |.i.| divides j )

proof end;

theorem Th6: :: NUMBER14:6

for n being Nat
for i being Integer
for p being Prime st p divides i |^ n holds
p divides i

proof end;

theorem Th7: :: NUMBER14:7

for p being Prime
for m, n being Nat holds
( not m divides n * p or m divides n or ex z being Nat st
( m = z * p & z divides n ) )

proof end;

theorem Th8: :: NUMBER14:8

for p being Prime
for m, n being Integer holds
( not m divides n * p or m divides n or ex z being Integer st
( m = z * p & z divides n ) )

proof end;

theorem Th9: :: NUMBER14:9

for i, j being Integer holds
( i,j are_coprime iff |.i.|,|.j.| are_coprime ) by INT_2:34;

theorem Th10: :: NUMBER14:10

for i, j being Integer holds
( i,j are_coprime iff |.i.|,j are_coprime ) by INT_6:14;

theorem Th11: :: NUMBER14:11

for i, j being Integer holds
( i,j are_coprime iff - i, - j are_coprime )

proof end;

theorem :: NUMBER14:12

for i, j being Integer holds
( i,j are_coprime iff - i,j are_coprime ) by NEWTON02:1;

theorem :: NUMBER14:13

for i, j, k being Integer st i <> 0 & i divides k & i * j,k are_coprime & not i = 1 holds
i = - 1

proof end;

theorem Th14: :: NUMBER14:14

for i, j, k being Integer st i divides j & i,j are_coprime & not i = 1 holds
i = - 1

proof end;

theorem :: NUMBER14:15

for i, j being Integer st i divides j holds
j, 0 are_congruent_mod i ;

theorem Th16: :: NUMBER14:16

for a, b, c being Integer st a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime holds
a * b,c are_coprime

proof end;

theorem :: NUMBER14:17

for i, j being Integer st i,j are_congruent_mod 2 holds
( i is odd iff j is odd ) ;

theorem :: NUMBER14:18

for i, j being Integer st i,j are_congruent_mod 2 holds
( i is even iff j is even ) ;

theorem Th19: :: NUMBER14:19

for i, j, k being Integer st i > 0 & j,k are_congruent_mod i holds
( i divides j iff i divides k )

proof end;

theorem Th20: :: NUMBER14:20

for a, b being object
for f being FinSequence holds
( 1 in dom (<*a,b*> ^ f) & 2 in dom (<*a,b*> ^ f) )

proof end;

theorem Th21: :: NUMBER14:21

for a, b being object
for f being FinSequence holds
( (<*a,b*> ^ f) . 1 = a & (<*a,b*> ^ f) . 2 = b )

proof end;

theorem Th22: :: NUMBER14:22

for n being Nat
for a, b being object
for f being FinSequence st n in dom f holds
n + 2 in dom (<*a,b*> ^ f)

proof end;

theorem Th23: :: NUMBER14:23

for n being Nat
for a, b being object
for f being FinSequence st n in dom f holds
(<*a,b*> ^ f) . (n + 2) = f . n

proof end;

theorem :: NUMBER14:24

for f being real-valued decreasing FinSequence holds min_p f = len f

proof end;

theorem :: NUMBER14:25

for f being real-valued increasing FinSequence holds max_p f = len f

proof end;

registration

let X be included_in_Seg real-membered set ;

cluster Sgm X -> increasing ;

coherence
Sgm X is increasing

proof end;

end;

registration

let f be integer-valued Chinese_Remainder FinSequence;

cluster - f -> Chinese_Remainder ;

coherence
- f is Chinese_Remainder

proof end;

end;

registration

let f be non-empty integer-valued Chinese_Remainder FinSequence;

cluster f (#) f -> Chinese_Remainder ;

coherence
f (#) f is Chinese_Remainder

proof end;

end;

definition

let a1, n1, a2, n2 be Integer;
let x be Integer;

pred x solves_CRT a1,n1,a2,n2 means :: NUMBER14:def 1
( x,a1 are_congruent_mod n1 & x,a2 are_congruent_mod n2 );

end;

:: deftheorem defines solves_CRT NUMBER14:def 1 :
for a1, n1, a2, n2, x being Integer holds
( x solves_CRT a1,n1,a2,n2 iff ( x,a1 are_congruent_mod n1 & x,a2 are_congruent_mod n2 ) );

theorem Th26: :: NUMBER14:26

for a1, n1, a2, n2, x being Integer st x solves_CRT a1,n1,a2,n2 holds
for k being Integer holds x + ((k * n1) * n2) solves_CRT a1,n1,a2,n2

proof end;

theorem Th27: :: NUMBER14:27

for a1, a2 being Integer
for n1, n2 being Nat st n1 > 0 & n2 > 0 holds
for x being Integer st x solves_CRT a1,n1,a2,n2 holds
x mod (n1 * n2) solves_CRT a1,n1,a2,n2

proof end;

definition

let a1, a2 be Integer;
let n1, n2 be Nat;
assume that
A1: n1,n2 are_coprime and
A2: n1 > 0 and
A3: n2 > 0 ;

func CRT (a1,n1,a2,n2) -> Element of NAT means :Def2: :: NUMBER14:def 2
( it solves_CRT a1,n1,a2,n2 & it < n1 * n2 );

existence
ex b₁ being Element of NAT st
( b₁ solves_CRT a1,n1,a2,n2 & b₁ < n1 * n2 )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st b₁ solves_CRT a1,n1,a2,n2 & b₁ < n1 * n2 & b₂ solves_CRT a1,n1,a2,n2 & b₂ < n1 * n2 holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines CRT NUMBER14:def 2 :
for a1, a2 being Integer
for n1, n2 being Nat st n1,n2 are_coprime & n1 > 0 & n2 > 0 holds
for b₅ being Element of NAT holds
( b₅ = CRT (a1,n1,a2,n2) iff ( b₅ solves_CRT a1,n1,a2,n2 & b₅ < n1 * n2 ) );

theorem Th28: :: NUMBER14:28

for a1, a2 being Integer
for n1, n2 being Nat st n1,n2 are_coprime & n1 > 0 & n2 > 0 holds
{ x where x is positive Nat : x solves_CRT a1,n1,a2,n2 } is infinite

proof end;

theorem :: NUMBER14:29

for a1, a2 being Integer
for n1, n2 being Nat st n1,n2 are_coprime & n1 > 0 & n2 > 0 holds
{ x where x is Nat : x solves_CRT a1,n1,a2,n2 } is infinite

proof end;

definition

let u, m be integer-valued FinSequence;
let z be Integer;

pred z solves_CRT u,m means :: NUMBER14:def 3
for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i;

end;

:: deftheorem defines solves_CRT NUMBER14:def 3 :
for u, m being integer-valued FinSequence
for z being Integer holds
( z solves_CRT u,m iff for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i );

definition

let u be integer-valued FinSequence;
let m be CR_Sequence;
assume A1: dom u = dom m ;

func CRT (u,m) -> Element of NAT means :Def4: :: NUMBER14:def 4
( it solves_CRT u,m & it < Product m );

existence
ex b₁ being Element of NAT st
( b₁ solves_CRT u,m & b₁ < Product m )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st b₁ solves_CRT u,m & b₁ < Product m & b₂ solves_CRT u,m & b₂ < Product m holds
b₁ = b₂ by A1, INT_6:42;

end;

:: deftheorem Def4 defines CRT NUMBER14:def 4 :
for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
for b₃ being Element of NAT holds
( b₃ = CRT (u,m) iff ( b₃ solves_CRT u,m & b₃ < Product m ) );

theorem Th30: :: NUMBER14:30

for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
for z being Integer st z solves_CRT u,m holds
for k being Integer holds z + (k * (Product m)) solves_CRT u,m

proof end;

theorem Th31: :: NUMBER14:31

for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
{ z where z is positive Nat : z solves_CRT u,m } is infinite

proof end;

theorem :: NUMBER14:32

for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
{ z where z is Nat : z solves_CRT u,m } is infinite

proof end;

definition

let a, b, c be Integer;

pred two_or_more_are_even_among a,b,c means :: NUMBER14:def 5
( ( a is even & b is even & c is odd ) or ( a is even & b is odd & c is even ) or ( a is odd & b is even & c is even ) or ( a is even & b is even & c is even ) );

pred two_or_more_are_odd_among a,b,c means :: NUMBER14:def 6
( ( a is odd & b is odd & c is even ) or ( a is odd & b is even & c is odd ) or ( a is even & b is odd & c is odd ) or ( a is odd & b is odd & c is odd ) );

end;

:: deftheorem defines two_or_more_are_even_among NUMBER14:def 5 :
for a, b, c being Integer holds
( two_or_more_are_even_among a,b,c iff ( ( a is even & b is even & c is odd ) or ( a is even & b is odd & c is even ) or ( a is odd & b is even & c is even ) or ( a is even & b is even & c is even ) ) );

:: deftheorem defines two_or_more_are_odd_among NUMBER14:def 6 :
for a, b, c being Integer holds
( two_or_more_are_odd_among a,b,c iff ( ( a is odd & b is odd & c is even ) or ( a is odd & b is even & c is odd ) or ( a is even & b is odd & c is odd ) or ( a is odd & b is odd & c is odd ) ) );

definition

let a, b, c, n be Integer;

pred a,b,c give_three_different_remainders_upon_dividing_by n means :: NUMBER14:def 7
a mod n,b mod n,c mod n are_mutually_distinct ;

pred a,b,c at_least_two_are_not_divisible_by n means :: NUMBER14:def 8
( ( not n divides a & not n divides b & n divides c ) or ( not n divides a & n divides b & not n divides c ) or ( n divides a & not n divides b & not n divides c ) or ( not n divides a & not n divides b & not n divides c ) );

end;

:: deftheorem defines give_three_different_remainders_upon_dividing_by NUMBER14:def 7 :
for a, b, c, n being Integer holds
( a,b,c give_three_different_remainders_upon_dividing_by n iff a mod n,b mod n,c mod n are_mutually_distinct );

:: deftheorem defines at_least_two_are_not_divisible_by NUMBER14:def 8 :
for a, b, c, n being Integer holds
( a,b,c at_least_two_are_not_divisible_by n iff ( ( not n divides a & not n divides b & n divides c ) or ( not n divides a & n divides b & not n divides c ) or ( n divides a & not n divides b & not n divides c ) or ( not n divides a & not n divides b & not n divides c ) ) );

definition

let a, b, c be Integer;

func numberR (a,b,c) -> Element of NAT equals :Def9: :: NUMBER14:def 9
1 if two_or_more_are_even_among a,b,c
otherwise 0 ;

correctness
coherence
( ( two_or_more_are_even_among a,b,c implies 1 is Element of NAT ) & ( not two_or_more_are_even_among a,b,c implies 0 is Element of NAT ) );
consistency
for b₁ being Element of NAT holds verum;
;

end;

:: deftheorem Def9 defines numberR NUMBER14:def 9 :
for a, b, c being Integer holds
( ( two_or_more_are_even_among a,b,c implies numberR (a,b,c) = 1 ) & ( not two_or_more_are_even_among a,b,c implies numberR (a,b,c) = 0 ) );

theorem Th33: :: NUMBER14:33

for a, b, c being Integer
for r being Nat st r = numberR (a,b,c) holds
two_or_more_are_odd_among a + r,b + r,c + r

proof end;

definition

let a, b, c be Integer;

func numberR0 (a,b,c) -> Element of INT equals :Def10: :: NUMBER14:def 10
0 if a,b,c give_three_different_remainders_upon_dividing_by 3
1 - (a mod 3) if ( a mod 3 = b mod 3 or a mod 3 = c mod 3 )
otherwise 1 - (b mod 3);

coherence
( ( a,b,c give_three_different_remainders_upon_dividing_by 3 implies 0 is Element of INT ) & ( ( a mod 3 = b mod 3 or a mod 3 = c mod 3 ) implies 1 - (a mod 3) is Element of INT ) & ( a,b,c give_three_different_remainders_upon_dividing_by 3 or a mod 3 = b mod 3 or a mod 3 = c mod 3 or 1 - (b mod 3) is Element of INT ) ) by INT_1:def 2;
consistency
for b₁ being Element of INT st a,b,c give_three_different_remainders_upon_dividing_by 3 & ( a mod 3 = b mod 3 or a mod 3 = c mod 3 ) holds
( b₁ = 0 iff b₁ = 1 - (a mod 3) ) by ZFMISC_1:def 5;

end;

:: deftheorem Def10 defines numberR0 NUMBER14:def 10 :
for a, b, c being Integer holds
( ( a,b,c give_three_different_remainders_upon_dividing_by 3 implies numberR0 (a,b,c) = 0 ) & ( ( a mod 3 = b mod 3 or a mod 3 = c mod 3 ) implies numberR0 (a,b,c) = 1 - (a mod 3) ) & ( a,b,c give_three_different_remainders_upon_dividing_by 3 or a mod 3 = b mod 3 or a mod 3 = c mod 3 or numberR0 (a,b,c) = 1 - (b mod 3) ) );

theorem Th34: :: NUMBER14:34

for a, b, c, r0 being Integer st r0 = numberR0 (a,b,c) holds
a + r0,b + r0,c + r0 at_least_two_are_not_divisible_by 3

proof end;

definition

let h be Integer;

func PrimeDivisors>3 h -> Subset of NAT equals :: NUMBER14:def 11
(PrimeDivisors h) /\ (GreaterOrEqualsNumbers 4);

coherence
(PrimeDivisors h) /\ (GreaterOrEqualsNumbers 4) is Subset of NAT ;

end;

:: deftheorem defines PrimeDivisors>3 NUMBER14:def 11 :
for h being Integer holds PrimeDivisors>3 h = (PrimeDivisors h) /\ (GreaterOrEqualsNumbers 4);

theorem Th35: :: NUMBER14:35

for h, i being Integer st i in PrimeDivisors>3 h holds
i > 3

proof end;

theorem Th36: :: NUMBER14:36

for h, i being Integer st i in PrimeDivisors>3 h holds
i divides h

proof end;

theorem Th37: :: NUMBER14:37

for h, i being Integer st i in PrimeDivisors>3 h holds
i is prime

proof end;

theorem Th38: :: NUMBER14:38

for h, i being Integer st i is prime & i > 3 & i divides h holds
i in PrimeDivisors>3 h

proof end;

theorem Th39: :: NUMBER14:39

for h being Integer st h <> 0 holds
PrimeDivisors>3 h c= Seg |.h.|

proof end;

registration

let h be non zero Integer;

cluster PrimeDivisors>3 h -> included_in_Seg ;

coherence
PrimeDivisors>3 h is included_in_Seg

proof end;

end;

theorem Th40: :: NUMBER14:40

for h being Integer st h <> 0 holds
for n being Nat st n in dom (Sgm (PrimeDivisors>3 h)) holds
(Sgm (PrimeDivisors>3 h)) . n > 3

proof end;

theorem :: NUMBER14:41

for h being Integer st h <> 0 holds
for n being Nat st n in dom (Sgm (PrimeDivisors>3 h)) holds
(Sgm (PrimeDivisors>3 h)) . n divides h

proof end;

theorem Th42: :: NUMBER14:42

for h being Integer st h <> 0 holds
for n being Nat st n in dom (Sgm (PrimeDivisors>3 h)) holds
(Sgm (PrimeDivisors>3 h)) . n is prime

proof end;

definition

let a, b, c be Integer;
assume A1: a,b,c are_mutually_distinct ;

mode Sierp45FS of a,b,c -> FinSequence of INT means :Def12: :: NUMBER14:def 12
ex h being Integer ex F being FinSequence of NAT st
( h = ((a - b) * (a - c)) * (b - c) & F = Sgm (PrimeDivisors>3 h) & len it = len F & ( for i being object st i in dom it holds
( not F . i divides a + (it . i) & not F . i divides b + (it . i) & not F . i divides c + (it . i) ) ) );

existence
ex b₁ being FinSequence of INT ex h being Integer ex F being FinSequence of NAT st
( h = ((a - b) * (a - c)) * (b - c) & F = Sgm (PrimeDivisors>3 h) & len b₁ = len F & ( for i being object st i in dom b₁ holds
( not F . i divides a + (b₁ . i) & not F . i divides b + (b₁ . i) & not F . i divides c + (b₁ . i) ) ) )

proof end;

end;

:: deftheorem Def12 defines Sierp45FS NUMBER14:def 12 :
for a, b, c being Integer st a,b,c are_mutually_distinct holds
for b₄ being FinSequence of INT holds
( b₄ is Sierp45FS of a,b,c iff ex h being Integer ex F being FinSequence of NAT st
( h = ((a - b) * (a - c)) * (b - c) & F = Sgm (PrimeDivisors>3 h) & len b₄ = len F & ( for i being object st i in dom b₄ holds
( not F . i divides a + (b₄ . i) & not F . i divides b + (b₄ . i) & not F . i divides c + (b₄ . i) ) ) ) );

Lm7: for a, b, c, h being Integer st h = ((a - b) * (a - c)) * (b - c) holds
for S being Sierp45FS of a,b,c
for n being Nat st a,b,c are_mutually_distinct & n, numberR (a,b,c) are_congruent_mod 2 & n, numberR0 (a,b,c) are_congruent_mod 3 & ( for i being Nat st i in dom S holds
n,S . i are_congruent_mod (Sgm (PrimeDivisors>3 h)) . i ) holds
a + n,b + n are_coprime

proof end;

Lm8: for a, b, c, h being Integer st h = ((a - b) * (a - c)) * (b - c) holds
for S being Sierp45FS of a,b,c
for n being Nat st a,b,c are_mutually_distinct & n, numberR (a,b,c) are_congruent_mod 2 & n, numberR0 (a,b,c) are_congruent_mod 3 & ( for i being Nat st i in dom S holds
n,S . i are_congruent_mod (Sgm (PrimeDivisors>3 h)) . i ) holds
a + n,c + n are_coprime

proof end;

Lm9: for a, b, c, h being Integer st h = ((a - b) * (a - c)) * (b - c) holds
for S being Sierp45FS of a,b,c
for n being Nat st a,b,c are_mutually_distinct & n, numberR (a,b,c) are_congruent_mod 2 & n, numberR0 (a,b,c) are_congruent_mod 3 & ( for i being Nat st i in dom S holds
n,S . i are_congruent_mod (Sgm (PrimeDivisors>3 h)) . i ) holds
b + n,c + n are_coprime

proof end;

theorem Th43: :: NUMBER14:43

for a, b, c, h being Integer st h = ((a - b) * (a - c)) * (b - c) holds
for S being Sierp45FS of a,b,c st a,b,c are_mutually_distinct holds
for n being Nat st n, numberR (a,b,c) are_congruent_mod 2 & n, numberR0 (a,b,c) are_congruent_mod 3 & ( for i being Nat st i in dom S holds
n,S . i are_congruent_mod (Sgm (PrimeDivisors>3 h)) . i ) holds
a + n,b + n,c + n are_mutually_coprime

proof end;

Lm10: now :: thesis: for n being Nat st n >= 1 & n <> 1 & n <> 2 holds
not n <= 2

let n be Nat; :: thesis: ( n >= 1 & n <> 1 & n <> 2 implies not n <= 2 )
assume A1: ( n >= 1 & n <> 1 & n <> 2 ) ; :: thesis: not n <= 2
assume n <= 2 ; :: thesis: contradiction
then not not n = 0 & ... & not n = 2 ;
hence contradiction by A1; :: thesis: verum

end;

theorem Th44: :: NUMBER14:44

for h being Integer st h <> 0 holds
rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) c= SetPrimes

proof end;

theorem Th45: :: NUMBER14:45

for h being Integer st h <> 0 holds
<*2,3*> ^ (Sgm (PrimeDivisors>3 h)) is Chinese_Remainder

proof end;

:: Problem 45

theorem :: NUMBER14:46

for a, b, c being Integer st a,b,c are_mutually_distinct holds
{ n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } is infinite

proof end;

registration

let n be non zero Nat;

cluster PrimeDivisors n -> finite ;

coherence
PrimeDivisors n is finite

proof end;

end;

registration

let n be non zero Nat;

cluster PrimeDivisors n -> included_in_Seg ;

coherence
PrimeDivisors n is included_in_Seg

proof end;

end;

registration

let X be non trivial natural-membered set ;

cluster non empty included_in_Seg complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered for Element of bool X;

existence
ex b₁ being Subset of X st
( not b₁ is empty & b₁ is included_in_Seg )

proof end;

end;

registration

let X be non empty included_in_Seg Subset of SetPrimes;

cluster Sgm X -> non empty ;

coherence
not Sgm X is empty

proof end;

end;

registration

let X be included_in_Seg Subset of SetPrimes;
set f = Sgm X;
A1: rng (Sgm X) = X by FINSEQ_1:def 14;

cluster Sgm X -> positive-yielding ;

coherence
Sgm X is positive-yielding

proof end;

cluster Sgm X -> Chinese_Remainder ;

coherence
Sgm X is Chinese_Remainder

proof end;

end;

definition

let n be non zero Nat;

func PrimeDivisorsFS n -> FinSequence of SetPrimes equals :: NUMBER14:def 13
Sgm (PrimeDivisors n);

coherence
Sgm (PrimeDivisors n) is FinSequence of SetPrimes

proof end;

end;

:: deftheorem defines PrimeDivisorsFS NUMBER14:def 13 :
for n being non zero Nat holds PrimeDivisorsFS n = Sgm (PrimeDivisors n);

registration

let n be non zero Nat;

cluster PrimeDivisorsFS n -> increasing ;

coherence
PrimeDivisorsFS n is increasing ;

end;

theorem Th47: :: NUMBER14:47

for n being non zero Nat
for i being Nat st i in dom (PrimeDivisorsFS n) holds
(PrimeDivisorsFS n) . i is prime

proof end;

definition

let m be non zero Nat;
let k be Nat;

mode Sierp49FS of m,k -> FinSequence of INT means :Def14: :: NUMBER14:def 14
( len it = len (PrimeDivisorsFS m) & ( for i being object st i in dom it holds
not (PrimeDivisorsFS m) . i divides (it . i) * ((it . i) + (2 * k)) ) );

existence
ex b₁ being FinSequence of INT st
( len b₁ = len (PrimeDivisorsFS m) & ( for i being object st i in dom b₁ holds
not (PrimeDivisorsFS m) . i divides (b₁ . i) * ((b₁ . i) + (2 * k)) ) )

proof end;

end;

:: deftheorem Def14 defines Sierp49FS NUMBER14:def 14 :
for m being non zero Nat
for k being Nat
for b₃ being FinSequence of INT holds
( b₃ is Sierp49FS of m,k iff ( len b₃ = len (PrimeDivisorsFS m) & ( for i being object st i in dom b₃ holds
not (PrimeDivisorsFS m) . i divides (b₃ . i) * ((b₃ . i) + (2 * k)) ) ) );

registration

let n be non zero Nat;

cluster PrimeDivisorsFS n -> positive-yielding Chinese_Remainder ;

coherence
( PrimeDivisorsFS n is Chinese_Remainder & PrimeDivisorsFS n is positive-yielding )

proof end;

end;

registration

cluster PrimeDivisorsFS 1 -> empty ;

coherence
PrimeDivisorsFS 1 is empty

proof end;

end;

theorem Th48: :: NUMBER14:48

for n being non zero Nat holds support (pfexp n) = PrimeDivisors n

proof end;

theorem Th49: :: NUMBER14:49

for n being non zero Nat st PrimeDivisors n is empty holds
n = 1

proof end;

theorem Th50: :: NUMBER14:50

for n being non zero Nat st PrimeDivisorsFS n is empty holds
n = 1

proof end;

registration

let n be non trivial Nat;
A1: n <> 1 by NAT_2:29;

cluster PrimeDivisors n -> non empty ;

coherence
not PrimeDivisors n is empty by A1, Th49;

cluster PrimeDivisorsFS n -> non empty ;

coherence
not PrimeDivisorsFS n is empty by A1, Th50;

end;

theorem Th51: :: NUMBER14:51

for n being non zero Nat holds PrimeDivisorsFS n = sort_a (canFS (support (pfexp n)))

proof end;

theorem Th52: :: NUMBER14:52

for n being non zero Nat holds PrimeDivisorsFS n = sort_a (canFS (support (ppf n)))

proof end;

theorem Th53: :: NUMBER14:53

for j being Integer st j <> 0 holds
for n being positive Nat st ( for i being Nat st i in dom (PrimeDivisorsFS n) holds
j,(PrimeDivisorsFS n) . i are_coprime ) holds
j,n are_coprime

proof end;

:: Problem 49 with example solution

theorem Th54: :: NUMBER14:54

for m being positive Nat
for k being Nat
for S being Sierp49FS of m,k
for q being CR_Sequence st q = PrimeDivisorsFS m holds
ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime & a = ((CRT (S,q)) + (Product q)) + (2 * k) & b = (CRT (S,q)) + (Product q) )

proof end;

:: Problem 49

theorem :: NUMBER14:55

for m being positive Nat
for k being Nat ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime )

proof end;

:: Problem 120

theorem :: NUMBER14:56

for m being non zero Nat ex s being Nat st
for n being Nat st n > s holds
((2 |^ m) * (2 |^ (2 |^ n))) + 1 is composite

proof end;

definition

let i be Integer;

mode Multiple of i -> Integer means :Def15: :: NUMBER14:def 15
i divides it;

existence
ex b₁ being Integer st i divides b₁ ;

end;

:: deftheorem Def15 defines Multiple NUMBER14:def 15 :
for i, b₂ being Integer holds
( b₂ is Multiple of i iff i divides b₂ );

theorem Th57: :: NUMBER14:57

for i, j being Integer holds i * j is Multiple of i

proof end;

theorem Th58: :: NUMBER14:58

for h, i, j being Integer st j is Multiple of i holds
j + (h * i) is Multiple of i

proof end;

theorem Th59: :: NUMBER14:59

for i being Integer st i <> 1 & i <> - 1 holds
for m being Multiple of i holds
( not m is prime or m = i or m = - i )

proof end;

theorem Th60: :: NUMBER14:60

for n being Nat st n <> 1 holds
for m being Multiple of n st m is prime holds
m = n

proof end;

definition

let i be Integer;

func multiples i -> Subset of INT equals :: NUMBER14:def 16
{ m where m is Multiple of i : verum } ;

coherence
{ m where m is Multiple of i : verum } is Subset of INT

proof end;

end;

:: deftheorem defines multiples NUMBER14:def 16 :
for i being Integer holds multiples i = { m where m is Multiple of i : verum } ;

theorem Th61: :: NUMBER14:61

for i being Integer
for x being object st x in multiples i holds
x is Multiple of i

proof end;

theorem Th62: :: NUMBER14:62

for i, j being Integer holds
( j in multiples i iff i divides j )

proof end;

theorem Th63: :: NUMBER14:63

for i, j being Integer holds i * j in multiples i

proof end;

registration

let i be Integer;

cluster multiples i -> non empty ;

coherence
not multiples i is empty by Th63;

end;

theorem :: NUMBER14:64

multiples 0 = {0}

proof end;

theorem :: NUMBER14:65

multiples 1 = INT

proof end;

theorem :: NUMBER14:66

multiples (- 1) = INT

proof end;

registration

let i be non zero Integer;

cluster i (#) (id INT) -> one-to-one ;

coherence
i (#) (id INT) is one-to-one

proof end;

end;

theorem Th67: :: NUMBER14:67

for i being non zero Integer holds INT , multiples i are_equipotent

proof end;

registration

let i be non zero Integer;

cluster multiples i -> infinite ;

coherence
not multiples i is finite

proof end;

end;

theorem :: NUMBER14:68

for i being Integer st i <> 1 & i <> - 1 & not i is prime & not - i is prime holds
multiples i misses SetPrimes

proof end;

definition

let m, n be Nat;

func primeNumbers (m,n) -> Subset of NAT equals :: NUMBER14:def 17
(seq (m,n)) /\ SetPrimes;

coherence
(seq (m,n)) /\ SetPrimes is Subset of NAT ;

end;

:: deftheorem defines primeNumbers NUMBER14:def 17 :
for m, n being Nat holds primeNumbers (m,n) = (seq (m,n)) /\ SetPrimes;

registration

let m, n be Nat;

cluster primeNumbers (m,n) -> finite ;

coherence
primeNumbers (m,n) is finite ;

end;

theorem Th69: :: NUMBER14:69

primeNumbers (0,10) = {2,3,5,7}

proof end;

theorem Th70: :: NUMBER14:70

primeNumbers (1,10) = {2,3,5,7,11}

proof end;

theorem Th71: :: NUMBER14:71

primeNumbers (2,10) = {3,5,7,11}

proof end;

theorem :: NUMBER14:72

primeNumbers (3,10) = {5,7,11,13}

proof end;

theorem Th73: :: NUMBER14:73

for m, n being Nat holds card (seq (m,n)) = n

proof end;

theorem Th74: :: NUMBER14:74

for m, n being Nat holds seq (m,n) misses {((m + n) + 1),((m + n) + 2)}

proof end;

theorem Th75: :: NUMBER14:75

for a being Integer st a is even holds
a is Multiple of 2

proof end;

theorem Th76: :: NUMBER14:76

for a being Integer st a is even holds
a in multiples 2

proof end;

theorem Th77: :: NUMBER14:77

for a being Integer st a is odd holds
not a is Multiple of 2

proof end;

theorem :: NUMBER14:78

for a being Integer st a is odd holds
not a in multiples 2

proof end;

theorem Th79: :: NUMBER14:79

for a being Integer st a is even holds
(multiples 2) /\ {a,(a + 1)} = {a}

proof end;

theorem Th80: :: NUMBER14:80

for a being Integer st a is odd holds
(multiples 2) /\ {a,(a + 1)} = {(a + 1)}

proof end;

theorem :: NUMBER14:81

for a being Integer holds
( (multiples 2) /\ {a,(a + 1)} = {a} or (multiples 2) /\ {a,(a + 1)} = {(a + 1)} ) by Th79, Th80;

theorem Th82: :: NUMBER14:82

for a being Integer holds card ((multiples 2) /\ {a,(a + 1)}) = 1

proof end;

theorem Th83: :: NUMBER14:83

for k, m being Nat holds card ((multiples 2) /\ (seq (k,(2 * m)))) = m

proof end;

theorem Th84: :: NUMBER14:84

for k, n being Nat st n >= 8 holds
ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

proof end;

theorem :: NUMBER14:85

for k, m being Nat
for p being Prime st p <= k holds
(multiples p) /\ (seq (k,m)) misses primeNumbers (k,m)

proof end;

:: Problem 131 a

theorem :: NUMBER14:86

card (primeNumbers (0,10)) = 4 by Th69, CARD_2:59;

:: Problem 131 b

theorem :: NUMBER14:87

card (primeNumbers (1,10)) = 5

proof end;

:: Problem 131 c

theorem :: NUMBER14:88

for k being Nat st 2 <= k holds
card (primeNumbers (k,10)) <= 4

proof end;

Lm11: for D being odd Integer holds { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } is infinite

proof end;

registration

let A be set ;

cluster -> even for Element of EvenNAT \ A;

coherence
for b₁ being Element of EvenNAT \ A holds b₁ is even

proof end;

end;

registration

let A be set ;

cluster epsilon-transitive epsilon-connected ordinal natural complex real integer dim-like finite cardinal even ext-real non negative rational for Element of EvenNAT \ A;

existence
ex b₁ being Element of EvenNAT \ A st b₁ is even

proof end;

end;

Lm12: for D being even Integer holds { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } is infinite

proof end;

:: Problem 144

theorem :: NUMBER14:89

for D being non zero Integer holds { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } is infinite

proof end;

theorem :: NUMBER14:90

for x, y, z being Complex holds
( (((((x ^2) + (y ^2)) + (z ^2)) + x) + y) + z = 1 iff ((((2 * x) + 1) ^2) + (((2 * y) + 1) ^2)) + (((2 * z) + 1) ^2) = 7 ) ;

theorem Th91: :: NUMBER14:91

for a, b, c being Integer st (((a ^2) + (b ^2)) + (c ^2)) mod 4 = 0 holds
( a is even & b is even & c is even )

proof end;

theorem Th92: :: NUMBER14:92

for a, b, c being Integer holds
( (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 )

proof end;

theorem Th93: :: NUMBER14:93

for x, y, z being Rational holds not ((x ^2) + (y ^2)) + (z ^2) = 7

proof end;

:: Problem 148

theorem :: NUMBER14:94

for x, y, z being Rational holds not (((((x ^2) + (y ^2)) + (z ^2)) + x) + y) + z = 1

proof end;

:: Problem 149 a

theorem :: NUMBER14:95

for x, y, z being positive Integer holds not (((4 * x) * y) - x) - y = z ^2

proof end;

deffunc H₁( Nat) -> object = - 1;

deffunc H₂( Nat) -> set = (- (5 * ($1 ^2))) - (2 * $1);

deffunc H₃( Nat) -> set = (- (5 * $1)) - 1;

deffunc H₄( Nat) -> object = [H₁($1),H₂($1),H₃($1)];

definition

func exampleSierpinski149 -> Function of NATPLUS,[:INT,INT,INT:] means :Def18: :: NUMBER14:def 18
for n being non zero Nat holds it . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)];

existence
ex b₁ being Function of NATPLUS,[:INT,INT,INT:] st
for n being non zero Nat holds b₁ . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)]

proof end;

uniqueness
for b₁, b₂ being Function of NATPLUS,[:INT,INT,INT:] st ( for n being non zero Nat holds b₁ . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)] ) & ( for n being non zero Nat holds b₂ . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines exampleSierpinski149 NUMBER14:def 18 :
for b₁ being Function of NATPLUS,[:INT,INT,INT:] holds
( b₁ = exampleSierpinski149 iff for n being non zero Nat holds b₁ . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)] );

set f = exampleSierpinski149 ;

registration

cluster exampleSierpinski149 -> one-to-one ;

coherence
exampleSierpinski149 is one-to-one

proof end;

end;

theorem Th96: :: NUMBER14:96

rng exampleSierpinski149 c= { [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 }

proof end;

:: Problem 149 b

theorem :: NUMBER14:97

{ [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 } is infinite

proof end;

definition

let m, D be Complex;
set R = [:COMPLEX,COMPLEX:];

func exampleSierpinski150 (m,D) -> sequence of [:COMPLEX,COMPLEX:] means :Def19: :: NUMBER14:def 19
( it . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds it . (n + 1) = [((((it . n) `1) ^2) + (D * (((it . n) `2) ^2))),((2 * ((it . n) `1)) * ((it . n) `2))] ) );

existence
ex b₁ being sequence of [:COMPLEX,COMPLEX:] st
( b₁ . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds b₁ . (n + 1) = [((((b₁ . n) `1) ^2) + (D * (((b<sub>1</sub> . n) `2) ^2))),((2 * ((b₁ . n) `1)) * ((b<sub>1</sub> . n) `2))] ) )

proof end;

uniqueness
for b₁, b₂ being sequence of [:COMPLEX,COMPLEX:] st b₁ . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds b₁ . (n + 1) = [((((b₁ . n) `1) ^2) + (D * (((b<sub>1</sub> . n) `2) ^2))),((2 * ((b₁ . n) `1)) * ((b<sub>1</sub> . n) `2))] ) & b₂ . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds b₂ . (n + 1) = [((((b₂ . n) `1) ^2) + (D * (((b<sub>2</sub> . n) `2) ^2))),((2 * ((b₂ . n) `1)) * ((b<sub>2</sub> . n) `2))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines exampleSierpinski150 NUMBER14:def 19 :
for m, D being Complex
for b₃ being sequence of [:COMPLEX,COMPLEX:] holds
( b₃ = exampleSierpinski150 (m,D) iff ( b₃ . 0 = [((2 * (m ^2)) + 1),(2 * m)] & ( for n being Nat holds b₃ . (n + 1) = [((((b₃ . n) `1) ^2) + (D * (((b<sub>3</sub> . n) `2) ^2))),((2 * ((b₃ . n) `1)) * ((b<sub>3</sub> . n) `2))] ) ) );

registration

let m, D be Real;

cluster exampleSierpinski150 (m,D) -> [:REAL,REAL:] -valued ;

coherence
exampleSierpinski150 (m,D) is [:REAL,REAL:] -valued

proof end;

end;

registration

let m, D be Rational;

cluster exampleSierpinski150 (m,D) -> [:RAT,RAT:] -valued ;

coherence
exampleSierpinski150 (m,D) is [:RAT,RAT:] -valued

proof end;

end;

registration

let m, D be Integer;

cluster exampleSierpinski150 (m,D) -> [:INT,INT:] -valued ;

coherence
exampleSierpinski150 (m,D) is [:INT,INT:] -valued

proof end;

end;

registration

let m, D be Nat;

cluster exampleSierpinski150 (m,D) -> [:NAT,NAT:] -valued ;

coherence
exampleSierpinski150 (m,D) is [:NAT,NAT:] -valued

proof end;

end;

registration

let m, D be natural positive Number ;
let n be Nat;
set f = exampleSierpinski150 (m,D);

cluster ((exampleSierpinski150 (m,D)) . n) `1 -> positive ;

coherence
((exampleSierpinski150 (m,D)) . n) `1 is positive

proof end;

cluster ((exampleSierpinski150 (m,D)) . n) `2 -> positive ;

coherence
((exampleSierpinski150 (m,D)) . n) `2 is positive

proof end;

end;

theorem Th98: :: NUMBER14:98

for m, D being natural positive Number
for a, b being Nat st a < b holds
( ((exampleSierpinski150 (m,D)) . a) `1 < ((exampleSierpinski150 (m,D)) . b) `1 & ((exampleSierpinski150 (m,D)) . a) `2 < ((exampleSierpinski150 (m,D)) . b) `2 )

proof end;

registration

let m, D be natural positive Number ;

cluster exampleSierpinski150 (m,D) -> one-to-one ;

coherence
exampleSierpinski150 (m,D) is one-to-one

proof end;

end;

:: Problem 150

theorem :: NUMBER14:99

for D, m being positive Integer st D = (m ^2) + 1 holds
{ [x,y] where x, y is positive Integer : (x ^2) - (D * (y ^2)) = 1 } is infinite

proof end;

theorem Th100: :: NUMBER14:100

for n being Nat
for i being Integer st 2 |^ 2 <= n & 2 |^ n divides i |^ 3 holds
2 |^ 2 divides i

proof end;

theorem Th101: :: NUMBER14:101

for n being Nat
for i being Integer st 2 |^ 3 <= n & 2 |^ n divides i |^ 3 holds
2 |^ 3 divides i

proof end;

theorem Th102: :: NUMBER14:102

for n being Nat
for i, j being Integer
for p being Prime st i,j are_coprime & p |^ n divides i * j & not p |^ n divides i holds
p |^ n divides j

proof end;

theorem Th103: :: NUMBER14:103

for n being Nat
for i, j, z being Integer st n is odd & i,j are_coprime & i * j = z |^ n holds
ex k being Integer st i = k |^ n

proof end;

theorem Th104: :: NUMBER14:104

for n being Nat st n is odd holds
for r, s being negative Real st r <= s holds
r |^ n <= s |^ n

proof end;

theorem Th105: :: NUMBER14:105

for j, z being Integer st 0 <= j & j ^2 < z & z < (j + 1) ^2 holds
for i being Integer holds not z = i ^2

proof end;

Lm13: for i being Integer holds not i ^2 = 464

proof end;

:: Problem 151

theorem :: NUMBER14:106

{ [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } = {[0,4],[0,(- 4)]}

proof end;

theorem Th107: :: NUMBER14:107

for m being Complex
for x, y, z being non zero Complex holds
( ((x / y) + (y / z)) + (z / x) = m iff (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z )

proof end;

theorem Th108: :: NUMBER14:108

for m being Integer
for x, y, z being non zero Integer st ((x / y) + (y / z)) + (z / x) = m & x,y,z are_mutually_coprime holds
( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) )

proof end;

theorem :: NUMBER14:109

for m being Integer
for x, y, z being positive Integer st ((x / y) + (y / z)) + (z / x) = m & x,y,z are_mutually_coprime holds
( x = 1 & y = 1 & z = 1 ) by Th108;

Lm14: ((1 / 1) + (1 / 1)) + (1 / 1) = 3
;

Lm15: (((- 1) / (- 1)) + ((- 1) / (- 1))) + ((- 1) / (- 1)) = 3
;

:: Problem 152 a

theorem :: NUMBER14:110

{ [x,y,z] where x, y, z is positive Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } = {[1,1,1]}

proof end;

:: Problem 152 b

theorem :: NUMBER14:111

{ [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } = {[1,1,1],[(- 1),(- 1),(- 1)]}

proof end;

:: Problem 152 c

theorem :: NUMBER14:112

for m being Nat st m <> 3 holds
for x, y, z being non zero Integer holds
( not ((x / y) + (y / z)) + (z / x) = m or not x,y,z are_mutually_coprime )

proof end;