1038 * 1038 = (1259 * 855) + 999
;
then A1:
(1038 * 1038) mod 1259 = 999
by NAT_D:def 2;
A2:
999 * 744 = (1259 * 590) + 446
;
847 * 847 = (1259 * 569) + 1038
;
then A3:
(847 * 847) mod 1259 = 1038
by NAT_D:def 2;
A4:
1038 * 1136 = (1259 * 936) + 744
;
999 * 999 = (1259 * 792) + 873
;
then A5:
(999 * 999) mod 1259 = 873
by NAT_D:def 2;
A6:
765 * 446 = (1259 * 271) + 1
;
A7:
2128 = (1259 * 1) + 869
;
A8:
847 * 4 = (1259 * 2) + 870
;
434 * 434 = (1259 * 149) + 765
;
then A9:
(434 * 434) mod 1259 = 765
by NAT_D:def 2;
A10:
(2 |^ 34) -' 1 = (2 |^ 34) - 1
by PREPOWER:11, XREAL_1:233;
873 * 873 = (1259 * 605) + 434
;
then A11:
(873 * 873) mod 1259 = 434
by NAT_D:def 2;
A12: 1259 -' 1 =
1259 - 1
by XREAL_1:233
.=
1258
;
68 * 68 = (1259 * 3) + 847
;
then A13:
(68 * 68) mod 1259 = 847
by NAT_D:def 2;
A14:
847 * 1024 = (1259 * 688) + 1136
;
256 * 256 = (1259 * 52) + 68
;
then A15:
(256 * 256) mod 1259 = 68
by NAT_D:def 2;
A16:
( 1259 - 1 = 37 * 34 & 37 = 37 |^ 1 )
;
A17:
(2 |^ 1) mod 1259 = 2
by NAT_D:24;
A18: (2 |^ 2) mod 1259 =
(2 |^ (2 * 1)) mod 1259
.=
(2 * 2) mod 1259
by A17, Th11
.=
4
by NAT_D:24
;
A19: (2 |^ 4) mod 1259 =
(2 |^ (2 * 2)) mod 1259
.=
(4 * 4) mod 1259
by A18, Th11
.=
16
by NAT_D:24
;
A20: (2 |^ 8) mod 1259 =
(2 |^ (2 * 4)) mod 1259
.=
(16 * 16) mod 1259
by A19, Th11
.=
256
by NAT_D:24
;
A21: (2 |^ 16) mod 1259 =
(2 |^ (2 * 8)) mod 1259
.=
68
by A20, A15, Th11
;
A22: (2 |^ 32) mod 1259 =
(2 |^ (2 * 16)) mod 1259
.=
847
by A21, A13, Th11
;
A23: (2 |^ 34) mod 1259 =
(2 |^ (32 + 2)) mod 1259
.=
((2 |^ 32) * (2 |^ 2)) mod 1259
by NEWTON:8
.=
(847 * 4) mod 1259
by A18, A22, EULER_2:9
.=
870
by A8, NAT_D:def 2
;
A24: (2 |^ 64) mod 1259 =
(2 |^ (2 * 32)) mod 1259
.=
1038
by A22, A3, Th11
;
1258 = (37 * 34) + 0
;
then A25: ((2 |^ ((1259 -' 1) div 37)) -' 1) gcd 1259 =
((2 |^ 34) -' 1) gcd 1259
by A12, NAT_D:def 1
.=
(((2 |^ 34) -' 1) + (1259 * 1)) gcd 1259
by EULER_1:8
.=
1259 gcd (((2 |^ 34) + 1258) mod 1259)
by A10, NAT_D:28
.=
1259 gcd ((870 + (1258 mod 1259)) mod 1259)
by A23, EULER_2:6
.=
1259 gcd ((870 + 1258) mod 1259)
by NAT_D:24
.=
((869 * 1) + 390) gcd 869
by A7, NAT_D:def 2
.=
390 gcd ((390 * 2) + 89)
by EULER_1:8
.=
((89 * 4) + 34) gcd 89
by EULER_1:8
.=
34 gcd ((34 * 2) + 21)
by EULER_1:8
.=
((21 * 1) + 13) gcd 21
by EULER_1:8
.=
13 gcd ((13 * 1) + 8)
by EULER_1:8
.=
((8 * 1) + 5) gcd 8
by EULER_1:8
.=
5 gcd ((5 * 1) + 3)
by EULER_1:8
.=
((3 * 1) + 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
;
A26: (2 |^ 128) mod 1259 =
(2 |^ (2 * 64)) mod 1259
.=
999
by A24, A1, Th11
;
A27: (2 |^ 256) mod 1259 =
(2 |^ (2 * 128)) mod 1259
.=
873
by A26, A5, Th11
;
A28: (2 |^ 512) mod 1259 =
(2 |^ (2 * 256)) mod 1259
.=
434
by A27, A11, Th11
;
A29: (2 |^ 1024) mod 1259 =
(2 |^ (2 * 512)) mod 1259
.=
765
by A28, A9, Th11
;
(2 |^ (1259 -' 1)) mod 1259 =
(2 |^ (1024 + 234)) mod 1259
by A12
.=
((2 |^ 1024) * (2 |^ 234)) mod 1259
by NEWTON:8
.=
(((2 |^ 1024) mod 1259) * ((2 |^ (128 + 106)) mod 1259)) mod 1259
by EULER_2:9
.=
(765 * (((2 |^ 128) * (2 |^ 106)) mod 1259)) mod 1259
by A29, NEWTON:8
.=
(765 * ((999 * ((2 |^ (64 + 42)) mod 1259)) mod 1259)) mod 1259
by A26, EULER_2:9
.=
(765 * ((999 * (((2 |^ 64) * (2 |^ 42)) mod 1259)) mod 1259)) mod 1259
by NEWTON:8
.=
(765 * ((999 * ((1038 * ((2 |^ (32 + 10)) mod 1259)) mod 1259)) mod 1259)) mod 1259
by A24, EULER_2:9
.=
(765 * ((999 * ((1038 * (((2 |^ 32) * (2 |^ 10)) mod 1259)) mod 1259)) mod 1259)) mod 1259
by NEWTON:8
.=
(765 * ((999 * ((1038 * ((847 * ((2 |^ (8 + 2)) mod 1259)) mod 1259)) mod 1259)) mod 1259)) mod 1259
by A22, EULER_2:9
.=
(765 * ((999 * ((1038 * ((847 * (((2 |^ 8) * (2 |^ 2)) mod 1259)) mod 1259)) mod 1259)) mod 1259)) mod 1259
by NEWTON:8
.=
(765 * ((999 * ((1038 * ((847 * ((256 * 4) mod 1259)) mod 1259)) mod 1259)) mod 1259)) mod 1259
by A18, A20, EULER_2:9
.=
(765 * ((999 * ((1038 * ((847 * 1024) mod 1259)) mod 1259)) mod 1259)) mod 1259
by NAT_D:24
.=
(765 * ((999 * ((1038 * 1136) mod 1259)) mod 1259)) mod 1259
by A14, NAT_D:def 2
.=
(765 * ((999 * 744) mod 1259)) mod 1259
by A4, NAT_D:def 2
.=
(765 * 446) mod 1259
by A2, NAT_D:def 2
.=
1
by A6, NAT_D:def 2
;
hence
1259 is prime
by A16, A25, Th25, Th31; verum