:: Elementary Number Theory Problems. {P}art {II}
:: by Artur Korni{\l}owicz and Dariusz Surowik
::
:: 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 ;

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
existence
ex b1 being Integer st b1 is composite
proof end;
existence
ex b1 being Nat st b1 is composite
proof end;
coherence
for b1 being Integer st b1 is composite holds
b1 is positive
;
cluster integer prime -> non composite for object ;
coherence
for b1 being Integer st b1 is prime holds
not b1 is composite
;
cluster integer composite -> non prime for object ;
coherence
for b1 being Integer st b1 is composite holds
not b1 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 ;

theorem Th57: :: NUMBER02:57
not (2 |^ 4) + ((2 + 1) |^ 4) is composite by ;

theorem Th58: :: NUMBER02:58
not (3 |^ 4) + ((3 + 1) |^ 4) is composite by ;

theorem Th59: :: NUMBER02:59
not (4 |^ 4) + ((4 + 1) |^ 4) is composite by ;

:: 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;