:: Primality of 6700417
:: by Library Committee
::
:: Received September 18, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, XXREAL_0, RELAT_1, ARYTM_3, NEWTON, INT_1,
SUBSET_1, ARYTM_1, INT_2, NAT_1, SQUARE_1, ZFMISC_1, NAT_6;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, SQUARE_1, INT_2,
XXREAL_0, NEWTON, NAT_6;
constructors NAT_D, PEPIN, EC_PF_2, INT_7, NAT_6;
registrations XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, SQUARE_1, INT_2, NAT_6;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions INT_1;
equalities SQUARE_1;
expansions INT_1;
theorems INT_1, INT_2, NAT_2, NEWTON, NAT_4, SQUARE_1, NAT_6, XPRIMET1,
WSIERP_1;
begin
theorem LemSq:
for a,e being Nat, n,r,s,k being Integer st
a|^e,r are_congruent_mod n & r*r = k*n+s
holds a|^(e+e),s are_congruent_mod n
proof
let a,e be Nat;
let n,r,s,k be Integer;
assume that
A1: a|^e,r are_congruent_mod n and
A2: r*r = k*n+s;
(a|^e)*(a|^e),r*r are_congruent_mod n by A1,INT_1:18;
then
A3: a|^(e+e),r*r are_congruent_mod n by NEWTON:8;
r*r,s are_congruent_mod n by A2;
hence thesis by A3,INT_1:15;
end;
theorem LemMul:
for a,e,f being Nat, n,r,s,t,k being Integer st
a|^e,r are_congruent_mod n &
a|^f,s are_congruent_mod n & r*s = k*n+t
holds a|^(e+f),t are_congruent_mod n
proof
let a,e,f be Nat;
let n,r,s,t,k be Integer;
assume that
A1: a|^e,r are_congruent_mod n and
A2: a|^f,s are_congruent_mod n and
A3: r*s = k*n+t;
(a|^e)*(a|^f),r*s are_congruent_mod n by A1,A2,INT_1:18;
then
A4: a|^(e+f),r*s are_congruent_mod n by NEWTON:8;
r*s,t are_congruent_mod n by A3;
hence thesis by A4,INT_1:15;
end;
theorem Lem17449:
17449 is prime
proof
now
17449 = 2*8724 + 1; hence not 2 divides 17449 by NAT_4:9;
17449 = 3*5816 + 1; hence not 3 divides 17449 by NAT_4:9;
17449 = 5*3489 + 4; hence not 5 divides 17449 by NAT_4:9;
17449 = 7*2492 + 5; hence not 7 divides 17449 by NAT_4:9;
17449 = 11*1586 + 3; hence not 11 divides 17449 by NAT_4:9;
17449 = 13*1342 + 3; hence not 13 divides 17449 by NAT_4:9;
17449 = 17*1026 + 7; hence not 17 divides 17449 by NAT_4:9;
17449 = 19*918 + 7; hence not 19 divides 17449 by NAT_4:9;
17449 = 23*758 + 15; hence not 23 divides 17449 by NAT_4:9;
17449 = 29*601 + 20; hence not 29 divides 17449 by NAT_4:9;
17449 = 31*562 + 27; hence not 31 divides 17449 by NAT_4:9;
17449 = 37*471 + 22; hence not 37 divides 17449 by NAT_4:9;
17449 = 41*425 + 24; hence not 41 divides 17449 by NAT_4:9;
17449 = 43*405 + 34; hence not 43 divides 17449 by NAT_4:9;
17449 = 47*371 + 12; hence not 47 divides 17449 by NAT_4:9;
17449 = 53*329 + 12; hence not 53 divides 17449 by NAT_4:9;
17449 = 59*295 + 44; hence not 59 divides 17449 by NAT_4:9;
17449 = 61*286 + 3; hence not 61 divides 17449 by NAT_4:9;
17449 = 67*260 + 29; hence not 67 divides 17449 by NAT_4:9;
17449 = 71*245 + 54; hence not 71 divides 17449 by NAT_4:9;
17449 = 73*239 + 2; hence not 73 divides 17449 by NAT_4:9;
17449 = 79*220 + 69; hence not 79 divides 17449 by NAT_4:9;
17449 = 83*210 + 19; hence not 83 divides 17449 by NAT_4:9;
17449 = 89*196 + 5; hence not 89 divides 17449 by NAT_4:9;
17449 = 97*179 + 86; hence not 97 divides 17449 by NAT_4:9;
17449 = 101*172 + 77; hence not 101 divides 17449 by NAT_4:9;
17449 = 103*169 + 42; hence not 103 divides 17449 by NAT_4:9;
17449 = 107*163 + 8; hence not 107 divides 17449 by NAT_4:9;
17449 = 109*160 + 9; hence not 109 divides 17449 by NAT_4:9;
17449 = 113*154 + 47; hence not 113 divides 17449 by NAT_4:9;
17449 = 127*137 + 50; hence not 127 divides 17449 by NAT_4:9;
17449 = 131*133 + 26; hence not 131 divides 17449 by NAT_4:9;
end;
then for p being Element of NAT st 1 < p & p*p <= 17449 & p is prime
holds not p divides 17449 by XPRIMET1:64;
hence thesis by NAT_4:14;
end;
theorem
6700417 is prime
proof
set N = 6700417;
set a = 5;
A1: a|^1,5 are_congruent_mod N by INT_1:11;
A2: a|^2,25 are_congruent_mod N
proof
5*5 = 0*N+25;
then a|^(1+1),25 are_congruent_mod N by A1,LemSq;
hence thesis;
end;
A3: a|^4,625 are_congruent_mod N
proof
25*25 = 0*N+625;
then a|^(2+2),625 are_congruent_mod N by A2,LemSq;
hence thesis;
end;
A4: a|^8,390625 are_congruent_mod N
proof
625*625 = 0*N+390625;
then a|^(4+4),390625 are_congruent_mod N by A3,LemSq;
hence thesis;
end;
A5: a|^16,5994701 are_congruent_mod N
proof
390625*390625 = 22772*N+5994701;
then a|^(8+8),5994701 are_congruent_mod N by A4,LemSq;
hence thesis;
end;
A6: a|^32,6477880 are_congruent_mod N
proof
5994701*5994701 = 5363313*N+6477880;
then a|^(16+16),6477880 are_congruent_mod N by A5,LemSq;
hence thesis;
end;
A7: a|^64,6634739 are_congruent_mod N
proof
6477880*6477880 = 6262733*N+6634739;
then a|^(32+32),6634739 are_congruent_mod N by A6,LemSq;
hence thesis;
end;
A8: a|^128,5231553 are_congruent_mod N
proof
6634739*6634739 = 6569704*N+5231553;
then a|^(64+64),5231553 are_congruent_mod N by A7,LemSq;
hence thesis;
end;
A9: a|^256,374828 are_congruent_mod N
proof
5231553*5231553 = 4084693*N+374828;
then a|^(128+128),374828 are_congruent_mod N by A8,LemSq;
hence thesis;
end;
A10: a|^512,1685928 are_congruent_mod N
proof
374828*374828 = 20968*N+1685928;
then a|^(256+256),1685928 are_congruent_mod N by A9,LemSq;
hence thesis;
end;
A11: a|^1024,2827699 are_congruent_mod N
proof
1685928*1685928 = 424205*N+2827699;
then a|^(512+512),2827699 are_congruent_mod N by A10,LemSq;
hence thesis;
end;
A12: a|^2048,6011821 are_congruent_mod N
proof
2827699*2827699 = 1193340*N+6011821;
then a|^(1024+1024),6011821 are_congruent_mod N by A11,LemSq;
hence thesis;
end;
A13: a|^4096,2741794 are_congruent_mod N
proof
6011821*6011821 = 5393991*N+2741794;
then a|^(2048+2048),2741794 are_congruent_mod N by A12,LemSq;
hence thesis;
end;
A14: a|^8192,1991541 are_congruent_mod N
proof
2741794*2741794 = 1121935*N+1991541;
then a|^(4096+4096),1991541 are_congruent_mod N by A13,LemSq;
hence thesis;
end;
A15: a|^16384,4116535 are_congruent_mod N
proof
1991541*1991541 = 591938*N+4116535;
then a|^(8192+8192),4116535 are_congruent_mod N by A14,LemSq;
hence thesis;
end;
A16: a|^32768,3281950 are_congruent_mod N
proof
4116535*4116535 = 2529075*N+3281950;
then a|^(16384+16384),3281950 are_congruent_mod N by A15,LemSq;
hence thesis;
end;
A17: a|^65536,757903 are_congruent_mod N
proof
3281950*3281950 = 1607541*N+757903;
then a|^(32768+32768),757903 are_congruent_mod N by A16,LemSq;
hence thesis;
end;
A18: a|^131072,3608833 are_congruent_mod N
proof
757903*757903 = 85728*N+3608833;
then a|^(65536+65536),3608833 are_congruent_mod N by A17,LemSq;
hence thesis;
end;
A19: a|^262144,1394402 are_congruent_mod N
proof
3608833*3608833 = 1943711*N+1394402;
then a|^(131072+131072),1394402 are_congruent_mod N by A18,LemSq;
hence thesis;
end;
A20: a|^524288,3130876 are_congruent_mod N
proof
1394402*1394402 = 290184*N+3130876;
then a|^(262144+262144),3130876 are_congruent_mod N by A19,LemSq;
hence thesis;
end;
A21: a|^1048576,2776809 are_congruent_mod N
proof
3130876*3130876 = 1462951*N+2776809;
then a|^(524288+524288),2776809 are_congruent_mod N by A20,LemSq;
hence thesis;
end;
A22: a|^2097152,2549723 are_congruent_mod N
proof
2776809*2776809 = 1150774*N+2549723;
then a|^(1048576+1048576),2549723 are_congruent_mod N by A21,LemSq;
hence thesis;
end;
A23: a|^4194304,1082062 are_congruent_mod N
proof
2549723*2549723 = 970251*N+1082062;
then a|^(2097152+2097152),1082062 are_congruent_mod N by A22,LemSq;
hence thesis;
end;
A24: a|^384,1909498 are_congruent_mod N
proof
5231553*374828 = 292658*N+1909498;
then a|^(128+256),1909498 are_congruent_mod N by A8,A9,LemMul;
hence thesis;
end;
A25: a|^1408,1448571 are_congruent_mod N
proof
1909498*2827699 = 805843*N+1448571;
then a|^(384+1024),1448571 are_congruent_mod N by A24,A11,LemMul;
hence thesis;
end;
A26: a|^3456,4182057 are_congruent_mod N
proof
1448571*6011821 = 1299702*N+4182057;
then a|^(1408+2048),4182057 are_congruent_mod N by A25,A12,LemMul;
hence thesis;
end;
A27: a|^7552,2283579 are_congruent_mod N
proof
4182057*2741794 = 1711287*N+2283579;
then a|^(3456+4096),2283579 are_congruent_mod N by A26,A13,LemMul;
hence thesis;
end;
A28: a|^15744,170659 are_congruent_mod N
proof
2283579*1991541 = 678740*N+170659;
then a|^(7552+8192),170659 are_congruent_mod N by A27,A14,LemMul;
hence thesis;
end;
A29: a|^146816,4301975 are_congruent_mod N
proof
170659*3608833 = 91916*N+4301975;
then a|^(15744+131072),4301975 are_congruent_mod N
by A28,A18,LemMul;
hence thesis;
end;
A30: a|^408960,216360 are_congruent_mod N
proof
4301975*1394402 = 895270*N+216360;
then a|^(146816+262144),216360 are_congruent_mod N
by A29,A19,LemMul;
hence thesis;
end;
A31: a|^2506112,6036253 are_congruent_mod N
proof
216360*2549723 = 82331*N+6036253;
then a|^(408960+2097152),6036253 are_congruent_mod N
by A30,A22,LemMul;
hence thesis;
end;
A32: a|^6700416,1 are_congruent_mod N
proof
6036253*1082062 = 974805*N+1;
then a|^(2506112+4194304),1 are_congruent_mod N
by A31,A23,LemMul;
hence thesis;
end;
A33: 1909497 gcd 6700417 = 1
proof
set d = 1909497 gcd 6700417;
d divides 1909497*1950542 by INT_2:2,21;
then
A35: d divides 6700417*555869+1;
d divides 6700417*555869 by INT_2:2,21;
then d divides 1 by A35,INT_2:1;
hence thesis by INT_2:13;
end;
reconsider n = 6700417 as 2_greater Nat by NAT_6:def 1;
17449 divides n-1
proof
take 384;
thus thesis;
end;
then reconsider s = 17449 as Divisor of n-1 by NAT_6:def 2;
reconsider 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 thesis by SQUARE_1:def 2;
end;
now
let q be prime Divisor of s;
A37: q = 1 or q = s by Lem17449,INT_2:def 4,NAT_6:def 2;
a|^384-1,1909498-1 are_congruent_mod n by A24;
hence a|^((n-1)/q)-1 gcd n = 1 by A33,A37,WSIERP_1:43,INT_2:def 4;
end;
hence thesis by A36,A32,NAT_6:21;
end;