NUMBER03: Elementary Number Theory Problems. Part III

:: Elementary Number Theory Problems. Part III
:: by Artur Korni{\l}owicz
::
:: Received July 23, 2022
:: Copyright (c) 2022-2024 Association of Mizar Users

registration

cluster natural -> natural-membered for set ;

coherence

proof end;

end;

theorem Th1: :: NUMBER03:1

for e1, e2, e3, e4 being ExtReal st e1 <= e2 & e2 <= e3 & e3 <= e4 holds
e1 <= e4

proof end;

theorem Th2: :: NUMBER03:2

for e1, e2, e3, e4, e5 being ExtReal st e1 <= e2 & e2 <= e3 & e3 <= e4 & e4 <= e5 holds
e1 <= e5

proof end;

theorem :: NUMBER03:3

(2 |^ 10) + 1 = 1025

proof end;

theorem Th4: :: NUMBER03:4

(3 |^ 10) + 1 = 5905 * 10

proof end;

theorem Th5: :: NUMBER03:5

(4 |^ 10) + 1 = (1048 * 1000) + 577

proof end;

theorem Th6: :: NUMBER03:6

(5 |^ 10) + 1 = (9765 * 1000) + 626

proof end;

theorem Th7: :: NUMBER03:7

(6 |^ 10) + 1 = (6046 * 10000) + 6177

proof end;

theorem Th8: :: NUMBER03:8

(7 |^ 10) + 1 = ((2824 * 10000) + 7525) * 10

proof end;

theorem Th9: :: NUMBER03:9

(8 |^ 10) + 1 = (((1073 * 100) + 74) * 10000) + 1825

proof end;

theorem Th10: :: NUMBER03:10

(9 |^ 10) + 1 = (((3486 * 100) + 78) * 10000) + 4402

proof end;

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

Lm2: 2 mod 3 = 2
by NAT_D:24;

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

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

Lm5: ((3 * 10) + 2) mod 3 = 2 mod 3
by NAT_D:21;

Lm6: 1 mod 4 = 1
by NAT_D:24;

Lm7: 2 mod 4 = 2
by NAT_D:24;

Lm8: 3 mod 4 = 3
by NAT_D:24;

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

Lm10: ((1 * 5) + 2) mod 5 = 2 mod 5
by NAT_D:21;

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

Lm12: ((6 * 5) + 2) mod 5 = 2 mod 5
by NAT_D:21;

Lm13: 1 mod 5 = 1
by NAT_D:24;

Lm14: 2 mod 5 = 2
by NAT_D:24;

Lm15: 3 mod 5 = 3
by NAT_D:24;

Lm16: 4 mod 5 = 4
by NAT_D:24;

theorem Th11: :: NUMBER03:11

for m being Nat
for n being Integer holds
not not n mod (m + 1) = 0 & ... & not n mod (m + 1) = m

proof end;

Lm17: for a being Nat holds
( ( 3 divides a & not a mod 3 <> 0 ) or a mod 3 = 1 or a mod 3 = 2 )

proof end;

Lm18: for a being Nat holds
( ( 5 divides a & not a mod 5 <> 0 ) or a mod 5 = 1 or a mod 5 = 2 or a mod 5 = 3 or a mod 5 = 4 )

proof end;

theorem Th12: :: NUMBER03:12

for n being Nat st n divides 8 holds
n in {1,2,4,8}

proof end;

theorem Th13: :: NUMBER03:13

for m, n being Nat st 0 < m holds
m gcd n <= m

proof end;

theorem Th14: :: NUMBER03:14

for i, j being Integer holds
( not i,j are_coprime or i <> j or ( i = j & j = 1 ) or ( i = j & j = - 1 ) )

proof end;

theorem :: NUMBER03:15

for i, j being Nat holds
( not i,j are_coprime or i <> j or ( i = j & j = 1 ) ) by Th14;

theorem Th16: :: NUMBER03:16

for a, b, n being Nat st a < n & b < n & n divides a - b holds
a = b

proof end;

theorem Th17: :: NUMBER03:17

for a, b, m being Integer st a < b holds
ex k being Nat st
( m < (((b - a) * k) + 1) - a & k = |.[/((((m + a) - 1) / (b - a)) + 1)\].| )

proof end;

Lm19: not 2 divides 1025

proof end;

Lm20: not 2 divides (1048 * 1000) + 577

proof end;

Lm21: not 5 divides (9765 * 1000) + 626

proof end;

Lm22: not 2 divides (6046 * 10000) + 6177

proof end;

Lm23: not 2 divides (((1073 * 100) + 74) * 10000) + 1825

proof end;

Lm24: not 5 divides (((3486 * 100) + 78) * 10000) + 4402

proof end;

Lm25: not 2 * 5 divides 1025
by Lm19, NEWTON03:11;

Lm26: not 2 * 5 divides (1048 * 1000) + 577
by Lm20, NEWTON03:11;

Lm27: not 2 * 5 divides (9765 * 1000) + 626
by Lm21, NEWTON03:11;

Lm28: not 2 * 5 divides (6046 * 10000) + 6177
by Lm22, NEWTON03:11;

Lm29: not 2 * 5 divides (((1073 * 100) + 74) * 10000) + 1825
by Lm23, NEWTON03:11;

Lm30: not 2 * 5 divides (((3486 * 100) + 78) * 10000) + 4402
by Lm24, NEWTON03:11;

registration

let i be Integer;

cluster i GeoSeq -> INT -valued ;

coherence

proof end;

end;

registration

let n be Nat;

cluster n GeoSeq -> NAT -valued ;

coherence

proof end;

end;

registration

let f be real-valued nonnegative-yielding ManySortedSet of NAT ;

cluster Partial_Sums f -> non-decreasing ;

coherence

proof end;

end;

theorem Th18: :: NUMBER03:18

for a, b being Nat st ( a <> 0 or b <> 0 ) holds
ex A, B being Nat st
( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime )

proof end;

theorem Th19: :: NUMBER03:19

for n being Nat st n <> 0 holds
for p, m being Integer st p divides m holds
p divides (m GeoSeq) . n

proof end;

theorem Th20: :: NUMBER03:20

for a, b being Nat
for r being Real holds (r GeoSeq) . (a + b) = ((r GeoSeq) . a) * (r |^ b)

proof end;

theorem Th21: :: NUMBER03:21

for n being Nat
for p, m being Integer st p divides m holds
p divides ((Partial_Sums (m GeoSeq)) . n) - 1

proof end;

theorem Th22: :: NUMBER03:22

for m, n being Nat holds (Partial_Sums (m GeoSeq)) . n,m |^ (n + 1) are_coprime

proof end;

theorem Th23: :: NUMBER03:23

for a, i, k being Nat holds ((Partial_Sums (a GeoSeq)) . k) gcd ((Partial_Sums (a GeoSeq)) . (k + i)) = ((Partial_Sums (a GeoSeq)) . k) gcd (((Partial_Sums (a GeoSeq)) . (k + i)) - ((Partial_Sums (a GeoSeq)) . k))

proof end;

theorem Th24: :: NUMBER03:24

for i, k being Nat
for r being Real holds ((Partial_Sums (r GeoSeq)) . ((k + i) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . i)

proof end;

Lm31: for m, n, x being Nat st n + 1,m + 1 are_coprime & n < m holds
(Partial_Sums (x GeoSeq)) . n,(Partial_Sums (x GeoSeq)) . m are_coprime

proof end;

theorem Th25: :: NUMBER03:25

for a, m, n being Nat st n + 1,m + 1 are_coprime holds
(Partial_Sums (a GeoSeq)) . n,(Partial_Sums (a GeoSeq)) . m are_coprime

proof end;

theorem Th26: :: NUMBER03:26

for a, b, i being Nat st a <> 0 & b <> 0 & i <> 0 holds
((i |^ a) - 1) gcd ((i |^ b) - 1) = (i |^ (a gcd b)) - 1

proof end;

theorem :: NUMBER03:27

for n being Nat
for a, b, k being Integer st a + b > 0 & (a mod k) + (b mod k) > 0 holds
((a + b) to_power n) mod k = (((a mod k) + (b mod k)) to_power n) mod k

proof end;

theorem Th28: :: NUMBER03:28

for n being Nat
for a, b, k being Integer holds ((a + b) |^ n) mod k = (((a mod k) + (b mod k)) |^ n) mod k

proof end;

theorem Th29: :: NUMBER03:29

for a, b, m being Nat st 1 < m holds
( m divides (a |^ b) + 1 iff m divides ((a mod m) |^ b) + 1 )

proof end;

theorem Th30: :: NUMBER03:30

for a being Nat holds
( 10 divides (a |^ 10) + 1 iff ex r, k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 ) )

proof end;

theorem Th31: :: NUMBER03:31

for a, b being odd Nat st a - b = 2 holds
a,b are_coprime

proof end;

theorem Th32: :: NUMBER03:32

for a, b, c being odd Nat st c - b = 2 & b - a = 2 & not 3 divides a & not 3 divides b holds
3 divides c

proof end;

theorem Th33: :: NUMBER03:33

for a, b, c being odd Prime st c - b = 2 & b - a = 2 holds
( a = 3 & b = 5 & c = 7 )

proof end;

theorem Th34: :: NUMBER03:34

for a, n being Nat st a |^ n is prime holds
n = 1

proof end;

theorem Th35: :: NUMBER03:35

for a, n being Nat st 1 < a holds
ex k being Nat st
( 1 < k & n < a |^ k )

proof end;

theorem :: NUMBER03:36

for n being Nat holds
( (2 |^ n) mod 3 = 1 or (2 |^ n) mod 3 = 2 )

proof end;

theorem Th37: :: NUMBER03:37

for m being Nat holds 3 |^ m divides (2 |^ (3 |^ m)) + 1

proof end;

theorem Th38: :: NUMBER03:38

Euler 0 = 0

proof end;

registration

cluster Euler 0 -> zero ;

coherence by Th38;

end;

registration

let n be positive Nat;

cluster Euler n -> positive ;

coherence

proof end;

end;

deffunc H₁( Nat) -> set = ((2 |^ ((2 * $1) + 1)) - (2 |^ ($1 + 1))) + 1;

deffunc H₂( Nat) -> Element of omega = ((2 |^ ((2 * $1) + 1)) + (2 |^ ($1 + 1))) + 1;

Lm32: now :: thesis:

let k be Nat; :: thesis:
(((2 * 2) * 2) * 2) mod 5 = 1 by Lm9, NAT_D:24;
then (2 |^ 4) mod 5 = 1 by POLYEQ_5:3;
hence ((2 |^ 4) |^ k) mod 5 = (1 |^ k) mod 5 by INT_4:8
.= 1 by NAT_D:24 ;
:: thesis:

end;

Lm33: now :: thesis:

let k be Nat; :: thesis:
A1: ((2 |^ 4) |^ k) mod 5 = 1 by Lm32;
A2: (2 |^ 4) |^ k = 2 |^ (4 * k) by NEWTON:9;
2 |^ (2 * (4 * k)) = (2 |^ (4 * k)) |^ 2 by NEWTON:9;
hence (2 |^ (2 * (4 * k))) mod 5 = ((1 |^ k) |^ 2) mod 5 by A1, A2, INT_4:8
.= 1 by NAT_D:24 ;
:: thesis:

end;

Lm34: now :: thesis:

let k be Nat; :: thesis:
set x = 2 |^ ((2 * (4 * k)) + 1);
set y = 2 |^ ((4 * k) + 1);
A1: (2 |^ (2 * (4 * k))) mod 5 = 1 by Lm33;
A2: ((2 |^ 4) |^ k) mod 5 = 1 by Lm32;
A3: (2 |^ 4) |^ k = 2 |^ (4 * k) by NEWTON:9;
2 |^ ((2 * (4 * k)) + 1) = 2 * (2 |^ (2 * (4 * k))) by NEWTON:6;
then A4: (2 |^ ((2 * (4 * k)) + 1)) mod 5 = (2 * 1) mod 5 by A1, Lm14, NAT_D:67
.= 2 by NAT_D:24 ;
2 |^ ((4 * k) + 1) = 2 * (2 |^ (4 * k)) by NEWTON:6;
then A5: (2 |^ ((4 * k) + 1)) mod 5 = (2 * 1) mod 5 by A2, A3, Lm14, NAT_D:67
.= 2 by NAT_D:24 ;
thus H₁(4 * k) mod 5 = ((((2 |^ ((2 * (4 * k)) + 1)) - (2 |^ ((4 * k) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((2 - 2) mod 5) + 1) mod 5 by A4, A5, INT_6:7
.= (0 + 1) mod 5
.= 1 by NAT_D:24 ; :: thesis:
thus H₂(4 * k) mod 5 = ((((2 |^ ((2 * (4 * k)) + 1)) + (2 |^ ((4 * k) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((2 + 2) mod 5) + 1) mod 5 by A4, A5, NAT_D:66
.= 0 by Lm16, INT_1:50 ; :: thesis:

end;

Lm35: now :: thesis:

let k be Nat; :: thesis:
set x = 2 |^ ((2 * ((4 * k) + 1)) + 1);
set y = 2 |^ (((4 * k) + 1) + 1);
A1: (2 |^ (2 * (4 * k))) mod 5 = 1 by Lm33;
A2: ((2 |^ 4) |^ k) mod 5 = 1 by Lm32;
A3: (2 |^ 4) |^ k = 2 |^ (4 * k) by NEWTON:9;
A4: 2 |^ 3 = (2 * 2) * 2 by POLYEQ_5:2;
A5: 7 mod 5 = 2 by Lm10, NAT_D:24;
A6: 8 mod 5 = 3 by Lm11, NAT_D:24;
2 |^ ((2 * ((4 * k) + 1)) + 1) = 2 |^ ((8 * k) + 3) ;
then 2 |^ ((2 * ((4 * k) + 1)) + 1) = (2 |^ (2 * (4 * k))) * (2 |^ 3) by NEWTON:8;
then A7: (2 |^ ((2 * ((4 * k) + 1)) + 1)) mod 5 = (1 * 3) mod 5 by A1, A4, A6, NAT_D:67
.= 3 by NAT_D:24 ;
A8: 2 |^ 2 = 2 * 2 by POLYEQ_5:1;
A9: 4 mod 5 = 4 by NAT_D:24;
2 |^ (((4 * k) + 1) + 1) = 2 |^ ((4 * k) + 2) ;
then 2 |^ (((4 * k) + 1) + 1) = (2 |^ (4 * k)) * (2 |^ 2) by NEWTON:8;
then A10: (2 |^ (((4 * k) + 1) + 1)) mod 5 = (1 * 4) mod 5 by A2, A3, A8, A9, NAT_D:67
.= 4 by NAT_D:24 ;
thus H₁((4 * k) + 1) mod 5 = ((((2 |^ ((2 * ((4 * k) + 1)) + 1)) - (2 |^ (((4 * k) + 1) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((3 - 4) mod 5) + 1) mod 5 by A7, A10, INT_6:7
.= (((3 - 4) mod 5) + (1 mod 5)) mod 5 by NAT_D:24
.= (((3 - 4) + 1) mod 5) mod 5 by NAT_D:66
.= 0 ; :: thesis:
thus H₂((4 * k) + 1) mod 5 = ((((2 |^ ((2 * ((4 * k) + 1)) + 1)) + (2 |^ (((4 * k) + 1) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((3 + 4) mod 5) + 1) mod 5 by A7, A10, NAT_D:66
.= 3 by A5, NAT_D:24 ; :: thesis:

end;

Lm36: now :: thesis:

let k be Nat; :: thesis:
set x = 2 |^ ((2 * ((4 * k) + 2)) + 1);
set y = 2 |^ (((4 * k) + 2) + 1);
A1: (2 |^ (2 * (4 * k))) mod 5 = 1 by Lm33;
A2: ((2 |^ 4) |^ k) mod 5 = 1 by Lm32;
A3: (2 |^ 4) |^ k = 2 |^ (4 * k) by NEWTON:9;
A4: 2 |^ 5 = (((2 * 2) * 2) * 2) * 2 by NUMBER02:1;
A5: ((6 * 5) + 2) mod 5 = 2 by Lm12, NAT_D:24;
2 |^ ((2 * ((4 * k) + 2)) + 1) = 2 |^ ((8 * k) + 5) ;
then 2 |^ ((2 * ((4 * k) + 2)) + 1) = (2 |^ (2 * (4 * k))) * (2 |^ 5) by NEWTON:8;
then A6: (2 |^ ((2 * ((4 * k) + 2)) + 1)) mod 5 = (1 * 2) mod 5 by A1, A4, A5, NAT_D:67
.= 2 by NAT_D:24 ;
A7: 2 |^ 3 = (2 * 2) * 2 by POLYEQ_5:2;
A8: 8 mod 5 = 3 by Lm11, NAT_D:24;
2 |^ (((4 * k) + 2) + 1) = 2 |^ ((4 * k) + 3) ;
then 2 |^ (((4 * k) + 2) + 1) = (2 |^ (4 * k)) * (2 |^ 3) by NEWTON:8;
then A9: (2 |^ (((4 * k) + 2) + 1)) mod 5 = (1 * 3) mod 5 by A2, A3, A7, A8, NAT_D:67
.= 3 by NAT_D:24 ;
thus H₁((4 * k) + 2) mod 5 = ((((2 |^ ((2 * ((4 * k) + 2)) + 1)) - (2 |^ (((4 * k) + 2) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((2 - 3) mod 5) + 1) mod 5 by A6, A9, INT_6:7
.= (((2 - 3) mod 5) + (1 mod 5)) mod 5 by NAT_D:24
.= (((2 - 3) + 1) mod 5) mod 5 by NAT_D:66
.= 0 ; :: thesis:
thus H₂((4 * k) + 2) mod 5 = ((((2 |^ ((2 * ((4 * k) + 2)) + 1)) + (2 |^ (((4 * k) + 2) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((2 + 3) mod 5) + 1) mod 5 by A6, A9, NAT_D:66
.= (0 + 1) mod 5 by NAT_D:25
.= 1 by NAT_D:24 ; :: thesis:

end;

Lm37: now :: thesis:

let k be Nat; :: thesis:
set x = 2 |^ ((2 * ((4 * k) + 3)) + 1);
set y = 2 |^ (((4 * k) + 3) + 1);
A1: (2 |^ (2 * (4 * k))) mod 5 = 1 by Lm33;
A2: ((2 |^ 4) |^ k) mod 5 = 1 by Lm32;
A3: (2 |^ 4) |^ k = 2 |^ (4 * k) by NEWTON:9;
A4: 2 |^ 7 = (((((2 * 2) * 2) * 2) * 2) * 2) * 2 by NUMBER02:3;
A5: ((5 * 25) + 3) mod 5 = 3 by Lm15, NAT_D:21;
2 |^ ((2 * ((4 * k) + 3)) + 1) = 2 |^ ((8 * k) + 7) ;
then 2 |^ ((2 * ((4 * k) + 3)) + 1) = (2 |^ (2 * (4 * k))) * (2 |^ 7) by NEWTON:8;
then A6: (2 |^ ((2 * ((4 * k) + 3)) + 1)) mod 5 = (1 * 3) mod 5 by A1, A4, A5, NAT_D:67
.= 3 by NAT_D:24 ;
A7: 2 |^ 4 = ((2 * 2) * 2) * 2 by POLYEQ_5:3;
2 |^ (((4 * k) + 3) + 1) = 2 |^ ((4 * k) + 4) ;
then 2 |^ (((4 * k) + 3) + 1) = (2 |^ (4 * k)) * (2 |^ 4) by NEWTON:8;
then A8: (2 |^ (((4 * k) + 3) + 1)) mod 5 = (1 * 1) mod 5 by A2, A3, A7, Lm9, NAT_D:67
.= 1 by NAT_D:24 ;
thus H₁((4 * k) + 3) mod 5 = ((((2 |^ ((2 * ((4 * k) + 3)) + 1)) - (2 |^ (((4 * k) + 3) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((3 - 1) mod 5) + 1) mod 5 by A6, A8, INT_6:7
.= 3 by Lm14, NAT_D:24 ; :: thesis:
thus H₂((4 * k) + 3) mod 5 = ((((2 |^ ((2 * ((4 * k) + 3)) + 1)) + (2 |^ (((4 * k) + 3) + 1))) mod 5) + 1) mod 5 by Lm13, NAT_D:66
.= (((3 + 1) mod 5) + 1) mod 5 by A6, A8, NAT_D:66
.= (4 + 1) mod 5 by NAT_D:24
.= 0 by NAT_D:25 ; :: thesis:

end;

:: Problem 11 a

theorem Th39: :: NUMBER03:39

for n being Nat holds
( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff ( n mod 4 = 1 or n mod 4 = 2 ) )

proof end;

:: Problem 11 b

theorem Th40: :: NUMBER03:40

for n being Nat holds
( 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 iff ( n mod 4 = 0 or n mod 4 = 3 ) )

proof end;

:: Problem 11 c

theorem :: NUMBER03:41

for n being Nat holds
( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff not 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 )

proof end;

:: Problem 16 a

theorem :: NUMBER03:42

{ n where n is Nat : n divides (2 |^ n) + 1 } is infinite

proof end;

:: Problem 16 b

theorem :: NUMBER03:43

{ n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } = {3}

proof end;

:: Problem 19

theorem :: NUMBER03:44

for a being Nat holds
( 10 divides (a |^ 10) + 1 iff ex k being Nat st
( a = (10 * k) + 3 or a = (10 * k) + 7 ) )

proof end;

theorem Th45: :: NUMBER03:45

for a, b, n being Nat st ( a <> 0 or b <> 0 ) & n > 0 & a divides (b |^ n) - 1 holds
a,b are_coprime

proof end;

:: Problem 20

theorem :: NUMBER03:46

for n being Nat holds
( not 1 < n or not n divides (2 |^ n) - 1 )

proof end;

:: Problem 21

theorem :: NUMBER03:47

{ n where n is odd Nat : n divides (3 |^ n) + 1 } = {1}

proof end;

:: Problem 22

theorem :: NUMBER03:48

{ n where n is positive Nat : 3 divides (n * (2 |^ n)) + 1 } = { ((6 * k) + 1) where k is Nat : verum } \/ { ((6 * k) + 2) where k is Nat : verum }

proof end;

theorem Th49: :: NUMBER03:49

for k, n being Nat
for p being odd Prime st n = (p - 1) * ((k * p) + 1) holds
(2 |^ n) mod p = 1

proof end;

theorem Th50: :: NUMBER03:50

for k, n being Nat
for p being odd Prime st n = (p - 1) * ((k * p) + 1) holds
p divides CullenNumber n

proof end;

:: Problem 23

theorem :: NUMBER03:51

for p being odd Prime holds { n where n is Nat : p divides CullenNumber n } is infinite

proof end;

:: Problem 24

theorem :: NUMBER03:52

for n being Nat ex x, y being Nat st
( x > n & not x divides y & x |^ x divides y |^ y )

proof end;

Lm38: for a, n, r being Integer st 0 < n & 0 <= r & r < n & r <> (- a) mod n holds
not n divides a + r

proof end;

:: Problem 39

theorem :: NUMBER03:53

for a, b, c, n being Integer st 3 < n holds
ex k being Integer st
( not n divides k + a & not n divides k + b & not n divides k + c )

proof end;

Lm39: for a, b being Integer st a < b holds
{ n where n is Nat : a + n,b + n are_coprime } is infinite

proof end;

:: Problem 44

theorem :: NUMBER03:54

for a, b being Integer st a <> b holds
{ n where n is Nat : a + n,b + n are_coprime } is infinite

proof end;

definition

let a, b, c be Integer;

pred a,b,c are_mutually_coprime means :: NUMBER03:def 1
( a,b are_coprime & a,c are_coprime & b,c are_coprime );

let d be Integer;

pred a,b,c,d are_mutually_coprime means :: NUMBER03:def 2
( a,b are_coprime & a,c are_coprime & a,d are_coprime & b,c are_coprime & b,d are_coprime & c,d are_coprime );

end;

:: deftheorem defines are_mutually_coprime NUMBER03:def 1 :

:: deftheorem defines are_mutually_coprime NUMBER03:def 2 :

theorem :: NUMBER03:55

for a, b, c being Prime st a,b,c are_mutually_distinct holds
a,b,c are_mutually_coprime by INT_2:30;

theorem :: NUMBER03:56

for a, b, c, d being Prime st a,b,c,d are_mutually_distinct holds
a,b,c,d are_mutually_coprime by INT_2:30;

:: Problem 46

theorem :: NUMBER03:57

( 1,2,3,4 are_mutually_distinct & ( for n being positive Nat holds not 1 + n,2 + n,3 + n,4 + n are_mutually_coprime ) )

proof end;

:: Problem 74

theorem :: NUMBER03:58

for n being even Nat st n > 6 holds
ex p, q being Prime st
( n - p,n - q are_coprime & p = 3 & q = 5 )

proof end;

:: Problem 75

theorem :: NUMBER03:59

{ p where p is Prime : ( ex a, b being Prime st p = a + b & ex c, d being Prime st p = c - d ) } = {5}

proof end;

A corrollary from the Fermat Theorem

theorem Th60: :: NUMBER03:60

for k being Nat
for p being Prime st p = (4 * k) + 1 holds
ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )

proof end;

:: Problem 77

theorem :: NUMBER03:61

for k being Nat
for p being Prime st p = (4 * k) + 1 holds
ex a, b being positive Nat st p ^2 = (a ^2) + (b ^2)

proof end;

theorem Th62: :: NUMBER03:62

for n being Nat holds
( 5 divides n + 1 or 5 divides n + 7 or 5 divides n + 9 or 5 divides n + 13 or 5 divides n + 15 )

proof end;

:: Problem 82

theorem :: NUMBER03:63

{ n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } = {4}

proof end;

:: Problem 176

theorem :: NUMBER03:64

for r being Real holds
( ((r |^ 3) + ((r + 1) |^ 3)) + ((r + 2) |^ 3) = (r + 3) |^ 3 iff r = 3 )

proof end;

theorem Th1: :: NUMBER03:65

for p being Prime st p < 3 holds
p = 2

proof end;

theorem :: NUMBER03:66

for k being Nat
for p being Prime st p * p <= k & k < 9 holds
p = 2

proof end;

theorem Th3: :: NUMBER03:67

for p being Prime holds
( not p < 5 or p = 2 or p = 3 )

proof end;

theorem :: NUMBER03:68

for k being Nat
for p being Prime st p * p <= k & k < 25 & not p = 2 holds
p = 3

proof end;

theorem Th5: :: NUMBER03:69

for p being Prime holds
( not p < 7 or p = 2 or p = 3 or p = 5 )

proof end;

theorem :: NUMBER03:70

for k being Nat
for p being Prime st p * p <= k & k < 49 & not p = 2 & not p = 3 holds
p = 5

proof end;

theorem Th7: :: NUMBER03:71

for p being Prime holds
( not p < 11 or p = 2 or p = 3 or p = 5 or p = 7 )

proof end;

theorem :: NUMBER03:72

for k being Nat
for p being Prime st p * p <= k & k < 121 & not p = 2 & not p = 3 & not p = 5 holds
p = 7

proof end;

theorem Th9: :: NUMBER03:73

for p being Prime holds
( not p < 13 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 )

proof end;

theorem :: NUMBER03:74

for k being Nat
for p being Prime st p * p <= k & k < 169 & not p = 2 & not p = 3 & not p = 5 & not p = 7 holds
p = 11

proof end;

theorem Th11: :: NUMBER03:75

for p being Prime holds
( not p < 17 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 )

proof end;

theorem :: NUMBER03:76

for k being Nat
for p being Prime st p * p <= k & k < 289 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 holds
p = 13

proof end;

theorem Th13: :: NUMBER03:77

for p being Prime holds
( not p < 19 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 )

proof end;

theorem :: NUMBER03:78

for k being Nat
for p being Prime st p * p <= k & k < 361 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 holds
p = 17

proof end;

theorem Th15: :: NUMBER03:79

for p being Prime holds
( not p < 23 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )

proof end;

theorem :: NUMBER03:80

for k being Nat
for p being Prime st p * p <= k & k < 529 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 holds
p = 19

proof end;

theorem Th17: :: NUMBER03:81

for p being Prime holds
( not p < 29 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 )

proof end;

theorem :: NUMBER03:82

for k being Nat
for p being Prime st p * p <= k & k < 841 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 holds
p = 23

proof end;

theorem Th19: :: NUMBER03:83

for p being Prime holds
( not p < 31 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 )

proof end;

theorem :: NUMBER03:84

for k being Nat
for p being Prime st p * p <= k & k < 961 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 holds
p = 29

proof end;

theorem Th21: :: NUMBER03:85

for p being Prime holds
( not p < 37 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 )

proof end;

theorem :: NUMBER03:86

for k being Nat
for p being Prime st p * p <= k & k < 1369 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 holds
p = 31

proof end;

theorem Th23: :: NUMBER03:87

for p being Prime holds
( not p < 41 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 )

proof end;

theorem :: NUMBER03:88

for k being Nat
for p being Prime st p * p <= k & k < 1681 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 holds
p = 37

proof end;

theorem Th25: :: NUMBER03:89

for p being Prime holds
( not p < 43 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 )

proof end;

theorem :: NUMBER03:90

for k being Nat
for p being Prime st p * p <= k & k < 1849 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 holds
p = 41

proof end;

theorem Th27: :: NUMBER03:91

for p being Prime holds
( not p < 47 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 )

proof end;

theorem :: NUMBER03:92

for k being Nat
for p being Prime st p * p <= k & k < 2209 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 holds
p = 43

proof end;

theorem Th29: :: NUMBER03:93

for p being Prime holds
( not p < 53 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 )

proof end;

theorem :: NUMBER03:94

for k being Nat
for p being Prime st p * p <= k & k < 2809 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 holds
p = 47

proof end;

theorem Th31: :: NUMBER03:95

for p being Prime holds
( not p < 59 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 )

proof end;

theorem :: NUMBER03:96

for k being Nat
for p being Prime st p * p <= k & k < 3481 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 holds
p = 53

proof end;

theorem Th33: :: NUMBER03:97

for p being Prime holds
( not p < 61 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 )

proof end;

theorem :: NUMBER03:98

for k being Nat
for p being Prime st p * p <= k & k < 3721 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 holds
p = 59

proof end;

theorem Th35: :: NUMBER03:99

for p being Prime holds
( not p < 67 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 )

proof end;

theorem :: NUMBER03:100

for k being Nat
for p being Prime st p * p <= k & k < 4489 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 holds
p = 61

proof end;

theorem Th37: :: NUMBER03:101

for p being Prime holds
( not p < 71 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 )

proof end;

theorem :: NUMBER03:102

for k being Nat
for p being Prime st p * p <= k & k < 5041 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 holds
p = 67

proof end;

theorem Th39: :: NUMBER03:103

for p being Prime holds
( not p < 73 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 )

proof end;

theorem :: NUMBER03:104

for k being Nat
for p being Prime st p * p <= k & k < 5329 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 holds
p = 71

proof end;

theorem Th41: :: NUMBER03:105

for p being Prime holds
( not p < 79 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 )

proof end;

theorem :: NUMBER03:106

for k being Nat
for p being Prime st p * p <= k & k < 6241 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 & not p = 71 holds
p = 73

proof end;

theorem Th43: :: NUMBER03:107

for p being Prime holds
( not p < 83 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 )

proof end;

theorem :: NUMBER03:108

for k being Nat
for p being Prime st p * p <= k & k < 6889 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 & not p = 71 & not p = 73 holds
p = 79

proof end;

theorem Th45: :: NUMBER03:109

for p being Prime holds
( not p < 89 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83 )

proof end;

theorem :: NUMBER03:110

for k being Nat
for p being Prime st p * p <= k & k < 7921 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 & not p = 71 & not p = 73 & not p = 79 holds
p = 83

proof end;

theorem Th47: :: NUMBER03:111

for p being Prime holds
( not p < 97 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83 or p = 89 )

proof end;

theorem :: NUMBER03:112

for k being Nat
for p being Prime st p * p <= k & k < 9409 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 & not p = 71 & not p = 73 & not p = 79 & not p = 83 holds
p = 89

proof end;

theorem Th49: :: NUMBER03:113

for p being Prime holds
( not p < 101 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83 or p = 89 or p = 97 )

proof end;

theorem :: NUMBER03:114

for k being Nat
for p being Prime st p * p <= k & k < 10201 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 & not p = 71 & not p = 73 & not p = 79 & not p = 83 & not p = 89 holds
p = 97

proof end;