A1:
(2 |^ 1) mod 4001 = 2
by NAT_D:24;
A2: (2 |^ 2) mod 4001 =
(2 |^ (2 * 1)) mod 4001
.=
(2 * 2) mod 4001
by A1, Th11
.=
4
by NAT_D:24
;
A3: (2 |^ 4) mod 4001 =
(2 |^ (2 * 2)) mod 4001
.=
(4 * 4) mod 4001
by A2, Th11
.=
16
by NAT_D:24
;
A4: (2 |^ 8) mod 4001 =
(2 |^ (2 * 4)) mod 4001
.=
(16 * 16) mod 4001
by A3, Th11
.=
256
by NAT_D:24
;
A5:
4001 - 1 = ((5 * 5) * 5) * 32
;
256 * 256 = (4001 * 16) + 1520
;
then A6:
(256 * 256) mod 4001 = 1520
by NAT_D:def 2;
A7: (5 * 5) * 5 =
((5 |^ 1) * 5) * 5
.=
(5 |^ (1 + 1)) * 5
by NEWTON:6
.=
5 |^ ((1 + 1) + 1)
by NEWTON:6
.=
5 |^ 3
;
1023 * 1023 = (4001 * 261) + 2268
;
then A8:
(1023 * 1023) mod 4001 = 2268
by NAT_D:def 2;
A9:
(2 |^ 800) -' 1 = (2 |^ 800) - 1
by PREPOWER:11, XREAL_1:233;
A10:
6311 = (4001 * 1) + 2310
;
A11:
3906 * 1913 = (4001 * 1867) + 2311
;
A12:
1522 * 1823 = (4001 * 693) + 1913
;
3441 * 3441 = (4001 * 2959) + 1522
;
then A13:
(3441 * 3441) mod 4001 = 1522
by NAT_D:def 2;
A14:
1023 * 2164 = (4001 * 553) + 1219
;
2499 * 2499 = (4001 * 1560) + 3441
;
then A15:
(2499 * 2499) mod 4001 = 3441
by NAT_D:def 2;
A16:
3906 * 988 = (4001 * 964) + 2164
;
1823 * 1823 = (4001 * 830) + 2499
;
then A17:
(1823 * 1823) mod 4001 = 2499
by NAT_D:def 2;
A18:
1522 * 3376 = (4001 * 1284) + 988
;
1520 * 1520 = (4001 * 577) + 1823
;
then A19:
(1520 * 1520) mod 4001 = 1823
by NAT_D:def 2;
A20:
3441 * 1823 = (4001 * 1567) + 3376
;
1522 * 1522 = (4001 * 578) + 3906
;
then A21:
(1522 * 1522) mod 4001 = 3906
by NAT_D:def 2;
A22:
2268 * 1219 = (4001 * 691) + 1
;
3906 * 3906 = (4001 * 3813) + 1023
;
then A23:
(3906 * 3906) mod 4001 = 1023
by NAT_D:def 2;
A24: 4001 -' 1 =
4001 - 1
by XREAL_1:233
.=
4000
;
A25: (2 |^ 16) mod 4001 =
(2 |^ (2 * 8)) mod 4001
.=
1520
by A4, A6, Th11
;
A26: (2 |^ 32) mod 4001 =
(2 |^ (2 * 16)) mod 4001
.=
1823
by A25, A19, Th11
;
A27: (2 |^ 64) mod 4001 =
(2 |^ (2 * 32)) mod 4001
.=
2499
by A26, A17, Th11
;
A28: (2 |^ 128) mod 4001 =
(2 |^ (2 * 64)) mod 4001
.=
3441
by A27, A15, Th11
;
A29: (2 |^ 256) mod 4001 =
(2 |^ (2 * 128)) mod 4001
.=
1522
by A28, A13, Th11
;
A30: (2 |^ 512) mod 4001 =
(2 |^ (2 * 256)) mod 4001
.=
3906
by A29, A21, Th11
;
A31: (2 |^ 1024) mod 4001 =
(2 |^ (2 * 512)) mod 4001
.=
1023
by A30, A23, Th11
;
A32: (2 |^ 800) mod 4001 =
(2 |^ (512 + 288)) mod 4001
.=
((2 |^ 512) * (2 |^ 288)) mod 4001
by NEWTON:8
.=
(3906 * ((2 |^ (256 + 32)) mod 4001)) mod 4001
by A30, EULER_2:9
.=
(3906 * (((2 |^ 256) * (2 |^ 32)) mod 4001)) mod 4001
by NEWTON:8
.=
(3906 * ((1522 * 1823) mod 4001)) mod 4001
by A26, A29, EULER_2:9
.=
(3906 * 1913) mod 4001
by A12, NAT_D:def 2
.=
2311
by A11, NAT_D:def 2
;
4000 = (5 * 800) + 0
;
then A33: ((2 |^ ((4001 -' 1) div 5)) -' 1) gcd 4001 =
((2 |^ 800) -' 1) gcd 4001
by A24, NAT_D:def 1
.=
(((2 |^ 800) -' 1) + (4001 * 1)) gcd 4001
by EULER_1:8
.=
4001 gcd (((2 |^ 800) + 4000) mod 4001)
by A9, NAT_D:28
.=
4001 gcd ((2311 + (4000 mod 4001)) mod 4001)
by A32, EULER_2:6
.=
4001 gcd ((2311 + 4000) mod 4001)
by NAT_D:24
.=
((2310 * 1) + 1691) gcd 2310
by A10, NAT_D:def 2
.=
1691 gcd ((1691 * 1) + 619)
by EULER_1:8
.=
((619 * 2) + 453) gcd 619
by EULER_1:8
.=
((453 * 1) + 166) gcd 453
by EULER_1:8
.=
166 gcd ((166 * 2) + 121)
by EULER_1:8
.=
((121 * 1) + 45) gcd 121
by EULER_1:8
.=
45 gcd ((45 * 2) + 31)
by EULER_1:8
.=
((31 * 1) + 14) gcd 31
by EULER_1:8
.=
14 gcd ((14 * 2) + 3)
by EULER_1:8
.=
((3 * 4) + 2) gcd 3
by EULER_1:8
.=
2 gcd ((2 * 1) + 1)
by EULER_1:8
.=
2 gcd 1
by EULER_1:8
.=
1
by NEWTON:51
;
A34: (2 |^ 2048) mod 4001 =
(2 |^ (2 * 1024)) mod 4001
.=
2268
by A31, A8, Th11
;
(2 |^ (4001 -' 1)) mod 4001 =
(2 |^ (2048 + 1952)) mod 4001
by A24
.=
((2 |^ 2048) * (2 |^ 1952)) mod 4001
by NEWTON:8
.=
(((2 |^ 2048) mod 4001) * ((2 |^ (1024 + 928)) mod 4001)) mod 4001
by EULER_2:9
.=
(2268 * (((2 |^ 1024) * (2 |^ 928)) mod 4001)) mod 4001
by A34, NEWTON:8
.=
(2268 * ((1023 * ((2 |^ (512 + 416)) mod 4001)) mod 4001)) mod 4001
by A31, EULER_2:9
.=
(2268 * ((1023 * (((2 |^ 512) * (2 |^ 416)) mod 4001)) mod 4001)) mod 4001
by NEWTON:8
.=
(2268 * ((1023 * ((3906 * ((2 |^ (256 + 160)) mod 4001)) mod 4001)) mod 4001)) mod 4001
by A30, EULER_2:9
.=
(2268 * ((1023 * ((3906 * (((2 |^ 256) * (2 |^ 160)) mod 4001)) mod 4001)) mod 4001)) mod 4001
by NEWTON:8
.=
(2268 * ((1023 * ((3906 * ((1522 * ((2 |^ (128 + 32)) mod 4001)) mod 4001)) mod 4001)) mod 4001)) mod 4001
by A29, EULER_2:9
.=
(2268 * ((1023 * ((3906 * ((1522 * (((2 |^ 128) * (2 |^ 32)) mod 4001)) mod 4001)) mod 4001)) mod 4001)) mod 4001
by NEWTON:8
.=
(2268 * ((1023 * ((3906 * ((1522 * ((3441 * 1823) mod 4001)) mod 4001)) mod 4001)) mod 4001)) mod 4001
by A26, A28, EULER_2:9
.=
(2268 * ((1023 * ((3906 * ((1522 * 3376) mod 4001)) mod 4001)) mod 4001)) mod 4001
by A20, NAT_D:def 2
.=
(2268 * ((1023 * ((3906 * 988) mod 4001)) mod 4001)) mod 4001
by A18, NAT_D:def 2
.=
(2268 * ((1023 * 2164) mod 4001)) mod 4001
by A16, NAT_D:def 2
.=
(2268 * 1219) mod 4001
by A14, NAT_D:def 2
.=
1
by A22, NAT_D:def 2
;
hence
4001 is prime
by A5, A7, A33, Th25, PEPIN:59; verum