NUMBER09: Elementary Number Theory Problems. {P}art {IX}

:: Elementary Number Theory Problems. {P}art {IX}
:: by Artur Korni{\l}owicz
::
:: Received November 21, 2023
:: Copyright (c) 2023-2024 Association of Mizar Users

Lm1: 2 |^ 0 = 1
by NEWTON:4;

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

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

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

Lm5: 2 |^ 5 = (((2 * 2) * 2) * 2) * 2
by NUMBER02:1;

Lm6: 2 |^ 6 = ((((2 * 2) * 2) * 2) * 2) * 2
by NUMBER02:2;

Lm7: 2 |^ 7 = (((((2 * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER02:3;

Lm8: 2 |^ 8 = ((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER02:4;

Lm9: 2 |^ 9 = (((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER02:5;

theorem Th1: :: NUMBER09:1

for z being Complex holds z |^ 11 = (((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th2: :: NUMBER09:2

for z being Complex holds z |^ 12 = ((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th3: :: NUMBER09:3

for z being Complex holds z |^ 13 = (((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th4: :: NUMBER09:4

for z being Complex holds z |^ 14 = ((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th5: :: NUMBER09:5

for z being Complex holds z |^ 15 = (((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th6: :: NUMBER09:6

for z being Complex holds z |^ 16 = ((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th7: :: NUMBER09:7

for z being Complex holds z |^ 17 = (((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th8: :: NUMBER09:8

for z being Complex holds z |^ 18 = ((((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th9: :: NUMBER09:9

for z being Complex holds z |^ 19 = (((((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

theorem Th10: :: NUMBER09:10

for z being Complex holds z |^ 20 = ((((((((((((((((((z * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z) * z

proof end;

Lm10: 2 |^ 11 = (((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by Th1;

Lm11: 2 |^ 13 = (((((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by Th3;

Lm12: 2 |^ 15 = (((((((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by Th5;

Lm13: 2 |^ 17 = (((((((((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by Th7;

Lm14: 2 |^ 19 = (((((((((((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by Th9;

theorem :: NUMBER09:11

for n being Nat st n >= 2 holds
ex k being positive Nat st (2 |^ n) - 1 = (4 * k) - 1

proof end;

registration

cluster finite natural-membered with_non-empty_elements -> finite included_in_Seg natural-membered for set ;

proof end;

end;

registration

let a, r be Nat;

cluster ArProg (a,r) -> natural-valued ;

proof end;

end;

definition

let i be Integer;

func Coprimes i -> Subset of INT equals :: NUMBER09:def 2
{ j where j is Integer : i,j are_coprime } ;

proof end;

end;

:: deftheorem NUMBER09:def 1 :

:: deftheorem defines Coprimes NUMBER09:def 2 :

theorem Th12: :: NUMBER09:12

for p being Prime
for X being included_in_Seg set st X c= SetPrimes & p divides Product (Sgm X) holds
p in X

proof end;

Lm15: now :: thesis:

let a, m be Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & p divides a ) } ;

assume 0 in { p where p is Prime : ( p divides m & p divides a ) } ; :: thesis:
then ex p being Prime st
( p = 0 & p divides m & p divides a ) ;
hence contradiction ; :: thesis:

end;

hence { p where p is Prime : ( p divides m & p divides a ) } is with_non-empty_elements by SETFAM_1:def 8; :: thesis:

end;

Lm16: now :: thesis:

let a, b, m be Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ;

assume 0 in { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ; :: thesis:
then ex p being Prime st
( p = 0 & p divides m & not p divides a & not p divides b ) ;
hence contradiction ; :: thesis:

end;

hence { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is with_non-empty_elements by SETFAM_1:def 8; :: thesis:

end;

Lm17: now :: thesis:

let a be Nat; :: thesis:
let m be non zero Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & p divides a ) } ;
{ p where p is Prime : ( p divides m & p divides a ) } c= NatDivisors m

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Prime : ( p divides m & p divides a ) } ; :: thesis:
then ex p being Prime st
( x = p & p divides m & p divides a ) ;
hence x in NatDivisors m ; :: thesis:

end;

hence { p where p is Prime : ( p divides m & p divides a ) } is finite ; :: thesis:

end;

Lm18: now :: thesis:

let a, b be Nat; :: thesis:
let m be non zero Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ;
{ p where p is Prime : ( p divides m & not p divides a & not p divides b ) } c= NatDivisors m

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ; :: thesis:
then ex p being Prime st
( x = p & p divides m & not p divides a & not p divides b ) ;
hence x in NatDivisors m ; :: thesis:

end;

hence { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is finite ; :: thesis:

end;

Lm19: now :: thesis:

let a be Nat; :: thesis:
let m be non zero Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & p divides a ) } ;
{ p where p is Prime : ( p divides m & p divides a ) } c= NAT

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Prime : ( p divides m & p divides a ) } ; :: thesis:
then ex p being Prime st
( x = p & p divides m & p divides a ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis:

end;

hence { p where p is Prime : ( p divides m & p divides a ) } is natural-membered ; :: thesis:

end;

Lm20: now :: thesis:

let a, b be Nat; :: thesis:
let m be non zero Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ;
{ p where p is Prime : ( p divides m & not p divides a & not p divides b ) } c= NAT

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ; :: thesis:
then ex p being Prime st
( x = p & p divides m & not p divides a & not p divides b ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis:

end;

hence { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is natural-membered ; :: thesis:

end;

Lm21: now :: thesis:

let a be Nat; :: thesis:
let m be non zero Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & p divides a ) } ;
A1: { p where p is Prime : ( p divides m & p divides a ) } is with_non-empty_elements by Lm15;
A2: { p where p is Prime : ( p divides m & p divides a ) } is finite by Lm17;
{ p where p is Prime : ( p divides m & p divides a ) } is natural-membered by Lm19;
hence { p where p is Prime : ( p divides m & p divides a ) } is included_in_Seg by A1, A2; :: thesis:

end;

Lm22: now :: thesis:

let a, b be Nat; :: thesis:
let m be non zero Nat; :: thesis:
set A = { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ;
A1: { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is with_non-empty_elements by Lm16;
A2: { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is finite by Lm18;
{ p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is natural-membered by Lm20;
hence { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } is included_in_Seg by A1, A2; :: thesis:

end;

Lm23: now :: thesis:

let a, m be Nat; :: thesis:
thus { p where p is Prime : ( p divides m & p divides a ) } c= SetPrimes :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Prime : ( p divides m & p divides a ) } ; :: thesis:
then ex p being Prime st
( x = p & p divides m & p divides a ) ;
hence x in SetPrimes by NEWTON:def 6; :: thesis:

end;

end;

Lm24: now :: thesis:

let a, b, m be Nat; :: thesis:
thus { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } c= SetPrimes :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Prime : ( p divides m & not p divides a & not p divides b ) } ; :: thesis:
then ex p being Prime st
( x = p & p divides m & not p divides a & not p divides b ) ;
hence x in SetPrimes by NEWTON:def 6; :: thesis:

end;

end;

theorem Th13: :: NUMBER09:13

for a, b being Nat
for m being non zero Nat st a,b are_coprime holds
Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ), Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } ) are_coprime

proof end;

theorem Th14: :: NUMBER09:14

for a, b being Nat
for m being non zero Nat holds Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime

proof end;

theorem Th15: :: NUMBER09:15

for a, b being Nat
for m being non zero Nat st a,b are_coprime holds
Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime

proof end;

theorem Th16: :: NUMBER09:16

for a being Nat
for X being included_in_Seg set st a in X holds
a divides Product (Sgm X)

proof end;

:: Problem 62

theorem :: NUMBER09:17

for b being Nat
for a, m being non zero Nat st a,b are_coprime holds
(rng (ArProg (b,a))) /\ (Coprimes m) is infinite

proof end;

definition

let n be Complex;

attr n is a_product_of_two_primes means :: NUMBER09:def 3
ex p1, p2 being Prime st n = p1 * p2;

end;

:: deftheorem defines a_product_of_two_primes NUMBER09:def 3 :

notation

let n be Complex;
antonym not_a_product_of_two_primes n for a_product_of_two_primes ;

end;

registration

cluster natural prime -> not_a_product_of_two_primes for set ;

end;

registration

let p1, p2 be Prime;

cluster p1 * p2 -> a_product_of_two_primes ;

end;

theorem :: NUMBER09:18

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

theorem Th19: :: NUMBER09:19

for n being Nat st n is a_product_of_two_primes holds
n >= 4

proof end;

theorem :: NUMBER09:20

for c being Nat st c is_a_product_of_two_different_primes holds
c is a_product_of_two_primes ;

registration

let p1, p2, p3 be Prime;

cluster (p1 * p2) * p3 -> not_a_product_of_two_primes ;

proof end;

end;

theorem :: NUMBER09:21

for n being Nat st n is a_product_of_two_primes holds
for a, b being Nat st a <> 1 & b <> 1 & n = a * b holds
( a is prime & b is prime ) by NUMBER07:59;

Lm25: for n being Nat st (2 |^ n) - 1 <= 1000000 holds
not not n = 0 & ... & not n = 19

proof end;

theorem Th22: :: NUMBER09:22

for n being Nat st (2 |^ n) - 1 is prime & (2 |^ n) + 1 is prime holds
n = 2

proof end;

registration

let n be zero Nat;

cluster Mersenne n -> zero ;

proof end;

end;

registration

let n be non zero Nat;

cluster Mersenne n -> odd ;

end;

theorem Th23: :: NUMBER09:23

for p, q being Prime st p is odd & q divides Mersenne p holds
ex k being Nat st q = ((2 * k) * p) + 1

proof end;

Lm26: now :: thesis:

let k be Nat; :: thesis:
set K = 34 * k;
assume A1: ((34 * k) + 1) * ((34 * k) + 1) <= 131071 ; :: thesis:
thus k <= 10 :: thesis:

assume k > 10 ; :: thesis:
then k >= 10 + 1 by NAT_1:13;
then 34 * k >= 34 * 11 by XREAL_1:64;
then (34 * k) + 1 >= 374 + 1 by XREAL_1:6;
then ((34 * k) + 1) ^2 >= 375 ^2 by SQUARE_1:15;
hence contradiction by A1, XXREAL_0:2; :: thesis:

end;

end;

Lm27: now :: thesis:

let k be Nat; :: thesis:
set K = 38 * k;
assume A1: ((38 * k) + 1) * ((38 * k) + 1) <= 524287 ; :: thesis:
thus k <= 19 :: thesis:

assume k > 19 ; :: thesis:
then k >= 19 + 1 by NAT_1:13;
then 38 * k >= 38 * 20 by XREAL_1:64;
then (38 * k) + 1 >= 760 + 1 by XREAL_1:6;
then ((38 * k) + 1) ^2 >= 761 ^2 by SQUARE_1:15;
hence contradiction by A1, XXREAL_0:2; :: thesis:

end;

end;

theorem Th24: :: NUMBER09:24

Mersenne 17 is prime

proof end;

theorem Th25: :: NUMBER09:25

Mersenne 19 is prime

proof end;

:: Problem 91 a

theorem :: NUMBER09:26

{ ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } = {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

proof end;

definition

let n be Nat;

attr n is having_at_least_three_different_divisors means :: NUMBER09:def 4
ex q1, q2, q3 being Nat st
( q1,q2,q3 are_mutually_distinct & q1 > 1 & q2 > 1 & q3 > 1 & q1 divides n & q2 divides n & q3 divides n );

end;

:: deftheorem defines having_at_least_three_different_divisors NUMBER09:def 4 :

registration

cluster natural having_at_least_three_different_prime_divisors -> having_at_least_three_different_divisors for set ;

proof end;

end;

registration

cluster natural having_at_least_three_different_prime_divisors -> not_a_product_of_two_primes for set ;

end;

theorem :: NUMBER09:27

for n being Nat st n is having_at_least_three_different_prime_divisors holds
not n is_a_product_of_two_different_primes ;

:: Problem 91 b

theorem :: NUMBER09:28

for n being Nat st n is even & n > 4 holds
(2 |^ n) - 1 is having_at_least_three_different_divisors

proof end;

Lm28: for a being even Nat st 1 < a & a <= 100 & not a = 2 & not a = 4 & not a = 6 & not a = 8 & not a = 10 & not a = 12 & not a = 14 & not a = 16 & not a = 18 & not a = 20 & not a = 22 & not a = 24 & not a = 26 & not a = 28 & not a = 30 & not a = 32 & not a = 34 & not a = 36 & not a = 38 & not a = 40 & not a = 42 & not a = 44 & not a = 46 & not a = 48 & not a = 50 & not a = 52 & not a = 54 & not a = 56 & not a = 58 & not a = 60 & not a = 62 & not a = 64 & not a = 66 & not a = 68 & not a = 70 & not a = 72 & not a = 74 & not a = 76 & not a = 78 & not a = 80 & not a = 82 & not a = 84 & not a = 86 & not a = 88 & not a = 90 & not a = 92 & not a = 94 & not a = 96 & not a = 98 holds
a = 100

proof end;

theorem :: NUMBER09:29

for m, n being Nat st Fermat m = Fermat n holds
m = n

proof end;

theorem Th30: :: NUMBER09:30

for m, n being Nat st m < n holds
Fermat m < Fermat n

proof end;

theorem :: NUMBER09:31

for m, n being Nat st m <= n holds
Fermat m <= Fermat n

proof end;

theorem Th32: :: NUMBER09:32

for i, j being Integer st i,j are_congruent_mod j holds
j divides i

proof end;

theorem Th33: :: NUMBER09:33

for n being Nat
for i being Integer holds i * n,n are_congruent_mod n

proof end;

Lm29: 17 divides (2 |^ (2 |^ 2)) + 1
by Lm2, Lm4;

Lm30: 17 divides (4 |^ (2 |^ 1)) + 1

proof end;

Lm31: 17 divides (6 |^ (2 |^ 3)) + 1

proof end;

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

Lm33: 4097 = 17 * 241
;

Lm34: 17 divides (8 |^ (2 |^ 2)) + 1
by Lm32, Lm33, Lm2;

Lm35: 17 divides (10 |^ (2 |^ 3)) + 1

proof end;

Lm36: 17 divides (12 |^ (2 |^ 3)) + 1

proof end;

Lm37: 17 divides (14 |^ (2 |^ 3)) + 1

proof end;

Lm38: 17 divides (20 |^ (2 |^ 3)) + 1

proof end;

Lm39: 17 divides (22 |^ (2 |^ 3)) + 1

proof end;

Lm40: 17 divides (24 |^ (2 |^ 3)) + 1

proof end;

Lm41: 17 divides (26 |^ (2 |^ 2)) + 1

proof end;

Lm42: 17 divides (28 |^ (2 |^ 3)) + 1

proof end;

Lm43: 17 divides (30 |^ (2 |^ 1)) + 1

proof end;

Lm44: 17 divides (32 |^ (2 |^ 2)) + 1

proof end;

Lm45: 257 divides (84 |^ (2 |^ 6)) + 1

proof end;

theorem Th34: :: NUMBER09:34

for a, k, m, n being Nat st a divides (m |^ k) + 1 holds
a divides (((a * n) + m) |^ k) + 1

proof end;

theorem Th35: :: NUMBER09:35

for k being Nat holds 17 divides (((34 * k) + 2) |^ (2 |^ 2)) + 1

proof end;

theorem Th36: :: NUMBER09:36

for k being Nat holds 17 divides (((34 * k) + 4) |^ (2 |^ 1)) + 1

proof end;

theorem Th37: :: NUMBER09:37

for k being Nat holds 17 divides (((34 * k) + 6) |^ (2 |^ 3)) + 1

proof end;

theorem Th38: :: NUMBER09:38

for k being Nat holds 17 divides (((34 * k) + 8) |^ (2 |^ 2)) + 1

proof end;

theorem Th39: :: NUMBER09:39

for k being Nat holds 17 divides (((34 * k) + 10) |^ (2 |^ 3)) + 1

proof end;

theorem Th40: :: NUMBER09:40

for k being Nat holds 17 divides (((34 * k) + 12) |^ (2 |^ 3)) + 1

proof end;

theorem Th41: :: NUMBER09:41

for k being Nat holds 17 divides (((34 * k) + 14) |^ (2 |^ 3)) + 1

proof end;

theorem Th42: :: NUMBER09:42

for k being Nat holds 17 divides (((34 * k) + 20) |^ (2 |^ 3)) + 1

proof end;

theorem Th43: :: NUMBER09:43

for k being Nat holds 17 divides (((34 * k) + 22) |^ (2 |^ 3)) + 1

proof end;

theorem Th44: :: NUMBER09:44

for k being Nat holds 17 divides (((34 * k) + 24) |^ (2 |^ 3)) + 1

proof end;

theorem Th45: :: NUMBER09:45

for k being Nat holds 17 divides (((34 * k) + 26) |^ (2 |^ 2)) + 1

proof end;

theorem Th46: :: NUMBER09:46

for k being Nat holds 17 divides (((34 * k) + 28) |^ (2 |^ 3)) + 1

proof end;

theorem Th47: :: NUMBER09:47

for k being Nat holds 17 divides (((34 * k) + 30) |^ (2 |^ 1)) + 1

proof end;

theorem Th48: :: NUMBER09:48

for k being Nat holds 17 divides (((34 * k) + 32) |^ (2 |^ 2)) + 1

proof end;

Lm46: 2 |^ (2 |^ (4 + 1)) = 2 |^ ((2 |^ 4) * (2 |^ 1)) by NEWTON:8
.= (2 |^ (2 |^ 4)) |^ 2 by NEWTON:9
.= (2 |^ (2 |^ 4)) * (2 |^ (2 |^ 4)) by WSIERP_1:1
.= (2 * 2) |^ (2 |^ 4) by NEWTON:7 ;

Lm47: 2 |^ (2 |^ (4 + 1)) = 4 |^ (2 |^ (3 + 1)) by Lm46
.= 4 |^ ((2 |^ 3) * (2 |^ 1)) by NEWTON:8
.= (4 |^ (2 |^ 3)) |^ (2 |^ 1) by NEWTON:9
.= (4 |^ (2 |^ 3)) * (4 |^ (2 |^ 3)) by WSIERP_1:1
.= (4 * 4) |^ (2 |^ 3) by NEWTON:7 ;

Lm48: for a, n being Nat st a > 4 & n > 0 holds
(a |^ (2 |^ n)) + 1 > 25

proof end;

Lm49: for a, n being Nat st a > 4 & n > 0 holds
(a |^ (2 |^ n)) + 1 > 17

proof end;

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

Lm51: Fermat 5 = (2 |^ (4 * 8)) + 1 by Lm5
.= (256 |^ 4) + 1 by Lm8, NEWTON:9 ;

:: Problem 125

theorem :: NUMBER09:49

for a being Nat st 1 < a & a <= 100 holds
ex n being positive Nat st
( n <= 6 & (a |^ (2 |^ n)) + 1 is composite )

proof end;

Lm52: for D being Integer st D > 0 holds
{ [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite

proof end;

Lm53: for D being Integer st D < 0 holds
{ [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite

proof end;

Lm54: { [x,y,z] where x, y, z is positive Nat : (x ^2) - (0 * (y ^2)) = z ^2 } is infinite

proof end;

:: Problem 143

theorem :: NUMBER09:50

for D being Integer holds { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite

proof end;

theorem Th51: :: NUMBER09:51

for n being Nat holds
( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

proof end;

:: Problem 146

theorem :: NUMBER09:52

for x, y, z being Nat holds ((x ^2) - (2 * (y ^2))) + (8 * z) <> 3

proof end;

:: Problem 147

theorem :: NUMBER09:53

{ [x,y] where x, y is Nat : (y ^2) - (((x * (x + 1)) * (x + 2)) * (x + 3)) = 1 } = { [x,y] where x, y is Nat : y = ((x ^2) + (3 * x)) + 1 }

proof end;

theorem Th54: :: NUMBER09:54

for a, b, c, d being positive Real st a / b < 1 & c / d < 1 holds
(a / b) * (c / d) < 1

proof end;

:: Problem 158 a

theorem :: NUMBER09:55

for x, y, z, t being positive Nat holds (((x / y) + (y / z)) + (z / t)) + (t / x) <> 1

proof end;

definition

let n be Nat;

func GreaterOrEqualsNumbers n -> Subset of NAT equals :: NUMBER09:def 5
NAT \ (Segm n);

end;

:: deftheorem defines GreaterOrEqualsNumbers NUMBER09:def 5 :

registration

let n be Nat;

cluster GreaterOrEqualsNumbers n -> infinite ;

end;

theorem Th56: :: NUMBER09:56

for k, n being Nat holds
( k in GreaterOrEqualsNumbers n iff n <= k )

proof end;

theorem :: NUMBER09:57

for k, n being Nat holds n + k in GreaterOrEqualsNumbers n by Th56, NAT_1:11;

theorem :: NUMBER09:58

for n being Nat holds n in GreaterOrEqualsNumbers n by Th56;

theorem :: NUMBER09:59

for k, n being Nat st k > 0 holds
not n in GreaterOrEqualsNumbers (n + k)

proof end;

registration

let n be Nat;

cluster -> n _or_greater for Element of GreaterOrEqualsNumbers n;

proof end;

end;

registration

let n be Nat;

cluster epsilon-transitive epsilon-connected ordinal natural complex V20() integer dim-like finite V49() ext-real non negative n _or_greater for set ;

proof end;

end;

theorem :: NUMBER09:60

for n being Nat
for k being b₁ _or_greater Nat holds k in GreaterOrEqualsNumbers n by EC_PF_2:def 1, Th56;

registration

let n be Nat;
let k be non zero Nat;

cluster k * n -> n _or_greater ;

proof end;

end;

registration

let n be Nat;
let k be n _or_greater Nat;

cluster k - n -> natural ;

proof end;

end;

:: Problem 158 b

theorem :: NUMBER09:61

{ [x,y,z,t] where x, y, z, t is Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 1 } is infinite

proof end;

:: Problem 166

theorem :: NUMBER09:62

1 / 2 = (((((((((((1 / (2 ^2)) + (1 / (3 ^2))) + (1 / (4 ^2))) + (1 / (6 ^2))) + (1 / (7 ^2))) + (1 / (9 ^2))) + (1 / (12 ^2))) + (1 / (14 ^2))) + (1 / (21 ^2))) + (1 / (36 ^2))) + (1 / (45 ^2))) + (1 / (60 ^2)) ;

:: Problem 178

theorem :: NUMBER09:63

for n being Nat holds ((((n + 1) |^ 3) + ((n + 2) |^ 3)) + ((n + 3) |^ 3)) + ((n + 4) |^ 3) <> (n + 5) |^ 3

proof end;

:: Problem 180

theorem :: NUMBER09:64

( 2 * (2 + 1) = (1 * (1 + 1)) * (1 + 2) & 14 * (14 + 1) = (5 * (5 + 1)) * (5 + 2) ) ;

:: Problem 181

theorem :: NUMBER09:65

{ [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 } is infinite

proof end;