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