NUMBER07: Elementary Number Theory Problems. Part {VII}

:: Elementary Number Theory Problems. Part {VII}
:: by Artur Korni{\l}owicz
::
:: Received March 31, 2023
:: Copyright (c) 2023-2024 Association of Mizar Users

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

Lm2: 5 |^ 2 = 5 * 5
by NEWTON:81;

theorem Th1: :: NUMBER07:1

for m, n being Nat holds m gcd (m * n) = m

proof end;

theorem :: NUMBER07:2

for m, n being Nat st m <> 1 holds
not m,m * n are_coprime by Th1;

theorem Th3: :: NUMBER07:3

for i, j being Integer st i <> - 1 & i <> 1 & i divides j holds
not i divides j + 1

proof end;

theorem Th4: :: NUMBER07:4

for i, j being Integer st i <> - 1 & i <> 1 & i divides j holds
not i divides j - 1

proof end;

theorem Th5: :: NUMBER07:5

for i, j being Integer st i divides j holds
i,j + 1 are_coprime

proof end;

theorem Th6: :: NUMBER07:6

for i, j being Integer st i divides j holds
i,j - 1 are_coprime

proof end;

theorem Th7: :: NUMBER07:7

for a, b, c being Nat st (a + b) + c is odd & a,b,c are_mutually_coprime holds
( a is odd & b is odd & c is odd )

proof end;

theorem :: NUMBER07:8

for n being Nat holds
( (4 * n) mod 8 = 0 or (4 * n) mod 8 = 4 )

proof end;

Lem1: for k, m, n being Nat st n divides k * m holds
ex a, b being Nat st
( a divides k & b divides m & n = a * b )

proof end;

Lem2: for n being Nat
for p1, p2 being Prime holds
( not n divides p1 * p2 or n = 1 or n = p1 or n = p2 or n = p1 * p2 )

proof end;

theorem Th9: :: NUMBER07:9

for n being Nat holds
( not n divides 2 or n = 1 or n = 2 ) by XPRIMES1:2;

theorem Th10: :: NUMBER07:10

for n being Nat holds
( not n divides 6 or n = 1 or n = 2 or n = 3 or n = 6 )

proof end;

theorem Th11: :: NUMBER07:11

for n being Nat holds
( not n divides 9 or n = 1 or n = 3 or n = 9 )

proof end;

theorem Th12: :: NUMBER07:12

for n being Nat holds
( not n divides 10 or n = 1 or n = 2 or n = 5 or n = 10 )

proof end;

theorem Th13: :: NUMBER07:13

for n being Nat holds
( not n divides 25 or n = 1 or n = 5 or n = 25 )

proof end;

theorem Th14: :: NUMBER07:14

for n being Nat holds
( not n divides 26 or n = 1 or n = 2 or n = 13 or n = 26 )

proof end;

theorem Th15: :: NUMBER07:15

for n being Nat holds
( not n divides 36 or n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 9 or n = 12 or n = 18 or n = 36 )

proof end;

theorem Th16: :: NUMBER07:16

for n being Nat holds
( not n divides 50 or n = 1 or n = 2 or n = 5 or n = 10 or n = 25 or n = 50 )

proof end;

theorem Th17: :: NUMBER07:17

for n being Nat holds
( not n divides 65 or n = 1 or n = 5 or n = 13 or n = 65 )

proof end;

theorem Th18: :: NUMBER07:18

for n being Nat holds
( not n divides 82 or n = 1 or n = 2 or n = 41 or n = 82 )

proof end;

theorem Th19: :: NUMBER07:19

for n being Nat holds
( not n divides 122 or n = 1 or n = 2 or n = 61 or n = 122 )

proof end;

theorem Th20: :: NUMBER07:20

for n being Nat holds
( not n divides 145 or n = 1 or n = 5 or n = 29 or n = 145 )

proof end;

theorem Th21: :: NUMBER07:21

for n being Nat holds
( not n divides 226 or n = 1 or n = 2 or n = 113 or n = 226 )

proof end;

theorem Th22: :: NUMBER07:22

for n being Nat holds
( not n divides 325 or n = 1 or n = 5 or n = 13 or n = 25 or n = 65 or n = 325 )

proof end;

theorem Th23: :: NUMBER07:23

for n being Nat holds
( not n divides 362 or n = 1 or n = 2 or n = 181 or n = 362 )

proof end;

theorem Th24: :: NUMBER07:24

for n being Nat holds
( not n divides 485 or n = 1 or n = 5 or n = 97 or n = 485 )

proof end;

theorem Th25: :: NUMBER07:25

for n being Nat holds
( not n divides 626 or n = 1 or n = 2 or n = 313 or n = 626 )

proof end;

theorem Th26: :: NUMBER07:26

for m, n being Nat
for p being Prime holds
( not m * n = p or ( m = 1 & n = p ) or ( m = p & n = 1 ) )

proof end;

theorem Th27: :: NUMBER07:27

for m, n being Nat holds
( not m * n = 10 or ( m = 1 & n = 10 ) or ( m = 2 & n = 5 ) or ( m = 5 & n = 2 ) or ( m = 10 & n = 1 ) )

proof end;

theorem Th28: :: NUMBER07:28

for m, n being Nat holds
( not m * n = 25 or ( m = 1 & n = 25 ) or ( m = 5 & n = 5 ) or ( m = 25 & n = 1 ) )

proof end;

theorem Th29: :: NUMBER07:29

for m, n being Nat holds
( not m * n = 26 or ( m = 1 & n = 26 ) or ( m = 2 & n = 13 ) or ( m = 13 & n = 2 ) or ( m = 26 & n = 1 ) )

proof end;

theorem Th30: :: NUMBER07:30

for m, n being Nat holds
( not m * n = 50 or ( m = 1 & n = 50 ) or ( m = 2 & n = 25 ) or ( m = 5 & n = 10 ) or ( m = 10 & n = 5 ) or ( m = 25 & n = 2 ) or ( m = 50 & n = 1 ) )

proof end;

theorem Th31: :: NUMBER07:31

for m, n being Nat holds
( not m * n = 65 or ( m = 1 & n = 65 ) or ( m = 5 & n = 13 ) or ( m = 13 & n = 5 ) or ( m = 65 & n = 1 ) )

proof end;

theorem Th32: :: NUMBER07:32

for m, n being Nat holds
( not m * n = 82 or ( m = 1 & n = 82 ) or ( m = 2 & n = 41 ) or ( m = 41 & n = 2 ) or ( m = 82 & n = 1 ) )

proof end;

theorem Th33: :: NUMBER07:33

for m, n being Nat holds
( not m * n = 122 or ( m = 1 & n = 122 ) or ( m = 2 & n = 61 ) or ( m = 61 & n = 2 ) or ( m = 122 & n = 1 ) )

proof end;

theorem Th34: :: NUMBER07:34

for m, n being Nat holds
( not m * n = 145 or ( m = 1 & n = 145 ) or ( m = 5 & n = 29 ) or ( m = 29 & n = 5 ) or ( m = 145 & n = 1 ) )

proof end;

theorem Th35: :: NUMBER07:35

for m, n being Nat holds
( not m * n = 226 or ( m = 1 & n = 226 ) or ( m = 2 & n = 113 ) or ( m = 113 & n = 2 ) or ( m = 226 & n = 1 ) )

proof end;

theorem Th36: :: NUMBER07:36

for m, n being Nat holds
( not m * n = 325 or ( m = 1 & n = 325 ) or ( m = 5 & n = 65 ) or ( m = 13 & n = 25 ) or ( m = 25 & n = 13 ) or ( m = 65 & n = 5 ) or ( m = 325 & n = 1 ) )

proof end;

theorem Th37: :: NUMBER07:37

for m, n being Nat holds
( not m * n = 362 or ( m = 1 & n = 362 ) or ( m = 2 & n = 181 ) or ( m = 181 & n = 2 ) or ( m = 362 & n = 1 ) )

proof end;

theorem Th38: :: NUMBER07:38

for m, n being Nat holds
( not m * n = 485 or ( m = 1 & n = 485 ) or ( m = 5 & n = 97 ) or ( m = 97 & n = 5 ) or ( m = 485 & n = 1 ) )

proof end;

theorem Th39: :: NUMBER07:39

for m, n being Nat holds
( not m * n = 626 or ( m = 1 & n = 626 ) or ( m = 2 & n = 313 ) or ( m = 313 & n = 2 ) or ( m = 626 & n = 1 ) )

proof end;

theorem Th40: :: NUMBER07:40

for p1, p2 being Prime holds
( not p1 <> p2 or ( 2 <= p1 & 3 <= p2 ) or ( 3 <= p1 & 2 <= p2 ) )

proof end;

definition

let n be Nat;

pred n satisfies_Sierpinski_problem_48 means :: NUMBER07:def 1
ex a, b, c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime );

end;

:: deftheorem defines satisfies_Sierpinski_problem_48 NUMBER07:def 1 :

theorem Th41: :: NUMBER07:41

for n being Nat st n is even & n > 8 holds
n satisfies_Sierpinski_problem_48

proof end;

:: Problem 48a

theorem :: NUMBER07:42

for n being Nat st n > 17 holds
n satisfies_Sierpinski_problem_48

proof end;

Lm3: now :: thesis:

let a, b, c be Nat; :: thesis:
assume that
A1: 1 < b and
A2: 1 < c and
A3: (a + b) + c = 17 ; :: thesis:
assume a >= 15 ; :: thesis:
then a + b > 15 + 1 by A1, XREAL_1:8;
then (a + b) + c > 16 + 1 by A2, XREAL_1:8;
hence contradiction by A3; :: thesis:

end;

Lm4: now :: thesis:

let n be odd Nat; :: thesis:
assume ( 1 < n & n < 15 ) ; :: thesis:
then ( 1 < n & n < 14 + 1 ) ;
then ( 1 + 1 <= n & n <= 14 ) by NAT_1:13;
then not not n = 2 + 0 & ... & not n = 2 + 12 by NAT_1:62;
then ( n = 2 * 1 or n = 3 or n = 2 * 2 or n = 5 or n = 2 * 3 or n = 7 or n = 2 * 4 or n = 9 or n = 2 * 5 or n = 11 or n = 2 * 6 or n = 13 or n = 2 * 7 ) ;
hence ( n = 3 or n = 5 or n = 7 or n = 9 or n = 11 or n = 13 ) ; :: thesis:

end;

:: Problem 48b

theorem :: NUMBER07:43

not 17 satisfies_Sierpinski_problem_48

proof end;

theorem Th44: :: NUMBER07:44

for p, q being Prime
for n being Nat holds
( not (p * (p + 1)) + (q * (q + 1)) = n * (n + 1) or ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

proof end;

:: Problem 80

theorem :: NUMBER07:45

for p, q, r being Prime st (p * (p + 1)) + (q * (q + 1)) = r * (r + 1) holds
( p = q & q = 2 & r = 3 )

proof end;

definition

let n be Nat;

pred n satisfies_Sierpinski_problem_87a means :: NUMBER07:def 2
ex a, b, c being Prime st
( a,b,c are_mutually_distinct & (n |^ 2) + 1 = (a * b) * c );

pred n satisfies_Sierpinski_problem_87b means :: NUMBER07:def 3
ex a, b, c being odd Prime st
( a,b,c are_mutually_distinct & (n |^ 2) + 1 = (a * b) * c );

end;

:: deftheorem defines satisfies_Sierpinski_problem_87a NUMBER07:def 2 :

:: deftheorem defines satisfies_Sierpinski_problem_87b NUMBER07:def 3 :

theorem Th46: :: NUMBER07:46

(13 |^ 2) + 1 = (2 * 5) * 17

proof end;

theorem :: NUMBER07:47

13 satisfies_Sierpinski_problem_87a

proof end;

theorem Th48: :: NUMBER07:48

(17 |^ 2) + 1 = (2 * 5) * 29

proof end;

theorem :: NUMBER07:49

17 satisfies_Sierpinski_problem_87a

proof end;

theorem Th50: :: NUMBER07:50

(21 |^ 2) + 1 = (2 * 13) * 17

proof end;

theorem :: NUMBER07:51

21 satisfies_Sierpinski_problem_87a

proof end;

theorem Th52: :: NUMBER07:52

(23 |^ 2) + 1 = (2 * 5) * 53

proof end;

theorem :: NUMBER07:53

23 satisfies_Sierpinski_problem_87a

proof end;

theorem Th54: :: NUMBER07:54

(27 |^ 2) + 1 = (2 * 5) * 73

proof end;

theorem :: NUMBER07:55

27 satisfies_Sierpinski_problem_87a

proof end;

Lm5: not 0 satisfies_Sierpinski_problem_87a

proof end;

Lm6: not 1 satisfies_Sierpinski_problem_87a

proof end;

Lm7: not 2 satisfies_Sierpinski_problem_87a

proof end;

Lm8: not 3 satisfies_Sierpinski_problem_87a

proof end;

Lm9: not 4 satisfies_Sierpinski_problem_87a

proof end;

Lm10: not 5 satisfies_Sierpinski_problem_87a

proof end;

Lm11: not 6 satisfies_Sierpinski_problem_87a

proof end;

Lm12: not 7 satisfies_Sierpinski_problem_87a

proof end;

Lm13: not 8 satisfies_Sierpinski_problem_87a

proof end;

Lm14: not 9 satisfies_Sierpinski_problem_87a

proof end;

Lm15: not 10 satisfies_Sierpinski_problem_87a

proof end;

Lm16: not 11 satisfies_Sierpinski_problem_87a

proof end;

Lm17: not 12 satisfies_Sierpinski_problem_87a

proof end;

Lm18: not 14 satisfies_Sierpinski_problem_87a

proof end;

Lm19: not 15 satisfies_Sierpinski_problem_87a

proof end;

Lm20: not 16 satisfies_Sierpinski_problem_87a

proof end;

Lm21: not 18 satisfies_Sierpinski_problem_87a

proof end;

Lm22: not 19 satisfies_Sierpinski_problem_87a

proof end;

Lm23: not 20 satisfies_Sierpinski_problem_87a

proof end;

Lm24: not 22 satisfies_Sierpinski_problem_87a

proof end;

Lm25: not 24 satisfies_Sierpinski_problem_87a

proof end;

Lm26: not 25 satisfies_Sierpinski_problem_87a

proof end;

Lm27: not 26 satisfies_Sierpinski_problem_87a

proof end;

:: Problem 87 a

theorem :: NUMBER07:56

for n being Nat st n satisfies_Sierpinski_problem_87a & n <= 27 holds
n in {13,17,21,23,27}

proof end;

theorem Th57: :: NUMBER07:57

(112 |^ 2) + 1 = (5 * 13) * 193

proof end;

:: Problem 87 b

theorem :: NUMBER07:58

112 satisfies_Sierpinski_problem_87b

proof end;

definition

let n be Nat;

pred n has_exactly_two_different_prime_divisors means :: NUMBER07:def 4
ex p, q being Prime st
( p <> q & p divides n & q divides n & ( for r being Prime st r <> p & r <> q holds
not r divides n ) );

end;

:: deftheorem defines has_exactly_two_different_prime_divisors NUMBER07:def 4 :

definition

let n be Complex;

pred n is_a_product_of_two_different_primes means :: NUMBER07:def 5
ex p, q being Prime st
( p <> q & n = p * q );

end;

:: deftheorem defines is_a_product_of_two_different_primes NUMBER07:def 5 :

theorem Th59: :: NUMBER07:59

for p, q being Prime
for a, b being Nat st a <> 1 & b <> 1 & p * q = a * b & not ( p = a & q = b ) holds
( p = b & q = a )

proof end;

theorem :: NUMBER07:60

for n being Nat st n is_a_product_of_two_different_primes holds
for a, b being Nat st a <> 1 & b <> 1 & n = a * b holds
( a is prime & b is prime ) by Th59;

theorem Th61: :: NUMBER07:61

for p being Prime holds not p is_a_product_of_two_different_primes ;

theorem :: NUMBER07:62

for p1, p2 being Prime st p1 <> p2 holds
p1 * p2 is_a_product_of_two_different_primes

proof end;

theorem Th63: :: NUMBER07:63

for a, n being Nat st a <> 1 & a <> n & not a is prime & a divides n holds
not n is_a_product_of_two_different_primes by GR_CY_3:1;

theorem Th64: :: NUMBER07:64

for p being Prime holds not p * p is_a_product_of_two_different_primes

proof end;

theorem Th65: :: NUMBER07:65

for n being Nat st n is_a_product_of_two_different_primes holds
n >= 6

proof end;

definition

let n be Nat;

pred n satisfies_Sierpinski_problem_89 means :: NUMBER07:def 6
( n is_a_product_of_two_different_primes & n + 1 is_a_product_of_two_different_primes & n + 2 is_a_product_of_two_different_primes );

end;

:: deftheorem defines satisfies_Sierpinski_problem_89 NUMBER07:def 6 :

reconsider P2 = 2 as Prime by XPRIMES1:2;

reconsider P3 = 3 as Prime by XPRIMES1:3;

reconsider P5 = 5 as Prime by XPRIMES1:5;

reconsider P7 = 7 as Prime by XPRIMES1:7;

reconsider P11 = 11 as Prime by XPRIMES1:11;

reconsider P13 = 13 as Prime by XPRIMES1:13;

reconsider P17 = 17 as Prime by XPRIMES1:17;

reconsider P19 = 19 as Prime by XPRIMES1:19;

reconsider P23 = 23 as Prime by XPRIMES1:23;

reconsider P29 = 29 as Prime by XPRIMES1:29;

reconsider P31 = 31 as Prime by XPRIMES1:31;

reconsider P43 = 43 as Prime by XPRIMES1:43;

reconsider P47 = 47 as Prime by XPRIMES1:47;

reconsider P67 = 67 as Prime by XPRIMES1:67;

reconsider P71 = 71 as Prime by XPRIMES1:71;

reconsider P101 = 101 as Prime by XPRIMES1:101;

theorem :: NUMBER07:66

33 satisfies_Sierpinski_problem_89

proof end;

theorem :: NUMBER07:67

85 satisfies_Sierpinski_problem_89

proof end;

theorem :: NUMBER07:68

93 satisfies_Sierpinski_problem_89

proof end;

theorem :: NUMBER07:69

141 satisfies_Sierpinski_problem_89

proof end;