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