NUMBER08: Elementary Number Theory Problems. {P}art {VIII}

proof end;

end;

registration

let p be Prime;
let n be non zero Nat;

cluster p |-count (p |^ n) -> non zero ;

coherence by NAT_3:25, INT_2:def 4;

end;

theorem Th13: :: NUMBER08:13

for b being finite-support Function holds dom (b * (canFS (support b))) = dom (canFS (support b))

proof end;

theorem Th14: :: NUMBER08:14

for f, g being complex-valued Function holds support (f (#) g) c= support f

proof end;

registration

let f, g be complex-valued finite-support Function;

cluster f (#) g -> finite-support ;

proof end;

end;

theorem Th15: :: NUMBER08:15

for f, g being complex-valued Function st support f = support g holds
support (f (#) g) = support f

proof end;

theorem Th16: :: NUMBER08:16

for X being set
for b1, b2 being complex-valued finite-support ManySortedSet of X st support b1 = support b2 holds
Product (b1 (#) b2) = (Product b1) * (Product b2)

proof end;

definition

let n be non zero Nat;
set A = support (ppf n);

func Euler_factorization n -> Function means :Def1: :: NUMBER08:def 1
( dom it = support (ppf n) & ( for p being Nat st p in dom it holds
ex c being non zero Nat st
( c = p |-count n & it . p = (p |^ c) - (p |^ (c - 1)) ) ) );

proof end;

proof end;

end;

:: deftheorem Def1 defines Euler_factorization NUMBER08:def 1 :

registration

let n be non zero Nat;

cluster proj1 (Euler_factorization n) -> finite ;

proof end;

end;

registration

let n be non zero Nat;

cluster Euler_factorization n -> SetPrimes -defined ;

proof end;

end;

theorem Th17: :: NUMBER08:17

for n being non zero Nat
for p being object st p in dom (Euler_factorization n) holds
p is Prime

proof end;

theorem Th18: :: NUMBER08:18

for n being non zero Nat
for p being Nat st p in dom (Euler_factorization n) holds
ex c being non zero Nat st
( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) )

proof end;

registration

let n be non zero Nat;

cluster Euler_factorization n -> natural-valued ;

proof end;

end;

registration

let n be non zero Nat;

cluster Euler_factorization n -> finite-support ;

proof end;

end;

registration

cluster Euler_factorization 1 -> empty ;

proof end;

end;

theorem Th19: :: NUMBER08:19

for p being Prime
for n being non zero Nat holds Euler_factorization (p |^ n) = p .--> ((p |^ n) - (p |^ (n - 1)))

proof end;

theorem :: NUMBER08:20

for p being Prime holds Euler_factorization p = p .--> (p - 1)

proof end;

theorem Th21: :: NUMBER08:21

for n being non zero Nat holds support (Euler_factorization n) = dom (Euler_factorization n)

proof end;

theorem Th22: :: NUMBER08:22

for n being non zero Nat st n > 1 holds
not support (Euler_factorization n) is empty

proof end;

theorem :: NUMBER08:23

for n being non zero Nat st n > 1 holds
not Euler_factorization n is empty

proof end;

set B = EmptyBag SetPrimes;

theorem Th24: :: NUMBER08:24

for s, t being non zero Nat st s,t are_coprime holds
dom (Euler_factorization s) misses dom (Euler_factorization t)

proof end;

theorem Th25: :: NUMBER08:25

for s, t being non zero Nat st s,t are_coprime holds
(EmptyBag SetPrimes) +* (Euler_factorization (s * t)) = ((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t))

proof end;

theorem Th26: :: NUMBER08:26

for n being non zero Nat holds Euler n = Product ((EmptyBag SetPrimes) +* (Euler_factorization n))

proof end;

definition

let n be non zero Nat;
set A = support (ppf n);

func Euler_factorization_1 n -> Function means :Def2: :: NUMBER08:def 2
( dom it = support (ppf n) & ( for p being Nat st p in dom it holds
ex c being non zero Nat st
( c = p |-count n & it . p = p |^ (c - 1) ) ) );

proof end;

proof end;

end;

:: deftheorem Def2 defines Euler_factorization_1 NUMBER08:def 2 :

registration

let n be non zero Nat;

cluster proj1 (Euler_factorization_1 n) -> finite ;

proof end;

end;

registration

let n be non zero Nat;

cluster Euler_factorization_1 n -> SetPrimes -defined ;

proof end;

end;

theorem Th27: :: NUMBER08:27

for n being non zero Nat
for p being object st p in dom (Euler_factorization_1 n) holds
p is Prime

proof end;

registration

let n be non zero Nat;

cluster Euler_factorization_1 n -> natural-valued ;

proof end;

end;

registration

let n be non zero Nat;

cluster Euler_factorization_1 n -> finite-support ;

proof end;

end;

theorem Th28: :: NUMBER08:28

for n being non zero Nat holds support (Euler_factorization_1 n) = dom (Euler_factorization_1 n)

proof end;

definition

let n be non zero Nat;
set A = support (ppf n);
deffunc H₁( Nat) -> set = $1 - 1;

func Euler_factorization_2 n -> Function means :Def3: :: NUMBER08:def 3
( dom it = support (ppf n) & ( for p being Nat st p in dom it holds
it . p = p - 1 ) );

proof end;

proof end;

end;

:: deftheorem Def3 defines Euler_factorization_2 NUMBER08:def 3 :

registration

let n be non zero Nat;

cluster proj1 (Euler_factorization_2 n) -> finite ;

proof end;

end;

registration

let n be non zero Nat;

cluster Euler_factorization_2 n -> SetPrimes -defined ;

proof end;

end;

theorem Th29: :: NUMBER08:29

for n being non zero Nat
for p being object st p in dom (Euler_factorization_2 n) holds
p is Prime

proof end;

registration

let n be non zero Nat;

cluster Euler_factorization_2 n -> natural-valued ;

proof end;

end;

registration

let n be non zero Nat;

cluster Euler_factorization_2 n -> finite-support ;

proof end;

end;

theorem Th30: :: NUMBER08:30

for n being non zero Nat holds support (Euler_factorization_2 n) = dom (Euler_factorization_2 n)

proof end;

theorem Th31: :: NUMBER08:31

for n being non zero Nat holds (EmptyBag SetPrimes) +* (Euler_factorization n) = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) (#) ((EmptyBag SetPrimes) +* (Euler_factorization_2 n))

proof end;

theorem Th32: :: NUMBER08:32

for f1, f2 being integer-valued FinSequence st len f1 = len f2 & ( for n being Nat st 1 <= n & n <= len f1 holds
f1 . n divides f2 . n ) holds
Product f1 divides Product f2

proof end;

theorem Th33: :: NUMBER08:33

for n being non zero Nat holds Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) divides n

proof end;

definition

let f be real-valued Function;
let r be Real;

pred f <= r means :: NUMBER08:def 4
for x being object st x in dom f holds
f . x <= r;

end;

:: deftheorem defines <= NUMBER08:def 4 :

theorem :: NUMBER08:34

for f being real-valued Function
for r1, r2 being Real st f <= r1 & r1 <= r2 holds
f <= r2

proof end;

theorem Th35: :: NUMBER08:35

for n being Nat
for f, g being real-valued Function st rng g c= rng f & f <= n holds
g <= n

proof end;

theorem Th36: :: NUMBER08:36

for f, g being ext-real-valued FinSequence st f ^ g is increasing holds
( f is increasing & g is increasing )

proof end;

theorem Th37: :: NUMBER08:37

for f, g being ext-real-valued FinSequence st f ^ g is positive-yielding holds
( f is positive-yielding & g is positive-yielding )

proof end;

theorem Th38: :: NUMBER08:38

for n being Nat
for f being natural-valued FinSequence st f <= n & f is increasing & f is positive-yielding holds
Product f divides n !

proof end;

registration

let f be natural-valued FinSequence;

cluster sort_a f -> natural-valued ;

proof end;

cluster sort_d f -> natural-valued ;

proof end;

end;

registration

let f be integer-valued FinSequence;

cluster sort_a f -> integer-valued ;

proof end;

cluster sort_d f -> integer-valued ;

proof end;

end;

registration

let f be rational-valued FinSequence;

cluster sort_a f -> rational-valued ;

proof end;

cluster sort_d f -> rational-valued ;

proof end;

end;

theorem Th39: :: NUMBER08:39

for P, R being Relation st rng R c= rng P & P is positive-yielding holds
R is positive-yielding

proof end;

registration

let f be real-valued positive-yielding FinSequence;

cluster sort_a f -> positive-yielding ;

proof end;

end;

registration

cluster Relation-like SetPrimes -defined Function-like -> NAT -defined for set ;

proof end;

end;

theorem Th40: :: NUMBER08:40

for n being Nat
for f being real-valued finite-support Function st f <= n holds
for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F <= n

proof end;

theorem Th41: :: NUMBER08:41

for f being natural-valued finite-support Function
for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F is positive-yielding

proof end;

theorem :: NUMBER08:42

for f being SetPrimes -defined natural-valued finite-support Function st f is increasing holds
for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
sort_a F is one-to-one

proof end;

theorem Th43: :: NUMBER08:43

proof end;

theorem Th44: :: NUMBER08:44

for n being Nat
for f being SetPrimes -defined natural-valued finite-support Function st f <= n & f is increasing holds
Product ((EmptyBag SetPrimes) +* f) divides n !

proof end;

theorem Th45: :: NUMBER08:45

for n being non zero Nat holds Euler_factorization_2 n <= n - 1

proof end;

registration

let n be non zero Nat;

cluster Euler_factorization_2 n -> increasing ;

proof end;

cluster Euler_factorization_2 n -> positive-yielding ;

proof end;

end;

theorem :: NUMBER08:46

for n being non zero Nat holds Product ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) divides (n - 1) ! by Th45, Th44;

theorem Th47: :: NUMBER08:47

for n being non zero Nat holds Euler n divides n !

proof end;

:: Problem 25

theorem :: NUMBER08:48

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

proof end;

theorem Th49: :: NUMBER08:49

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

proof end;

definition

let n be Nat;

pred n satisfies_Sierpinski_problem_86 means :: NUMBER08:def 5
ex p1, p2, p3 being Prime st
( p1,p2,p3 are_mutually_distinct & (n |^ 2) - 1 = (p1 * p2) * p3 );

end;

:: deftheorem defines satisfies_Sierpinski_problem_86 NUMBER08:def 5 :

Lm15: for a1, b1, c1, a2, b2, c2 being Nat st a1 <= a2 & b1 <= b2 & c1 <= c2 holds
(a1 * b1) * c1 <= (a2 * b2) * c2

proof end;

theorem Th50: :: NUMBER08:50

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

proof end;

theorem Th51: :: NUMBER08:51

for n being Nat
for a, b, c being Prime holds
( not (n |^ 2) - 1 = (a * b) * c or n - 1 is prime or n + 1 is prime )

proof end;

theorem Th52: :: NUMBER08:52

for n being Nat holds
( not n satisfies_Sierpinski_problem_86 or ( n - 1 is prime & ex x, y being Prime st
( x <> y & n + 1 = x * y ) ) or ( n + 1 is prime & ex x, y being Prime st
( x <> y & n - 1 = x * y ) ) )

proof end;

theorem Th53: :: NUMBER08:53

for n being Nat st n satisfies_Sierpinski_problem_86 holds
n is even

proof end;

theorem Th54: :: NUMBER08:54

(14 |^ 2) - 1 = (3 * 5) * 13

proof end;

theorem Th55: :: NUMBER08:55

(16 |^ 2) - 1 = (3 * 5) * 17

proof end;

theorem Th56: :: NUMBER08:56

(20 |^ 2) - 1 = (3 * 7) * 19

proof end;

theorem Th57: :: NUMBER08:57

(22 |^ 2) - 1 = (3 * 7) * 23

proof end;

theorem Th58: :: NUMBER08:58

(32 |^ 2) - 1 = (3 * 11) * 31

proof end;

::Problem 86 a

theorem :: NUMBER08:59

14 satisfies_Sierpinski_problem_86

proof end;

::Problem 86 b

theorem :: NUMBER08:60

16 satisfies_Sierpinski_problem_86

proof end;

::Problem 86 c

theorem :: NUMBER08:61

20 satisfies_Sierpinski_problem_86

proof end;

::Problem 86 d

theorem :: NUMBER08:62

22 satisfies_Sierpinski_problem_86

proof end;

::Problem 86 e

theorem :: NUMBER08:63

32 satisfies_Sierpinski_problem_86

proof end;

Lm16: not 6 satisfies_Sierpinski_problem_86

proof end;

Lm17: not 7 satisfies_Sierpinski_problem_86

proof end;

Lm18: not 8 satisfies_Sierpinski_problem_86

proof end;

Lm19: not 9 satisfies_Sierpinski_problem_86

proof end;

Lm20: not 10 satisfies_Sierpinski_problem_86

proof end;

Lm21: not 11 satisfies_Sierpinski_problem_86

proof end;

Lm22: not 12 satisfies_Sierpinski_problem_86

proof end;

Lm23: not 13 satisfies_Sierpinski_problem_86

proof end;

Lm24: not 15 satisfies_Sierpinski_problem_86

proof end;

Lm25: not 17 satisfies_Sierpinski_problem_86

proof end;

Lm26: not 18 satisfies_Sierpinski_problem_86

proof end;

Lm27: not 19 satisfies_Sierpinski_problem_86

proof end;

Lm28: not 21 satisfies_Sierpinski_problem_86

proof end;

Lm29: not 23 satisfies_Sierpinski_problem_86

proof end;

Lm30: not 24 satisfies_Sierpinski_problem_86

proof end;

Lm31: not 25 satisfies_Sierpinski_problem_86

proof end;

Lm32: not 26 satisfies_Sierpinski_problem_86

proof end;

Lm33: not 27 satisfies_Sierpinski_problem_86

proof end;

Lm34: not 28 satisfies_Sierpinski_problem_86

proof end;

Lm35: not 29 satisfies_Sierpinski_problem_86

proof end;

Lm36: not 30 satisfies_Sierpinski_problem_86

proof end;

Lm37: not 31 satisfies_Sierpinski_problem_86

proof end;

:: Problem 86

theorem :: NUMBER08:64

for n being Nat st n satisfies_Sierpinski_problem_86 & n <= 32 holds
n in {14,16,20,22,32}

proof end;

theorem Th65: :: NUMBER08:65

for k being Nat holds 3 |^ (2 * k),1 are_congruent_mod 8

proof end;

theorem Th66: :: NUMBER08:66

for n being Nat holds not 8 divides (3 |^ n) + 1

proof end;

:: Problem 184

theorem Th67: :: NUMBER08:67

for m, n being Nat st n <> 0 & (2 |^ m) - (3 |^ n) = 1 holds
( m = 2 & n = 1 )

proof end;

theorem Th68: :: NUMBER08:68

for k being Nat holds 3 |^ (2 * k),1 are_congruent_mod 4

proof end;

theorem Th69: :: NUMBER08:69

for n being Nat st (2 |^ n) mod 4 = 2 holds
n = 1

proof end;

theorem Th70: :: NUMBER08:70

for m, n being Nat st (2 |^ m) - (2 |^ n) = 2 holds
( m = 2 & n = 1 )

proof end;

theorem Th71: :: NUMBER08:71

for m, n being Nat st n is odd & (3 |^ n) - (2 |^ m) = 1 holds
( n = m & m = 1 )

proof end;

theorem Th72: :: NUMBER08:72

for m, n being Nat st n is even & (3 |^ n) - (2 |^ m) = 1 holds
( n = 2 & m = 3 )

proof end;

:: Problem 185

theorem Th73: :: NUMBER08:73

for m, n being Nat holds
( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) )

proof end;

definition

let n be Nat;

attr n is having_exactly_one_prime_divisor means :: NUMBER08:def 6
ex p being Prime st
( p divides n & ( for r being Prime st r <> p holds
not r divides n ) );

end;

:: deftheorem defines having_exactly_one_prime_divisor NUMBER08:def 6 :

definition

let n be Nat;
assume A1: n is having_exactly_one_prime_divisor ;

func the_only_divisor_of n -> Prime means :Def7: :: NUMBER08:def 7
( it divides n & ( for r being Prime st r <> it holds
not r divides n ) );

existence by A1;
uniqueness ;

end;

:: deftheorem Def7 defines the_only_divisor_of NUMBER08:def 7 :

theorem :: NUMBER08:74

for n being Nat
for p being Prime st n is having_exactly_one_prime_divisor & p divides n holds
the_only_divisor_of n = p by Def7;

registration

cluster natural prime -> having_exactly_one_prime_divisor for set ;

proof end;

end;

theorem :: NUMBER08:75

for p being Prime holds the_only_divisor_of p = p by Def7;

registration

cluster natural zero -> non having_exactly_one_prime_divisor for set ;

proof end;

end;

theorem :: NUMBER08:76

not 1 is having_exactly_one_prime_divisor by NAT_D:7, INT_2:def 4;

registration

let p be Prime;

cluster p |^ 0 -> non having_exactly_one_prime_divisor ;

proof end;

end;

registration

let p be Prime;
let k be non zero Nat;

cluster p |^ k -> having_exactly_one_prime_divisor ;

proof end;

end;

theorem Th77: :: NUMBER08:77

for p1, p2 being Prime st p1 <> p2 holds
not p1 * p2 is having_exactly_one_prime_divisor

proof end;

theorem Th78: :: NUMBER08:78

for n being Nat st n is having_exactly_one_prime_divisor holds
ex k being non zero Nat st n = (the_only_divisor_of n) |^ k

proof end;

:: Problem 88

theorem :: NUMBER08:79

for n being Nat st n > 7 holds
ex m being Nat ex p, q being Prime st
( p <> q & ( m = n or m = n + 1 or m = n + 2 ) & p divides m & q divides m )

proof end;

definition

let n be Nat;

attr n is having_at_least_three_different_prime_divisors means :: NUMBER08:def 8
ex q1, q2, q3 being Prime st
( q1,q2,q3 are_mutually_distinct & q1 divides n & q2 divides n & q3 divides n );

end;

:: deftheorem defines having_at_least_three_different_prime_divisors NUMBER08:def 8 :

definition

let n be non zero Nat;

pred n satisfies_Sierpinski_problem_105 means :: NUMBER08:def 9
( n - 1 is having_at_least_three_different_prime_divisors & n + 1 is having_at_least_three_different_prime_divisors );

end;

:: deftheorem defines satisfies_Sierpinski_problem_105 NUMBER08:def 9 :

reconsider P2 = 2 as Prime by XPRIMES1:2;

reconsider P3 = 3 as Prime by XPRIMES1:3;

reconsider P5 = 5 as Prime by XPRIMES1:5;

theorem :: NUMBER08:80

for n being Nat st n is having_exactly_one_prime_divisor holds
not n is having_at_least_three_different_prime_divisors

proof end;

registration

cluster natural zero -> having_at_least_three_different_prime_divisors for set ;

proof end;

end;

theorem Th81: :: NUMBER08:81

for n being Nat st n > 0 & n is having_at_least_three_different_prime_divisors holds
n >= 30

proof end;

registration

cluster natural prime -> non having_at_least_three_different_prime_divisors for set ;

proof end;

end;

registration

let p1, p2 be Prime;

cluster p1 * p2 -> non having_at_least_three_different_prime_divisors ;

proof end;

end;

registration

let p be Prime;
let n be Nat;

cluster p |^ n -> non having_at_least_three_different_prime_divisors ;

proof end;

end;

registration

let p1, p2 be Prime;
let m, n be Nat;

cluster (p1 |^ m) * (p2 |^ n) -> non having_at_least_three_different_prime_divisors ;

proof end;

end;

:: Problem 105 a

theorem :: NUMBER08:82

131 satisfies_Sierpinski_problem_105

proof end;

Lm38: not 37 satisfies_Sierpinski_problem_105

proof end;

Lm39: not 41 satisfies_Sierpinski_problem_105

proof end;

Lm40: not 43 satisfies_Sierpinski_problem_105

proof end;

Lm41: not 47 satisfies_Sierpinski_problem_105

proof end;

Lm42: not 53 satisfies_Sierpinski_problem_105

proof end;

Lm43: not 59 satisfies_Sierpinski_problem_105

proof end;

Lm44: not 61 satisfies_Sierpinski_problem_105

proof end;

Lm45: not 67 satisfies_Sierpinski_problem_105

proof end;

Lm46: not 71 satisfies_Sierpinski_problem_105

proof end;

Lm47: not 73 satisfies_Sierpinski_problem_105

proof end;

Lm48: not 79 satisfies_Sierpinski_problem_105

proof end;

Lm49: not 83 satisfies_Sierpinski_problem_105

proof end;

Lm50: not 89 satisfies_Sierpinski_problem_105

proof end;

Lm51: not 97 satisfies_Sierpinski_problem_105

proof end;

Lm52: not 101 satisfies_Sierpinski_problem_105

proof end;

Lm53: not 103 satisfies_Sierpinski_problem_105

proof end;

Lm54: not 107 satisfies_Sierpinski_problem_105

proof end;

Lm55: not 109 satisfies_Sierpinski_problem_105

proof end;

Lm56: not 113 satisfies_Sierpinski_problem_105

proof end;

:: Problem 105

theorem :: NUMBER08:83

for p being Prime holds
( not p <= 130 or not p satisfies_Sierpinski_problem_105 )

proof end;

theorem :: NUMBER08:84

(((1 + 3) + (3 |^ 2)) + (3 |^ 3)) + (3 |^ 4) = 11 |^ 2 by Lm8, Lm9, Lm10, Lm11;

theorem Th85: :: NUMBER08:85

for m being Nat
for p being Prime holds
( m divides p |^ 4 iff m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} )

proof end;

theorem Th86: :: NUMBER08:86

for p being Prime holds
( (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square iff p = 3 )

proof end;

:: Problem 111 a

theorem :: NUMBER08:87

for p being Prime holds NatDivisors (p |^ 4) = {1,p,(p |^ 2),(p |^ 3),(p |^ 4)}

proof end;

:: Problem 111

theorem :: NUMBER08:88

{ p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } = {3}

proof end;

registration

let D be non empty set ;

cluster Function-like V33( omega ,D) -> total for Element of bool [:omega,D:];

proof end;

end;

registration

let D be non empty set ;
let f be [:COMPLEX,D:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `1 -> complex ;

proof end;

end;

registration

let D be non empty set ;
let f be [:D,COMPLEX:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `2 -> complex ;

proof end;

end;

registration

let D be non empty set ;
let f be [:REAL,D:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `1 -> real ;

proof end;

end;

registration

let D be non empty set ;
let f be [:D,REAL:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `2 -> real ;

proof end;

end;

registration

let D be non empty set ;
let f be [:RAT,D:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `1 -> rational ;

proof end;

end;

registration

let D be non empty set ;
let f be [:D,RAT:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `2 -> rational ;

proof end;

end;

registration

let D be non empty set ;
let f be [:INT,D:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `1 -> integer ;

proof end;

end;

registration

let D be non empty set ;
let f be [:D,INT:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `2 -> integer ;

proof end;

end;

registration

let D be non empty set ;
let f be [:NAT,D:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `1 -> natural ;

proof end;

end;

registration

let D be non empty set ;
let f be [:D,NAT:] -valued ManySortedSet of NAT ;
let n be Nat;

cluster (f . n) `2 -> natural ;

proof end;

end;

definition

let a, b, x1, x2, x3, y1, y2, y3 be Complex;

func recSeqCart (a,b,x1,x2,x3,y1,y2,y3) -> [:COMPLEX,COMPLEX:] -valued ManySortedSet of NAT means :Def10: :: NUMBER08:def 10
( it . 0 = [a,b] & ( for n being Nat holds it . (n + 1) = [(((x1 * ((it . n) `1)) + (x2 * ((it . n) `2))) + x3),(((y1 * ((it . n) `1)) + (y2 * ((it . n) `2))) + y3)] ) );

proof end;

proof end;

end;

:: deftheorem Def10 defines recSeqCart NUMBER08:def 10 :

registration

let a, b, x1, x2, x3, y1, y2, y3 be Real;

cluster recSeqCart (a,b,x1,x2,x3,y1,y2,y3) -> [:REAL,REAL:] -valued [:COMPLEX,COMPLEX:] -valued ;

proof end;

end;

registration

let a, b, x1, x2, x3, y1, y2, y3 be Rational;

cluster recSeqCart (a,b,x1,x2,x3,y1,y2,y3) -> [:COMPLEX,COMPLEX:] -valued [:RAT,RAT:] -valued ;

proof end;

end;

registration

let a, b, x1, x2, x3, y1, y2, y3 be Integer;

cluster recSeqCart (a,b,x1,x2,x3,y1,y2,y3) -> [:COMPLEX,COMPLEX:] -valued [:INT,INT:] -valued ;

proof end;

end;

registration

let a, b, x1, x2, x3, y1, y2, y3 be Nat;

cluster recSeqCart (a,b,x1,x2,x3,y1,y2,y3) -> [:NAT,NAT:] -valued [:COMPLEX,COMPLEX:] -valued ;

proof end;

end;

theorem Th89: :: NUMBER08:89

for a, b, a1, a2, a3, b1, b2, b3 being Real st a > 0 & b > 0 & a3 >= 0 & b3 >= 0 & ( ( a1 > 0 & a2 >= 0 ) or ( a1 >= 0 & a2 > 0 ) ) & ( ( b1 > 0 & b2 >= 0 ) or ( b1 >= 0 & b2 > 0 ) ) holds
for n being Nat holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 > 0 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 > 0 )

proof end;

theorem Th90: :: NUMBER08:90

for a, b, a1, a2, a3, b1, b2, b3 being Real st a >= 0 & b >= 0 & a1 >= 0 & a2 >= 0 & a3 >= 0 & b1 >= 0 & b2 >= 0 & b3 >= 0 holds
for n being Nat holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 >= 0 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 >= 0 )

proof end;

theorem Th91: :: NUMBER08:91

for a, b, a1, a2, a3, b1, b2, b3 being Real st a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 holds
for m, n being Nat st m > n holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . m) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . m) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 )

proof end;

theorem Th92: :: NUMBER08:92

for a, b, a1, a2, a3, b1, b2, b3 being Real st a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 holds
recSeqCart (a,b,a1,a2,a3,b1,b2,b3) is one-to-one

proof end;

::Problem 137

theorem :: NUMBER08:93

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

proof end;

registration

cluster infinite natural-membered for set ;

proof end;

end;

theorem Th94: :: NUMBER08:94

for i being Integer
for p being Prime holds
( not i divides p or i = 1 or i = - 1 or i = p or i = - p )

proof end;

:: Problem 138 a

theorem :: NUMBER08:95

{ [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } = {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]}

proof end;

theorem Th96: :: NUMBER08:96

for r being Complex st r <> 0 holds
((2 * ((7 / r) |^ 3)) + ((7 / r) * (r - (98 / (r ^2))))) - 7 = 0

proof end;

theorem Th97: :: NUMBER08:97

for n being Nat st n |^ 3 <= 98 holds
n <= 4

proof end;

:: Problem 138 b

theorem :: NUMBER08:98

{ [x,y] where x, y is positive Rational : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } is infinite

proof end;

:: Problem 139

theorem :: NUMBER08:99

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

proof end;

registration

let a be Rational;
let n be Nat;

cluster a |^ n -> rational ;

proof end;

end;

registration

let a be Rational;
let i be Integer;

cluster a #Z i -> rational ;

proof end;

end;

registration

let a be Rational;
let i be Integer;

cluster a to_power i -> rational ;