:: Primality of 6700417
:: by Library Committee
::
:: Received September 18, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

theorem LemSq: :: XPRIMES3:1

for a, e being Nat
for 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 end;

theorem LemMul: :: XPRIMES3:2

for a, e, f being Nat
for 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 end;

theorem Lem17449: :: XPRIMES3:3

17449 is prime

proof end;

theorem :: XPRIMES3:4

6700417 is prime

proof end;