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

coherence

Del (f,i) is D -valued

end;
let f be D -valued FinSequence;

let i be Nat;

coherence

Del (f,i) is D -valued

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

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

n = 29

proof end;

registration
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)

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 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 )

( 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 )

( 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 )

( 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 )

( 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 )

( 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 )

( 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 )

( 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 ) )

( 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 ) )

( 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 ) )

( 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 ) )

( 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 ) )

( 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 ) )

( 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 ) )

( 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 ) )

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

definition
end;

:: deftheorem Def1 defines composite NUMBER02:def 1 :

for n being Integer holds

( n is composite iff ( 2 <= n & not n is prime ) );

for n being Integer holds

( n is composite iff ( 2 <= n & not n is prime ) );

registration

existence

ex b_{1} being Integer st b_{1} is composite

ex b_{1} being Nat st b_{1} is composite

for b_{1} being Integer st b_{1} is composite holds

b_{1} is positive
;

coherence

for b_{1} being Integer st b_{1} is prime holds

not b_{1} is composite
;

coherence

for b_{1} being Integer st b_{1} is composite holds

not b_{1} is prime
;

end;
ex b

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

proof end;

coherence for b

b

coherence

for b

not b

coherence

for b

not b

registration
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

a |^ m divides ((a,b) In_Power n) . i

proof end;

::Problem 14

:: Problem 15

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

( not n < 6 or n divides (2 |^ n) - 2 or not n divides (3 |^ n) - 3 ) ) )

proof end;

:: Problem 30

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 )

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 )

( 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 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 )

( (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

( 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

not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6

proof end;

:: Problem 34

:: Problem 78

theorem :: NUMBER02:53

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

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

( not n < 5 or not (n |^ 4) + ((n + 1) |^ 4) is composite ) ) )

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

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

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;