:: Elementary Number Theory Problems. {P}art {II}
:: by Artur Korni{\l}owicz and Dariusz Surowik
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

registration

let D be non empty set ;
let f be D -valued FinSequence;
let i be Nat;

cluster Del (f,i) -> D -valued ;

coherence
Del (f,i) is D -valued

proof end;

end;

theorem Th1: :: NUMBER02:1

for c being Complex holds c |^ 5 = (((c * c) * c) * c) * c

proof end;

theorem Th2: :: NUMBER02:2

for c being Complex holds c |^ 6 = ((((c * c) * c) * c) * c) * c

proof end;

theorem Th3: :: NUMBER02:3

for c being Complex holds c |^ 7 = (((((c * c) * c) * c) * c) * c) * c

proof end;

theorem Th4: :: NUMBER02:4

for c being Complex holds c |^ 8 = ((((((c * c) * c) * c) * c) * c) * c) * c

proof end;

theorem Th5: :: NUMBER02:5

for c being Complex holds c |^ 9 = (((((((c * c) * c) * c) * c) * c) * c) * c) * c

proof end;

theorem Th6: :: NUMBER02:6

for c being Complex holds c |^ 10 = ((((((((c * c) * c) * c) * c) * c) * c) * c) * c) * c

proof end;

theorem Th7: :: NUMBER02:7

for a, k, n being Nat st a = n - 1 & k < n holds
not not k = 0 & ... & not k = a

proof end;

theorem Th8: :: NUMBER02:8

(- 1) div 3 = - 1

proof end;

theorem Th9: :: NUMBER02:9

(- 1) mod 3 = 2

proof end;

theorem Th10: :: NUMBER02:10

not 30 is prime

proof end;

Lm1: ( not 12 is prime & not 14 is prime & not 15 is prime & not 16 is prime )
by NAT_4:57;

Lm2: ( not 18 is prime & not 20 is prime & not 21 is prime )
by NAT_4:57, NAT_4:58;

theorem Th11: :: NUMBER02:11

for n being Nat st n < 31 & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 & not n = 23 holds
n = 29

proof end;

theorem Th12: :: NUMBER02:12

for k, n being Nat st k < 961 & n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 & not n = 23 holds
n = 29

proof end;

theorem Th13: :: NUMBER02:13

113 is prime

proof end;

theorem Th14: :: NUMBER02:14

337 is prime

proof end;

theorem Th15: :: NUMBER02:15

881 is prime

proof end;

theorem Th16: :: NUMBER02:16

for a, b, k being Nat st k < a holds
((a * b) + k) mod a = k

proof end;

theorem :: NUMBER02:17

for a being Nat
for s, z being non zero Nat holds a divides (a |^ s) + (a |^ z)

proof end;

theorem Th18: :: NUMBER02:18

for a being Nat
for s, z being non zero Nat holds a divides (a |^ s) - (a |^ z)

proof end;

theorem :: NUMBER02:19

for a being Nat
for s, z being non zero Nat holds a divides (a |^ s) * (a |^ z)

proof end;

registration

let p, q be prime Nat;

cluster p * q -> non prime ;

coherence
not p * q is prime

proof end;

end;

theorem Th20: :: NUMBER02:20

11 divides (2 |^ 341) - 2

proof end;

theorem Th21: :: NUMBER02:21

31 divides (2 |^ 341) - 2

proof end;

theorem Th22: :: NUMBER02:22

for n being Nat
for z being non zero Nat holds
not for k being Nat holds not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)

proof end;

theorem Th23: :: NUMBER02:23

for n being Nat ex k being Nat st
( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 )

proof end;

theorem Th24: :: NUMBER02:24

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

proof end;

theorem Th25: :: NUMBER02:25

for n being Nat ex k being Nat st
( n = 5 * k or n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 )

proof end;

theorem Th26: :: NUMBER02:26

for n being Nat ex k being Nat st
( n = 6 * k or n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 )

proof end;

theorem Th27: :: NUMBER02:27

for n being Nat ex k being Nat st
( n = 7 * k or n = (7 * k) + 1 or n = (7 * k) + 2 or n = (7 * k) + 3 or n = (7 * k) + 4 or n = (7 * k) + 5 or n = (7 * k) + 6 )

proof end;

theorem Th28: :: NUMBER02:28

for n being Nat ex k being Nat st
( n = 8 * k or n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 )

proof end;

theorem Th29: :: NUMBER02:29

for n being Nat ex k being Nat st
( n = 9 * k or n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 )

proof end;

theorem Th30: :: NUMBER02:30

for n being Nat ex k being Nat st
( n = 10 * k or n = (10 * k) + 1 or n = (10 * k) + 2 or n = (10 * k) + 3 or n = (10 * k) + 4 or n = (10 * k) + 5 or n = (10 * k) + 6 or n = (10 * k) + 7 or n = (10 * k) + 8 or n = (10 * k) + 9 )

proof end;

theorem :: NUMBER02:31

for n being Nat holds
( not 3 divides n iff ex k being Nat st
( n = (3 * k) + 1 or n = (3 * k) + 2 ) )

proof end;

theorem Th32: :: NUMBER02:32

for n being Nat holds
( not 4 divides n iff ex k being Nat st
( n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) )

proof end;

theorem :: NUMBER02:33

for n being Nat holds
( not 5 divides n iff ex k being Nat st
( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) )

proof end;

theorem Th34: :: NUMBER02:34

for n being Nat holds
( not 6 divides n iff ex k being Nat st
( n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) )

proof end;

theorem Th35: :: NUMBER02:35

for n being Nat holds
( not 7 divides n iff ex k being Nat st
( n = (7 * k) + 1 or n = (7 * k) + 2 or n = (7 * k) + 3 or n = (7 * k) + 4 or n = (7 * k) + 5 or n = (7 * k) + 6 ) )

proof end;

theorem :: NUMBER02:36

for n being Nat holds
( not 8 divides n iff ex k being Nat st
( n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 ) )

proof end;

theorem :: NUMBER02:37

for n being Nat holds
( not 9 divides n iff ex k being Nat st
( n = (9 * k) + 1 or n = (9 * k) + 2 or n = (9 * k) + 3 or n = (9 * k) + 4 or n = (9 * k) + 5 or n = (9 * k) + 6 or n = (9 * k) + 7 or n = (9 * k) + 8 ) )

proof end;

theorem :: NUMBER02:38

for n being Nat holds
( not 10 divides n iff ex k being Nat st
( n = (10 * k) + 1 or n = (10 * k) + 2 or n = (10 * k) + 3 or n = (10 * k) + 4 or n = (10 * k) + 5 or n = (10 * k) + 6 or n = (10 * k) + 7 or n = (10 * k) + 8 or n = (10 * k) + 9 ) )

proof end;

theorem Th39: :: NUMBER02:39

for z being non zero Nat holds (2 |^ (2 |^ z)) mod 3 = 1

proof end;

definition

let n be Integer;

attr n is composite means :Def1: :: NUMBER02:def 1
( 2 <= n & not n is prime );

end;

:: deftheorem Def1 defines composite NUMBER02:def 1 :
for n being Integer holds
( n is composite iff ( 2 <= n & not n is prime ) );

registration

cluster complex V26() ext-real integer V57() composite for object ;

existence
ex b₁ being Integer st b₁ is composite

proof end;

cluster V15() V16() V17() V21() complex V26() ext-real non negative integer dim-like finite cardinal V57() composite for set ;

existence
ex b₁ being Nat st b₁ is composite

proof end;

cluster integer composite -> positive for object ;

coherence
for b₁ being Integer st b₁ is composite holds
b₁ is positive ;

cluster integer prime -> non composite for object ;

coherence
for b₁ being Integer st b₁ is prime holds
not b₁ is composite ;

cluster integer composite -> non prime for object ;

coherence
for b₁ being Integer st b₁ is composite holds
not b₁ is prime ;

end;

registration

let m, n be composite Nat;

cluster m * n -> composite ;

coherence
m * n is composite

proof end;

end;

theorem :: NUMBER02:40

for n being Nat st n is composite holds
4 <= n

proof end;

theorem Th41: :: NUMBER02:41

for a, b, i, m, n being Nat st 1 <= i & i <= (len ((a,b) In_Power n)) - m holds
a |^ m divides ((a,b) In_Power n) . i

proof end;

::Problem 14

theorem Th42: :: NUMBER02:42

for n being Nat holds n ^2 divides ((n + 1) |^ n) - 1

proof end;

:: Problem 15

theorem :: NUMBER02:43

for n being Nat holds ((2 |^ n) - 1) ^2 divides (2 |^ (((2 |^ n) - 1) * n)) - 1

proof end;

:: Problem 29

theorem :: NUMBER02:44

( not 6 divides (2 |^ 6) - 2 & 6 divides (3 |^ 6) - 3 & ( for n being Nat holds
( not n < 6 or n divides (2 |^ n) - 2 or not n divides (3 |^ n) - 3 ) ) )

proof end;

:: Problem 30

theorem :: NUMBER02:45

for a being non zero Nat ex n being non prime Nat st n divides (a |^ n) - a

proof end;

theorem Th46: :: NUMBER02:46

for a being Nat st not 7 divides a holds
ex k being Nat st
( a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )

proof end;

theorem :: NUMBER02:47

for a being Nat ex k being Nat st
( a ^2 = 7 * k or a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )

proof end;

theorem Th48: :: NUMBER02:48

for a being Nat holds
( 7 divides a or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )

proof end;

theorem Th49: :: NUMBER02:49

for a being Nat holds
( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )

proof end;

theorem :: NUMBER02:50

for a, b being Nat st ex k being Nat st
( a = (7 * k) + 1 or a = (7 * k) + 2 or a = (7 * k) + 4 ) & ex k being Nat st
( b = (7 * k) + 1 or b = (7 * k) + 2 or b = (7 * k) + 4 ) holds
ex k being Nat st

proof end;

theorem :: NUMBER02:51

for a, b being Nat st ( a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4 ) & ( b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4 ) holds
not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6

proof end;

:: Problem 34

theorem :: NUMBER02:52

for a, b being Nat st 7 divides (a ^2) + (b ^2) holds
( 7 divides a & 7 divides b )

proof end;

:: Problem 78

theorem :: NUMBER02:53

( (13 ^2) + 1 = (7 ^2) + (11 ^2) & (17 ^2) + 1 = (11 ^2) + (13 ^2) & (23 ^2) + 1 = (13 ^2) + (19 ^2) & (31 ^2) + 1 = (11 ^2) + (29 ^2) ) ;

:: Problem 83

theorem :: NUMBER02:54

( 2 = (1 |^ 4) + (1 |^ 4) & 17 = (1 |^ 4) + (2 |^ 4) & 97 = (2 |^ 4) + (3 |^ 4) & 257 = (1 |^ 4) + (4 |^ 4) & 641 = (2 |^ 4) + (5 |^ 4) )

proof end;

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

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

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

Lm6: 5 |^ 4 = ((5 * 5) * 5) * 5
by POLYEQ_5:3;

Lm7: 6 |^ 4 = ((6 * 6) * 6) * 6
by POLYEQ_5:3;

theorem :: NUMBER02:55

not (0 |^ 4) + ((0 + 1) |^ 4) is composite ;

theorem Th56: :: NUMBER02:56

not (1 |^ 4) + ((1 + 1) |^ 4) is composite by Lm3, PEPIN:60;

theorem Th57: :: NUMBER02:57

not (2 |^ 4) + ((2 + 1) |^ 4) is composite by Lm3, Lm4, NUMERAL2:35;

theorem Th58: :: NUMBER02:58

not (3 |^ 4) + ((3 + 1) |^ 4) is composite by Lm4, Lm5, Th14;

theorem Th59: :: NUMBER02:59

not (4 |^ 4) + ((4 + 1) |^ 4) is composite by Lm5, Lm6, Th15;

:: Problem 97

theorem :: NUMBER02:60

( (5 |^ 4) + ((5 + 1) |^ 4) is composite & ( for n being Nat holds
( not n < 5 or not (n |^ 4) + ((n + 1) |^ 4) is composite ) ) )

proof end;

theorem Th61: :: NUMBER02:61

for a, n being Nat st 1 <= a holds
(2 |^ (2 |^ n)) + ((6 * a) - 1) > 6

proof end;

theorem Th62: :: NUMBER02:62

for a being Nat
for z being non zero Nat holds 3 divides (2 |^ (2 |^ z)) + ((6 * a) - 1)

proof end;

theorem Th63: :: NUMBER02:63

for a being Nat
for z being non zero Nat st 1 <= a holds
not (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime

proof end;

theorem Th64: :: NUMBER02:64

for a being Nat
for z being non zero Nat st 1 <= a holds
(2 |^ (2 |^ z)) + ((6 * a) - 1) is composite

proof end;

:: Problem 116

theorem :: NUMBER02:65

for z being non zero Nat holds { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } is infinite

proof end;