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, NAT_D:67
.= (3906 * (((2 |^ 256) * (2 |^ 32)) mod 4001)) mod 4001 by NEWTON:8
.= (3906 * ((1522 * 1823) mod 4001)) mod 4001 by A26, A29, NAT_D:67
.= (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, NAT_D:66
.= 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 NAT_D:67
.= (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, NAT_D:67
.= (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, NAT_D:67
.= (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, NAT_D:67
.= (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, NAT_D:67
.= (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; :: thesis: verum