theorem Th54: :: NUMBER14:54

for m being positive Nat
for k being Nat
for S being Sierp49FS of m,k
for q being CR_Sequence st q = PrimeDivisorsFS m holds
ex a, b being positive Nat st
( 2 * k = a - b & a,m are_coprime & b,m are_coprime & a = ((CRT (S,q)) + (Product q)) + (2 * k) & b = (CRT (S,q)) + (Product q) )