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, EULER_2:9
.=
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, EULER_2:6
.=
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 EULER_2:9
.=
(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, EULER_2:9
.=
(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, EULER_2:9
.=
(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, EULER_2:9
.=
(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, EULER_2:9
.=
(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; verum