NUMBER04: Elementary Number Theory Problems. {P}art {IV}

:: Elementary Number Theory Problems. {P}art {IV}
:: by Artur Korni{\l}owicz
::
:: Received September 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

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

Lm2: 2 |^ (1 + 1) = (2 |^ 1) * 2 by NEWTON:6
.= 4 ;

Lm3: 2 |^ (2 + 1) = (2 |^ 2) * 2 by NEWTON:6
.= 8 by Lm2 ;

Lm4: 2 |^ (3 + 1) = (2 |^ 3) * 2 by NEWTON:6
.= 16 by Lm3 ;

Lm5: 2 |^ (4 + 1) = (2 |^ 4) * 2 by NEWTON:6
.= 32 by Lm4 ;

Lm6: 2 |^ (5 + 1) = (2 |^ 5) * 2 by NEWTON:6
.= 64 by Lm5 ;

Lm7: 2 |^ (6 + 1) = (2 |^ 6) * 2 by NEWTON:6
.= 128 by Lm6 ;

Lm8: 2 |^ (7 + 1) = (2 |^ 7) * 2 by NEWTON:6
.= 256 by Lm7 ;

Lm9: 2 |^ (8 + 1) = (2 |^ 8) * 2 by NEWTON:6
.= 512 by Lm8 ;

Lm10: 2 |^ (9 + 1) = (2 |^ 9) * 2 by NEWTON:6
.= 1024 by Lm9 ;

Lm11: 2 |^ (10 + 1) = (2 |^ 10) * 2 by NEWTON:6
.= 2048 by Lm10 ;

Lm12: 2 |^ (11 + 1) = (2 |^ 11) * 2 by NEWTON:6
.= 4096 by Lm11 ;

Lm13: 2 |^ (12 + 1) = (2 |^ 12) * 2 by NEWTON:6
.= 8192 by Lm12 ;

Lm14: 2 |^ (13 + 1) = (2 |^ 13) * 2 by NEWTON:6
.= 16384 by Lm13 ;

Lm15: 2 |^ (14 + 1) = (2 |^ 14) * 2 by NEWTON:6
.= 32768 by Lm14 ;

Lm16: 2 |^ (15 + 1) = (2 |^ 15) * 2 by NEWTON:6
.= 65536 by Lm15 ;

Lm1107: 2 |^ (6 + 6) = (2 |^ 6) * (2 |^ 6)
by NEWTON:8;

Lm1108: 3 |^ 2 = 3 * 3
by WSIERP_1:1;

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

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

Lm1111: 3 |^ 5 = (((3 * 3) * 3) * 3) * 3
by NUMBER02:1;

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

Lm1113: 3 |^ 10 = ((((((((3 * 3) * 3) * 3) * 3) * 3) * 3) * 3) * 3) * 3
by NUMBER02:6;

Lm1114: 3 |^ (5 + 6) = (3 |^ 5) * (3 |^ 6)
by NEWTON:8;

((3 |^ 5) * (3 |^ 6)) + 18 = 31 * 5715
by Lm1111, Lm1112;

then Lm1115: 3 |^ 11, - 18 are_congruent_mod 31
by Lm1114;

(10 - 31) mod 31 = 10 mod 31
by AESCIP_1:5;

then Lm1116: (- 21) mod 31 = 10
by NAT_D:24;

registration

let p be Prime;

reduce 1 mod p to 1;

reducibility by NAT_D:14, INT_2:def 4;

end;

registration

let n be Nat;

reduce (<*> NAT) mod n to <*> NAT;

proof end;

reduce (<*> INT) mod n to <*> INT;

proof end;

end;

theorem Th1: :: NUMBER04:1

for X being non empty natural-membered set st ( for a being Nat st a in X holds
ex b being Nat st
( b > a & b in X ) ) holds
X is infinite

proof end;

registration

cluster EvenNAT -> infinite ;

proof end;

cluster OddNAT -> infinite ;

proof end;

end;

registration

cluster -> even for Element of EvenNAT ;

proof end;

cluster -> odd for Element of OddNAT ;

proof end;

end;

theorem :: NUMBER04:2

canceled;

::$CT

theorem Th3: :: NUMBER04:3

for a, b, c being Integer st a * b divides c holds
( a divides c & b divides c )

proof end;

theorem Th4: :: NUMBER04:4

for a, b, m being Integer holds
( not a,b are_congruent_mod m or not m divides a or m divides b )

proof end;

theorem :: NUMBER04:5

for k, n being Nat st k is odd holds
(- 1) |^ k, - 1 are_congruent_mod n by INT_1:11;

theorem Th6: :: NUMBER04:6

for k, n being Nat
for a, b being Integer st k <> 0 & a,b are_congruent_mod n |^ k holds
a,b are_congruent_mod n

proof end;

theorem Th7: :: NUMBER04:7

for n being Nat holds 2 |^ (4 * n),1 are_congruent_mod 5

proof end;

theorem Th8: :: NUMBER04:8

for n being Nat holds 2 |^ (12 * n),1 are_congruent_mod 13

proof end;

theorem Th9: :: NUMBER04:9

for n being Nat
for i being Integer holds <*i*> mod n = <*(i mod n)*>

proof end;

theorem Th10: :: NUMBER04:10

for n being Nat st n <> 0 holds
for f being integer-valued FinSequence holds Sum f, Sum (f mod n) are_congruent_mod n

proof end;

theorem :: NUMBER04:11

for a, b, c being Nat st ( a <> 0 or b <> 0 ) & c <> 0 & a,b,c are_mutually_coprime holds
a * b,c are_coprime by EULER_1:14;

theorem Th12: :: NUMBER04:12

for a, b, c, n being Nat st ( a <> 0 or b <> 0 ) & c <> 0 & a,b,c are_mutually_coprime & a divides n & b divides n & c divides n holds
(a * b) * c divides n

proof end;

theorem Th13: :: NUMBER04:13

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

proof end;

theorem Th14: :: NUMBER04:14

for n being even Nat st n divides (2 |^ n) + 2 holds
ex k being non zero odd Nat st (2 |^ n) + 2 = n * k

proof end;

theorem Th15: :: NUMBER04:15

for n being even Nat st n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 holds
for n1 being Nat st n1 = (2 |^ n) + 2 holds
( n1 - 1 divides (2 |^ n1) + 1 & n1 divides (2 |^ n1) + 2 )

proof end;

theorem Th16: :: NUMBER04:16

{ n where n is non zero even Nat : ( n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 ) } is infinite

proof end;

definition

let i be Integer;

attr i is double_odd means :: NUMBER04:def 1
ex j being odd Integer st i = 2 * j;

end;

:: deftheorem defines double_odd NUMBER04:def 1 :

definition

let i be Nat;

redefine attr i is double_odd means :: NUMBER04:def 2
ex j being odd Nat st i = 2 * j;

proof end;

end;

:: deftheorem defines double_odd NUMBER04:def 2 :

registration

cluster complex real integer ext-real double_odd for object ;

proof end;

end;

registration

cluster integer double_odd -> even for object ;

end;

registration

let i be odd Integer;

cluster (i |^ 2) + 1 -> double_odd ;

proof end;

end;

registration

let i be odd Integer;

cluster (i ^2) + 1 -> double_odd ;

proof end;

end;

definition

let r be Complex;
let n be Nat;
defpred S₁[ Nat, object ] means for m being Nat st m = n - $1 holds
( ( $1 is odd implies $2 = r |^ m ) & ( $1 is even implies $2 = - (r |^ m) ) );
defpred S₂[ complex-valued FinSequence] means ( len $1 = n & ( for i being Nat st 1 <= i & i <= n holds
S₁[i,$1 . i] ) );

func OddEvenPowers (r,n) -> complex-valued FinSequence means :Def3: :: NUMBER04:def 3
( len it = n & ( for i being Nat st 1 <= i & i <= n holds
for m being Nat st m = n - i holds
( ( i is odd implies it . i = r |^ m ) & ( i is even implies it . i = - (r |^ m) ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def3 defines OddEvenPowers NUMBER04:def 3 :

registration

let r be Real;
let n be Nat;

cluster OddEvenPowers (r,n) -> complex-valued real-valued ;

proof end;

end;

registration

let r be Integer;
let n be Nat;

cluster OddEvenPowers (r,n) -> INT -valued complex-valued ;

proof end;

end;

theorem Th17: :: NUMBER04:17

for r being Complex holds OddEvenPowers (r,1) = <*1*>

proof end;

theorem Th18: :: NUMBER04:18

for r being Complex holds Sum (OddEvenPowers (r,1)) = 1

proof end;

theorem Th19: :: NUMBER04:19

for k being Nat
for r being Complex holds OddEvenPowers (r,((2 * (k + 1)) + 1)) = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ^ (OddEvenPowers (r,((2 * k) + 1)))

proof end;

theorem Th20: :: NUMBER04:20

for k being Nat
for r being Real holds Sum (OddEvenPowers (r,((2 * k) + 3))) = ((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1))))

proof end;

theorem Th21: :: NUMBER04:21

for n being Nat
for r being Real holds (r |^ ((2 * n) + 1)) + 1 = (r + 1) * (Sum (OddEvenPowers (r,((2 * n) + 1))))

proof end;

theorem Th22: :: NUMBER04:22

for a, k being Nat
for p being odd Prime st p |^ (k + 1) divides (a |^ (p |^ k)) + 1 holds
p |^ (k + 2) divides (a |^ (p |^ (k + 1))) + 1

proof end;

theorem Th23: :: NUMBER04:23

for a, k being Nat
for p being odd Prime st p divides a + 1 holds
( p |^ (k + 1) divides (a |^ (p |^ k)) + 1 & p |^ k divides (a |^ (p |^ k)) + 1 )

proof end;

Lm1117: for a being Nat st ( for i being Nat holds not a + 1 = 2 |^ i ) holds
{ n where n is Nat : n divides (a |^ n) + 1 } is infinite

proof end;

theorem Th24: :: NUMBER04:24

for a being odd Nat st a > 1 holds
for s being Nat st s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 holds
( (a |^ s) + 1 > s & (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 )

proof end;

:: Problem 17

theorem :: NUMBER04:25

for a being Nat st a > 1 holds
{ n where n is Nat : n divides (a |^ n) + 1 } is infinite

proof end;

:: Problem 18

theorem :: NUMBER04:26

{ n where n is Nat : n divides (2 |^ n) + 2 } is infinite

proof end;

:: Problem 26 a

theorem :: NUMBER04:27

{ n where n is Nat : 5 divides (2 |^ n) - 3 } is infinite

proof end;

:: Problem 26 b

theorem :: NUMBER04:28

{ n where n is Nat : 13 divides (2 |^ n) - 3 } is infinite

proof end;

64, - 1 are_congruent_mod 65
;

then Lm1118: (2 |^ 6) * (2 |^ 6),(- 1) * (- 1) are_congruent_mod 65
by Lm6, INT_1:18;

theorem :: NUMBER04:29

for n being Nat holds 2 |^ (n + 12),2 |^ n are_congruent_mod 65

proof end;

theorem Th30: :: NUMBER04:30

for n being Nat holds 2 |^ n,2 |^ (n mod 12) are_congruent_mod 65

proof end;

:: Problem 26 c

theorem :: NUMBER04:31

for n being Nat holds not 65 divides (2 |^ n) - 3

proof end;

theorem :: NUMBER04:32

341 is composite by XPRIMES0:341, NUMBER02:def 1;

:: Problem 27 a

theorem :: NUMBER04:33

561 is composite by XPRIMES0:561, NUMBER02:def 1;

theorem :: NUMBER04:34

645 is composite by XPRIMES0:645, NUMBER02:def 1;

:: Problem 27 b

theorem :: NUMBER04:35

1105 is composite by XPRIMES0:1105, NUMBER02:def 1;

:: Problem 28 a

theorem :: NUMBER04:36

341 divides (2 |^ 341) - 2

proof end;

Lm1119: (2 |^ 10) |^ 56 = 2 |^ (10 * 56)
by NEWTON:9;

Lm1120: (2 |^ 56) |^ 10 = 2 |^ (10 * 56)
by NEWTON:9;

Lm1121: (2 |^ 560) * (2 |^ 1) = 2 |^ (560 + 1)
by NEWTON:8;

Lm1122: (2 |^ 10) |^ 64 = 2 |^ (10 * 64)
by NEWTON:9;

Lm1123: (2 |^ 640) * (2 |^ 5) = 2 |^ (640 + 5)
by NEWTON:8;

Lm1124: (2 |^ 4) |^ 161 = 2 |^ (4 * 161)
by NEWTON:9;

Lm1125: (2 |^ 8) |^ 5 = 2 |^ (8 * 5)
by NEWTON:9;

Lm1126: (2 |^ 644) * (2 |^ 1) = 2 |^ (644 + 1)
by NEWTON:8;

Lm1127: (2 |^ 14) |^ 46 = 2 |^ (14 * 46)
by NEWTON:9;

Lm1128: (2 |^ 1104) * (2 |^ 1) = 2 |^ (1104 + 1)
by NEWTON:8;

Lm1129: (2 |^ 4) |^ 276 = 2 |^ (4 * 276)
by NEWTON:9;

Lm1130: (2 |^ 56) |^ 19 = 2 |^ (56 * 19)
by NEWTON:9;

Lm1131: (2 |^ 1064) * (2 |^ 41) = 2 |^ (1064 + 41)
by NEWTON:8;

Lm1132: (2 |^ 12) |^ 92 = 2 |^ (12 * 92)
by NEWTON:9;

Lm1133: (3 |^ 2) |^ 8 = 3 |^ (2 * 8)
by NEWTON:9;

Lm1134: (3 |^ 3) |^ 368 = 3 |^ (3 * 368)
by NEWTON:9;

Lm1135: (3 |^ 10) |^ 56 = 3 |^ (10 * 56)
by NEWTON:9;

Lm1136: (3 |^ 16) |^ 35 = 3 |^ (16 * 35)
by NEWTON:9;

Lm1137: (3 |^ 560) * (3 |^ 1) = 3 |^ (560 + 1)
by NEWTON:8;

Lm1138: (3 |^ 4) |^ 276 = 3 |^ (4 * 276)
by NEWTON:9;

Lm1139: (3 |^ 1104) * (3 |^ 1) = 3 |^ (1104 + 1)
by NEWTON:8;

Lm1140: (3 |^ 16) |^ 69 = 3 |^ (16 * 69)
by NEWTON:9;

15 = 5 * 3
;

then Lm1141: 2 |^ 4,1 are_congruent_mod 5
by Lm4;

80 = 5 * 16
;

then Lm1142: 3 |^ 4,1 are_congruent_mod 5
by Lm1110;

theorem Th37: :: NUMBER04:37

3 divides (2 |^ 561) - 2

proof end;

theorem Th38: :: NUMBER04:38

11 divides (2 |^ 561) - 2

proof end;

Lm1143: 9 |^ 8 = ((((((9 * 9) * 9) * 9) * 9) * 9) * 9) * 9 by NUMBER02:4
.= (10000 * 4304) + 6721 ;

Lm1144: (2 |^ 7) |^ 8 = 2 |^ (7 * 8)
by NEWTON:9;

119 = 17 * 7
;

then 2 |^ 7,9 are_congruent_mod 17
by Lm7;

then Lm1145: (2 |^ 7) |^ 8,9 |^ 8 are_congruent_mod 17
by GR_CY_3:34;

(10000 * 4304) + 6720 = 17 * ((100 * 25321) + 60)
;

then Lm1146: 9 |^ 8,1 are_congruent_mod 17
by Lm1143;

theorem Th39: :: NUMBER04:39

17 divides (2 |^ 561) - 2

proof end;

:: Problem 27 c

theorem :: NUMBER04:40

561 divides (2 |^ 561) - 2

proof end;

theorem Th41: :: NUMBER04:41

3 divides (2 |^ 645) - 2

proof end;

theorem Th42: :: NUMBER04:42

5 divides (2 |^ 645) - 2

proof end;

theorem Th43: :: NUMBER04:43

43 divides (2 |^ 645) - 2

proof end;

theorem :: NUMBER04:44

645 divides (2 |^ 645) - 2

proof end;

theorem Th45: :: NUMBER04:45

5 divides (2 |^ 1105) - 2

proof end;

theorem Th46: :: NUMBER04:46

13 divides (2 |^ 1105) - 2

proof end;

theorem Th47: :: NUMBER04:47

17 divides (2 |^ 1105) - 2

proof end;

:: Problem 27 d

theorem :: NUMBER04:48

1105 divides (2 |^ 1105) - 2

proof end;

LemS: for a, c, k, m, n, t2 being Nat st 2 |^ k,a are_congruent_mod n & (((a * a) * a) * a) * (2 |^ m) = (n * t2) + c holds
2 |^ ((k * 4) + m),c are_congruent_mod n

proof end;

Lem1: for a, c, k, m, n, t1, t2 being Nat st 2 |^ k = (n * t1) + a & (((a * a) * a) * a) * (2 |^ m) = (n * t2) + c holds
2 |^ ((k * 4) + m),c are_congruent_mod n

proof end;

theorem Th49: :: NUMBER04:49

for n being composite Nat st n <= 1105 & n divides (2 |^ n) - 2 holds
n in {341,561,645,1105}

proof end;

:: Problem 28 b

theorem Th50: :: NUMBER04:50

not 341 divides (3 |^ 341) - 3

proof end;

theorem Th51: :: NUMBER04:51

3 divides (3 |^ 561) - 3

proof end;

theorem Th52: :: NUMBER04:52

11 divides (3 |^ 561) - 3

proof end;

theorem Th53: :: NUMBER04:53

17 divides (3 |^ 561) - 3

proof end;

:: Problem 27 e

theorem :: NUMBER04:54

561 divides (3 |^ 561) - 3

proof end;

theorem Th55: :: NUMBER04:55

not 43 divides (3 |^ 645) - 3

proof end;

theorem Th56: :: NUMBER04:56

not 645 divides (3 |^ 645) - 3

proof end;

theorem Th57: :: NUMBER04:57

5 divides (3 |^ 1105) - 3

proof end;

theorem Th58: :: NUMBER04:58

13 divides (3 |^ 1105) - 3

proof end;

theorem Th59: :: NUMBER04:59

17 divides (3 |^ 1105) - 3

proof end;

:: Problem 27 f

theorem :: NUMBER04:60

1105 divides (3 |^ 1105) - 3

proof end;

:: Problem 27 g

theorem :: NUMBER04:61

for n being Nat st n <= 1105 & n is composite & n divides (2 |^ n) - 2 & n divides (3 |^ n) - 3 holds
n in {561,1105}

proof end;

theorem Th62: :: NUMBER04:62

for n being Nat st n divides (2 |^ n) - 2 & not n divides (3 |^ n) - 3 holds
n is composite

proof end;

:: Problem 28 c

theorem :: NUMBER04:63

for n being Nat st n <= 341 & n divides (2 |^ n) - 2 & not n divides (3 |^ n) - 3 holds
n = 341

proof end;

Lm2062: 10 |^ 4 = ((10 * 10) * 10) * 10
by POLYEQ_5:3;

theorem Th64: :: NUMBER04:64

for a, m, n being Nat st m,n are_coprime holds
(a * n) + m,n are_coprime

proof end;

theorem Th65: :: NUMBER04:65

for k being Nat holds 7 divides (10 |^ ((6 * k) + 4)) + 3

proof end;

theorem Th66: :: NUMBER04:66

for k being Nat holds (10 |^ ((6 * k) + 4)) + 3 is composite

proof end;

:: Problem 98

theorem :: NUMBER04:67

{ ((10 |^ n) + 3) where n is Nat : (10 |^ n) + 3 is composite } is infinite

proof end;