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