Theorem: Sieve.zeta_lt_self_of_prime (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
⊢ ∀ (p : ℕ), p.Prime → ↑ζ p < ↑p
Tactic:
intro p hp
State after:
p : ℕ
hp : p.Prime
⊢ ↑ζ p < ↑p

State before:
p : ℕ
hp : p.Prime
⊢ ↑ζ p < ↑p
Tactic:
rw [ArithmeticFunction.natCoe_apply, ArithmeticFunction.zeta_apply, if_neg (Nat.Prime.ne_zero hp)]
State after:
p : ℕ
hp : p.Prime
⊢ ↑1 < ↑p

State before:
p : ℕ
hp : p.Prime
⊢ ↑1 < ↑p
Tactic:
norm_num
State after:
p : ℕ
hp : p.Prime
⊢ 1 < p

State before:
p : ℕ
hp : p.Prime
⊢ 1 < p
Tactic:
exact Nat.succ_le.mp (Nat.Prime.two_le hp)
State after:
no goals