Existence of a sufficiently large prime for which a * c ^ p / (p - 1)! < 1

This is a technical result used in the proof of the Lindemann-Weierstrass theorem.

TODO: delete this file, as all its lemmas have been deprecated.

@[deprecated Nat.eventually_mul_pow_lt_factorial_sub]

theorem Nat.exists_prime_mul_pow_lt_factorial (n : ℕ) (a : ℕ) (c : ℕ) : ∃ p > n, Nat.Prime p ∧ a * c ^ p < (p - 1).factorial

@[deprecated FloorSemiring.eventually_mul_pow_lt_factorial_sub]

theorem FloorRing.exists_prime_mul_pow_lt_factorial {K : Type u_1} [LinearOrderedRing K] [FloorRing K] (n : ℕ) (a : K) (c : K) : ∃ p > n, Nat.Prime p ∧ a * c ^ p < ↑(p - 1).factorial

@[deprecated FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop]

theorem FloorRing.exists_prime_mul_pow_div_factorial_lt_one {K : Type u_1} [LinearOrderedField K] [FloorRing K] (n : ℕ) (a : K) (c : K) : ∃ p > n, Nat.Prime p ∧ a * c ^ p / ↑(p - 1).factorial < 1