A rigorous time bound for factoring integers