Source indexedlemma · leanprover/lean4:v4.32.0

RS_prime_helper.pi_nth_prime'

PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean:57 to 64

Mathematical statement

Exact Lean statement

lemma pi_nth_prime' (n : ℕ) (hn : n ≥ 1) :
    pi (nth_prime' n) = n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pi_nth_prime' (n : ℕ) (hn : n ≥ 1) :    pi (nth_prime' n) = n := by  have h_pi_eq : pi (nth_prime' n) = Nat.primeCounting (nth_prime' n) := by norm_num [pi]  have h_prime_counting : primeCounting (nth_prime' n) = count Nat.Prime (nth_prime' n + 1) :=    add_zero (List.countP.go (fun b ↦ decide (Nat.Prime b)) (List.range (nth_prime' n + 1)) 0)  have h_count : count Nat.Prime (nth_prime' n) = n - 1 := by    convert count_nth_of_infinite (infinite_setOf_prime) (n - 1) using 1  rcases n <;> simp_all [count_succ]