641 = (2 * 320) + 1 ;
then reconsider n = 641 as natural odd number ;
A1: 256 + 64 = 320 ;
A2: 3 * 3 = (3 |^ 1) * 3
.= (3 |^ 1) * (3 |^ 1)
.= 3 |^ (1 + 1) by NEWTON:8 ;
A3: (3 |^ 2) * (3 |^ 2) = 3 |^ (2 + 2) by NEWTON:8;
A4: (3 |^ 4) * (3 |^ 4) = 3 |^ (4 + 4) by NEWTON:8;
6561 = (10 * 641) + 151 ;
then 3 |^ 8,151 are_congruent_mod 641 by A4, A3, A2;
then (3 |^ 8) * (3 |^ 8),151 * 151 are_congruent_mod 641 by INT_1:18;
then A5: 3 |^ (8 + 8),22801 are_congruent_mod 641 by NEWTON:8;
22801 = (35 * 641) + 366 ;
then 22801,366 are_congruent_mod 641 ;
then 3 |^ 16,366 are_congruent_mod 641 by A5, INT_1:15;
then A6: (3 |^ 16) * (3 |^ 16),366 * 366 are_congruent_mod 641 by INT_1:18;
A7: 183,183 are_congruent_mod 641 by INT_1:11;
732,91 are_congruent_mod 641 ;
then 732 * 183,91 * 183 are_congruent_mod 641 by A7, INT_1:18;
then (3 |^ 16) * (3 |^ 16),91 * 183 are_congruent_mod 641 by A6, INT_1:15;
then A8: 3 |^ (16 + 16),91 * 183 are_congruent_mod 641 by NEWTON:8;
16653 = (26 * 641) + (- 13) ;
then 16653, - 13 are_congruent_mod 641 ;
then 3 |^ 32, - 13 are_congruent_mod 641 by A8, INT_1:15;
then (3 |^ 32) * (3 |^ 32),(- 13) * (- 13) are_congruent_mod 641 by INT_1:18;
then A9: 3 |^ (32 + 32),169 are_congruent_mod 641 by NEWTON:8;
then A10: (3 |^ 64) * (3 |^ 64),169 * 169 are_congruent_mod 641 by INT_1:18;
28561 = (44 * 641) + 357 ;
then 28561,357 are_congruent_mod 641 ;
then (3 |^ 64) * (3 |^ 64),357 are_congruent_mod 641 by A10, INT_1:15;
then 3 |^ (64 + 64),357 are_congruent_mod 641 by NEWTON:8;
then A11: (3 |^ 128) * (3 |^ 128),357 * 357 are_congruent_mod 641 by INT_1:18;
A12: 119,119 are_congruent_mod 641 by INT_1:11;
1071,430 are_congruent_mod 641 ;
then 1071 * 119,430 * 119 are_congruent_mod 641 by A12, INT_1:18;
then (3 |^ 128) * (3 |^ 128),430 * 119 are_congruent_mod 641 by A11, INT_1:15;
then A13: 3 |^ (128 + 128),3010 * 17 are_congruent_mod 641 by NEWTON:8;
A14: 17,17 are_congruent_mod 641 by INT_1:11;
3010 = (4 * 641) + 446 ;
then 3010,446 are_congruent_mod 641 ;
then 3010 * 17,446 * 17 are_congruent_mod 641 by A14, INT_1:18;
then A15: 3 |^ (128 + 128),446 * 17 are_congruent_mod 641 by A13, INT_1:15;
7582 = (12 * 641) + (- 110) ;
then 7582, - 110 are_congruent_mod 641 ;
then 3 |^ 256, - 110 are_congruent_mod 641 by A15, INT_1:15;
then (3 |^ 256) * (3 |^ 64),(- 110) * 169 are_congruent_mod 641 by A9, INT_1:18;
then A16: 3 |^ 320, - 18590 are_congruent_mod 641 by A1, NEWTON:8;
A17: - 18590 = ((- 30) * 641) + 640 ;
A18: 640, - 1 are_congruent_mod 641 ;
- 18590,640 are_congruent_mod 641 by A17;
then - 18590, - 1 are_congruent_mod 641 by A18, INT_1:15;
then ex a being natural number st a |^ ((n - 1) / 2), - 1 are_congruent_mod n by A16, INT_1:15;
hence 641 is prime by Th40, Th37; :: thesis: verum