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, NAT_D:67
.= 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, NAT_D:66
.= 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 NAT_D:67
.= (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, NAT_D:67
.= (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, NAT_D:67
.= (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, NAT_D:67
.= (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, NAT_D:67
.= (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; :: thesis: verum