A1: 2503 - 1 = 139 * 18 ;
A2: 139 = 139 |^ 1 by NEWTON:10;
A3: 139 gcd 18 = (13 + (18 * 7)) gcd 18
.= 13 gcd ((13 * 1) + 5) by EULER_1:9
.= (3 + (2 * 5)) gcd 5 by EULER_1:9
.= 3 gcd (2 + (3 * 1)) by EULER_1:9
.= (1 + (2 * 1)) 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 2503 = 2 by NAT_D:24;
A5: (2 |^ 2) mod 2503 = (2 |^ (2 * 1)) mod 2503
.= (2 * 2) mod 2503 by A4, Th11
.= 4 by NAT_D:24 ;
A6: (2 |^ 4) mod 2503 = (2 |^ (2 * 2)) mod 2503
.= (4 * 4) mod 2503 by A5, Th11
.= 16 by NAT_D:24 ;
A7: (2 |^ 8) mod 2503 = (2 |^ (2 * 4)) mod 2503
.= (16 * 16) mod 2503 by A6, Th11
.= 256 by NAT_D:24 ;
256 * 256 = (2503 * 26) + 458 ;
then A8: (256 * 256) mod 2503 = 458 by NAT_D:def 2;
A9: (2 |^ 16) mod 2503 = (2 |^ (2 * 8)) mod 2503
.= 458 by A7, A8, Th11 ;
458 * 458 = (2503 * 83) + 2015 ;
then A10: (458 * 458) mod 2503 = 2015 by NAT_D:def 2;
A11: (2 |^ 32) mod 2503 = (2 |^ (2 * 16)) mod 2503
.= 2015 by A9, A10, Th11 ;
2015 * 2015 = (2503 * 1622) + 359 ;
then A12: (2015 * 2015) mod 2503 = 359 by NAT_D:def 2;
A13: (2 |^ 64) mod 2503 = (2 |^ (2 * 32)) mod 2503
.= 359 by A11, A12, Th11 ;
359 * 359 = (2503 * 51) + 1228 ;
then A14: (359 * 359) mod 2503 = 1228 by NAT_D:def 2;
A15: (2 |^ 128) mod 2503 = (2 |^ (2 * 64)) mod 2503
.= 1228 by A13, A14, Th11 ;
1228 * 1228 = (2503 * 602) + 1178 ;
then A16: (1228 * 1228) mod 2503 = 1178 by NAT_D:def 2;
A17: (2 |^ 256) mod 2503 = (2 |^ (2 * 128)) mod 2503
.= 1178 by A15, A16, Th11 ;
1178 * 1178 = (2503 * 554) + 1022 ;
then A18: (1178 * 1178) mod 2503 = 1022 by NAT_D:def 2;
A19: (2 |^ 512) mod 2503 = (2 |^ (2 * 256)) mod 2503
.= 1022 by A17, A18, Th11 ;
1022 * 1022 = (2503 * 417) + 733 ;
then A20: (1022 * 1022) mod 2503 = 733 by NAT_D:def 2;
A21: (2 |^ 1024) mod 2503 = (2 |^ (2 * 512)) mod 2503
.= 733 by A19, A20, Th11 ;
733 * 733 = (2503 * 214) + 1647 ;
then A22: (733 * 733) mod 2503 = 1647 by NAT_D:def 2;
A23: (2 |^ 2048) mod 2503 = (2 |^ (2 * 1024)) mod 2503
.= 1647 by A21, A22, Th11 ;
A24: 359 * 64 = (2503 * 9) + 449 ;
A25: 1228 * 449 = (2503 * 220) + 712 ;
A26: 1178 * 712 = (2503 * 335) + 231 ;
A27: 1647 * 231 = (2503 * 152) + 1 ;
A28: 2503 -' 1 = 2503 - 1 by XREAL_1:235
.= 2502 ;
then A29: (2 |^ (2503 -' 1)) mod 2503 = (2 |^ (2048 + 454)) mod 2503
.= ((2 |^ 2048) * (2 |^ 454)) mod 2503 by NEWTON:13
.= (((2 |^ 2048) mod 2503) * ((2 |^ (256 + 198)) mod 2503)) mod 2503 by EULER_2:11
.= (1647 * (((2 |^ 256) * (2 |^ 198)) mod 2503)) mod 2503 by A23, NEWTON:13
.= (1647 * ((1178 * ((2 |^ (128 + 70)) mod 2503)) mod 2503)) mod 2503 by A17, EULER_2:11
.= (1647 * ((1178 * (((2 |^ 128) * (2 |^ 70)) mod 2503)) mod 2503)) mod 2503 by NEWTON:13
.= (1647 * ((1178 * ((1228 * ((2 |^ (64 + 6)) mod 2503)) mod 2503)) mod 2503)) mod 2503 by A15, EULER_2:11
.= (1647 * ((1178 * ((1228 * (((2 |^ 64) * (2 |^ 6)) mod 2503)) mod 2503)) mod 2503)) mod 2503 by NEWTON:13
.= (1647 * ((1178 * ((1228 * ((359 * ((2 |^ (4 + 2)) mod 2503)) mod 2503)) mod 2503)) mod 2503)) mod 2503 by A13, EULER_2:11
.= (1647 * ((1178 * ((1228 * ((359 * (((2 |^ 4) * (2 |^ 2)) mod 2503)) mod 2503)) mod 2503)) mod 2503)) mod 2503 by NEWTON:13
.= (1647 * ((1178 * ((1228 * ((359 * ((16 * 4) mod 2503)) mod 2503)) mod 2503)) mod 2503)) mod 2503 by A5, A6, EULER_2:11
.= (1647 * ((1178 * ((1228 * ((359 * 64) mod 2503)) mod 2503)) mod 2503)) mod 2503 by NAT_D:24
.= (1647 * ((1178 * ((1228 * 449) mod 2503)) mod 2503)) mod 2503 by A24, NAT_D:def 2
.= (1647 * ((1178 * 712) mod 2503)) mod 2503 by A25, NAT_D:def 2
.= (1647 * 231) mod 2503 by A26, NAT_D:def 2
.= 1 by A27, NAT_D:def 2 ;
A30: 2502 = (139 * 18) + 0 ;
A31: (2 |^ 18) -' 1 = (2 |^ 18) - 1 by PREPOWER:19, XREAL_1:235;
A32: (2 |^ 18) mod 2503 = (2 |^ (16 + 2)) mod 2503
.= ((2 |^ 16) * (2 |^ 2)) mod 2503 by NEWTON:13
.= (458 * 4) mod 2503 by A5, A9, EULER_2:11
.= 1832 by NAT_D:24 ;
A33: 4334 = (2503 * 1) + 1831 ;
((2 |^ ((2503 -' 1) div 139)) -' 1) gcd 2503 = ((2 |^ 18) -' 1) gcd 2503 by A28, A30, NAT_D:def 1
.= (((2 |^ 18) -' 1) + (2503 * 1)) gcd 2503 by EULER_1:9
.= 2503 gcd (((2 |^ 18) + 2502) mod 2503) by A31, NAT_D:28
.= 2503 gcd ((1832 + (2502 mod 2503)) mod 2503) by A32, EULER_2:8
.= 2503 gcd ((1832 + 2502) mod 2503) by NAT_D:24
.= ((1831 * 1) + 672) gcd 1831 by A33, NAT_D:def 2
.= 672 gcd ((672 * 2) + 487) by EULER_1:9
.= ((487 * 1) + 185) gcd 487 by EULER_1:9
.= 185 gcd ((185 * 2) + 117) by EULER_1:9
.= ((117 * 1) + 68) gcd 117 by EULER_1:9
.= 68 gcd ((68 * 1) + 49) by EULER_1:9
.= ((49 * 1) + 19) gcd 49 by EULER_1:9
.= 19 gcd ((19 * 2) + 11) by EULER_1:9
.= ((11 * 1) + 8) gcd 11 by EULER_1:9
.= 8 gcd ((8 * 1) + 3) by EULER_1:9
.= ((3 * 2) + 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 2503 is prime by A1, A2, A3, A29, Th25, Th34; :: thesis: verum