set N = 6700417;
set a = 5;
A1: 5 |^ 1,5 are_congruent_mod 6700417 by INT_1:11;
A2: 5 |^ 2,25 are_congruent_mod 6700417

proof

5 * 5 = (0 * 6700417) + 25 ;
then 5 |^ (1 + 1),25 are_congruent_mod 6700417 by A1, LemSq;
hence 5 |^ 2,25 are_congruent_mod 6700417 ; :: thesis: verum

end;

A3: 5 |^ 4,625 are_congruent_mod 6700417

proof

25 * 25 = (0 * 6700417) + 625 ;
then 5 |^ (2 + 2),625 are_congruent_mod 6700417 by A2, LemSq;
hence 5 |^ 4,625 are_congruent_mod 6700417 ; :: thesis: verum

end;

A4: 5 |^ 8,390625 are_congruent_mod 6700417

proof

625 * 625 = (0 * 6700417) + 390625 ;
then 5 |^ (4 + 4),390625 are_congruent_mod 6700417 by A3, LemSq;
hence 5 |^ 8,390625 are_congruent_mod 6700417 ; :: thesis: verum

end;

A5: 5 |^ 16,5994701 are_congruent_mod 6700417

proof

390625 * 390625 = (22772 * 6700417) + 5994701 ;
then 5 |^ (8 + 8),5994701 are_congruent_mod 6700417 by A4, LemSq;
hence 5 |^ 16,5994701 are_congruent_mod 6700417 ; :: thesis: verum

end;

A6: 5 |^ 32,6477880 are_congruent_mod 6700417

proof

5994701 * 5994701 = (5363313 * 6700417) + 6477880 ;
then 5 |^ (16 + 16),6477880 are_congruent_mod 6700417 by A5, LemSq;
hence 5 |^ 32,6477880 are_congruent_mod 6700417 ; :: thesis: verum

end;

A7: 5 |^ 64,6634739 are_congruent_mod 6700417

proof

6477880 * 6477880 = (6262733 * 6700417) + 6634739 ;
then 5 |^ (32 + 32),6634739 are_congruent_mod 6700417 by A6, LemSq;
hence 5 |^ 64,6634739 are_congruent_mod 6700417 ; :: thesis: verum

end;

A8: 5 |^ 128,5231553 are_congruent_mod 6700417

proof

6634739 * 6634739 = (6569704 * 6700417) + 5231553 ;
then 5 |^ (64 + 64),5231553 are_congruent_mod 6700417 by A7, LemSq;
hence 5 |^ 128,5231553 are_congruent_mod 6700417 ; :: thesis: verum

end;

A9: 5 |^ 256,374828 are_congruent_mod 6700417

proof

5231553 * 5231553 = (4084693 * 6700417) + 374828 ;
then 5 |^ (128 + 128),374828 are_congruent_mod 6700417 by A8, LemSq;
hence 5 |^ 256,374828 are_congruent_mod 6700417 ; :: thesis: verum

end;

A10: 5 |^ 512,1685928 are_congruent_mod 6700417

proof

374828 * 374828 = (20968 * 6700417) + 1685928 ;
then 5 |^ (256 + 256),1685928 are_congruent_mod 6700417 by A9, LemSq;
hence 5 |^ 512,1685928 are_congruent_mod 6700417 ; :: thesis: verum

end;

A11: 5 |^ 1024,2827699 are_congruent_mod 6700417

proof

1685928 * 1685928 = (424205 * 6700417) + 2827699 ;
then 5 |^ (512 + 512),2827699 are_congruent_mod 6700417 by A10, LemSq;
hence 5 |^ 1024,2827699 are_congruent_mod 6700417 ; :: thesis: verum

end;

A12: 5 |^ 2048,6011821 are_congruent_mod 6700417

proof

2827699 * 2827699 = (1193340 * 6700417) + 6011821 ;
then 5 |^ (1024 + 1024),6011821 are_congruent_mod 6700417 by A11, LemSq;
hence 5 |^ 2048,6011821 are_congruent_mod 6700417 ; :: thesis: verum

end;

A13: 5 |^ 4096,2741794 are_congruent_mod 6700417

proof

6011821 * 6011821 = (5393991 * 6700417) + 2741794 ;
then 5 |^ (2048 + 2048),2741794 are_congruent_mod 6700417 by A12, LemSq;
hence 5 |^ 4096,2741794 are_congruent_mod 6700417 ; :: thesis: verum

end;

A14: 5 |^ 8192,1991541 are_congruent_mod 6700417

proof

2741794 * 2741794 = (1121935 * 6700417) + 1991541 ;
then 5 |^ (4096 + 4096),1991541 are_congruent_mod 6700417 by A13, LemSq;
hence 5 |^ 8192,1991541 are_congruent_mod 6700417 ; :: thesis: verum

end;

A15: 5 |^ 16384,4116535 are_congruent_mod 6700417

proof

1991541 * 1991541 = (591938 * 6700417) + 4116535 ;
then 5 |^ (8192 + 8192),4116535 are_congruent_mod 6700417 by A14, LemSq;
hence 5 |^ 16384,4116535 are_congruent_mod 6700417 ; :: thesis: verum

end;

A16: 5 |^ 32768,3281950 are_congruent_mod 6700417

proof

4116535 * 4116535 = (2529075 * 6700417) + 3281950 ;
then 5 |^ (16384 + 16384),3281950 are_congruent_mod 6700417 by A15, LemSq;
hence 5 |^ 32768,3281950 are_congruent_mod 6700417 ; :: thesis: verum

end;

A17: 5 |^ 65536,757903 are_congruent_mod 6700417

proof

3281950 * 3281950 = (1607541 * 6700417) + 757903 ;
then 5 |^ (32768 + 32768),757903 are_congruent_mod 6700417 by A16, LemSq;
hence 5 |^ 65536,757903 are_congruent_mod 6700417 ; :: thesis: verum

end;

A18: 5 |^ 131072,3608833 are_congruent_mod 6700417

proof

757903 * 757903 = (85728 * 6700417) + 3608833 ;
then 5 |^ (65536 + 65536),3608833 are_congruent_mod 6700417 by A17, LemSq;
hence 5 |^ 131072,3608833 are_congruent_mod 6700417 ; :: thesis: verum

end;

A19: 5 |^ 262144,1394402 are_congruent_mod 6700417

proof

3608833 * 3608833 = (1943711 * 6700417) + 1394402 ;
then 5 |^ (131072 + 131072),1394402 are_congruent_mod 6700417 by A18, LemSq;
hence 5 |^ 262144,1394402 are_congruent_mod 6700417 ; :: thesis: verum

end;

A20: 5 |^ 524288,3130876 are_congruent_mod 6700417

proof

1394402 * 1394402 = (290184 * 6700417) + 3130876 ;
then 5 |^ (262144 + 262144),3130876 are_congruent_mod 6700417 by A19, LemSq;
hence 5 |^ 524288,3130876 are_congruent_mod 6700417 ; :: thesis: verum

end;

A21: 5 |^ 1048576,2776809 are_congruent_mod 6700417

proof

3130876 * 3130876 = (1462951 * 6700417) + 2776809 ;
then 5 |^ (524288 + 524288),2776809 are_congruent_mod 6700417 by A20, LemSq;
hence 5 |^ 1048576,2776809 are_congruent_mod 6700417 ; :: thesis: verum

end;

A22: 5 |^ 2097152,2549723 are_congruent_mod 6700417

proof

2776809 * 2776809 = (1150774 * 6700417) + 2549723 ;
then 5 |^ (1048576 + 1048576),2549723 are_congruent_mod 6700417 by A21, LemSq;
hence 5 |^ 2097152,2549723 are_congruent_mod 6700417 ; :: thesis: verum

end;

A23: 5 |^ 4194304,1082062 are_congruent_mod 6700417

proof

2549723 * 2549723 = (970251 * 6700417) + 1082062 ;
then 5 |^ (2097152 + 2097152),1082062 are_congruent_mod 6700417 by A22, LemSq;
hence 5 |^ 4194304,1082062 are_congruent_mod 6700417 ; :: thesis: verum

end;

A24: 5 |^ 384,1909498 are_congruent_mod 6700417

proof

5231553 * 374828 = (292658 * 6700417) + 1909498 ;
then 5 |^ (128 + 256),1909498 are_congruent_mod 6700417 by A8, A9, LemMul;
hence 5 |^ 384,1909498 are_congruent_mod 6700417 ; :: thesis: verum

end;

A25: 5 |^ 1408,1448571 are_congruent_mod 6700417

proof

1909498 * 2827699 = (805843 * 6700417) + 1448571 ;
then 5 |^ (384 + 1024),1448571 are_congruent_mod 6700417 by A24, A11, LemMul;
hence 5 |^ 1408,1448571 are_congruent_mod 6700417 ; :: thesis: verum

end;

A26: 5 |^ 3456,4182057 are_congruent_mod 6700417

proof

1448571 * 6011821 = (1299702 * 6700417) + 4182057 ;
then 5 |^ (1408 + 2048),4182057 are_congruent_mod 6700417 by A25, A12, LemMul;
hence 5 |^ 3456,4182057 are_congruent_mod 6700417 ; :: thesis: verum

end;

A27: 5 |^ 7552,2283579 are_congruent_mod 6700417

proof

4182057 * 2741794 = (1711287 * 6700417) + 2283579 ;
then 5 |^ (3456 + 4096),2283579 are_congruent_mod 6700417 by A26, A13, LemMul;
hence 5 |^ 7552,2283579 are_congruent_mod 6700417 ; :: thesis: verum

end;

A28: 5 |^ 15744,170659 are_congruent_mod 6700417

proof

2283579 * 1991541 = (678740 * 6700417) + 170659 ;
then 5 |^ (7552 + 8192),170659 are_congruent_mod 6700417 by A27, A14, LemMul;
hence 5 |^ 15744,170659 are_congruent_mod 6700417 ; :: thesis: verum

end;

A29: 5 |^ 146816,4301975 are_congruent_mod 6700417

proof

170659 * 3608833 = (91916 * 6700417) + 4301975 ;
then 5 |^ (15744 + 131072),4301975 are_congruent_mod 6700417 by A28, A18, LemMul;
hence 5 |^ 146816,4301975 are_congruent_mod 6700417 ; :: thesis: verum

end;

A30: 5 |^ 408960,216360 are_congruent_mod 6700417

proof

4301975 * 1394402 = (895270 * 6700417) + 216360 ;
then 5 |^ (146816 + 262144),216360 are_congruent_mod 6700417 by A29, A19, LemMul;
hence 5 |^ 408960,216360 are_congruent_mod 6700417 ; :: thesis: verum

end;

A31: 5 |^ 2506112,6036253 are_congruent_mod 6700417

proof

216360 * 2549723 = (82331 * 6700417) + 6036253 ;
then 5 |^ (408960 + 2097152),6036253 are_congruent_mod 6700417 by A30, A22, LemMul;
hence 5 |^ 2506112,6036253 are_congruent_mod 6700417 ; :: thesis: verum

end;

A32: 5 |^ 6700416,1 are_congruent_mod 6700417

proof

6036253 * 1082062 = (974805 * 6700417) + 1 ;
then 5 |^ (2506112 + 4194304),1 are_congruent_mod 6700417 by A31, A23, LemMul;
hence 5 |^ 6700416,1 are_congruent_mod 6700417 ; :: thesis: verum

end;

A33: 1909497 gcd 6700417 = 1

proof

set d = 1909497 gcd 6700417;
1909497 gcd 6700417 divides 1909497 * 1950542 by INT_2:2, INT_2:21;
then A35: 1909497 gcd 6700417 divides (6700417 * 555869) + 1 ;
1909497 gcd 6700417 divides 6700417 * 555869 by INT_2:2, INT_2:21;
then 1909497 gcd 6700417 divides 1 by A35, INT_2:1;
hence 1909497 gcd 6700417 = 1 by INT_2:13; :: thesis: verum

end;

reconsider n = 6700417 as 2 _greater Nat by NAT_6:def 1;
17449 divides n - 1

proof

take 384 ; :: according to INT_1:def 3 :: thesis: n - 1 = 17449 * 384
thus n - 1 = 17449 * 384 ; :: thesis: verum

end;

then reconsider s = 17449 as Divisor of n - 1 by NAT_6:def 2;
reconsider s = s as non trivial Divisor of n - 1 by NAT_2:def 1;
A36: s > sqrt n

proof

sqrt n < sqrt (s ^2) by SQUARE_1:27;
hence s > sqrt n by SQUARE_1:def 2; :: thesis: verum

end;

now :: thesis: for q being prime Divisor of s holds ((5 |^ ((n - 1) / q)) - 1) gcd n = 1

let q be prime Divisor of s; :: thesis: ((5 |^ ((n - 1) / q)) - 1) gcd n = 1
A37: ( q = 1 or q = s ) by Lem17449, INT_2:def 4, NAT_6:def 2;
(5 |^ 384) - 1,1909498 - 1 are_congruent_mod n by A24;
hence ((5 |^ ((n - 1) / q)) - 1) gcd n = 1 by A33, A37, WSIERP_1:43, INT_2:def 4; :: thesis: verum

end;

hence 6700417 is prime by A36, A32, NAT_6:21; :: thesis: verum