Theorem infpn

Description: There exist infinitely many prime numbers: for any positive integer N , there exists a prime number j greater than N . (See infpn2 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006)

	Ref	Expression
Assertion	infpn	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑗 ∈ ℕ ( 𝑁 < 𝑗 ∧ ∀ 𝑘 ∈ ℕ ( ( 𝑗 / 𝑘 ) ∈ ℕ → ( 𝑘 = 1 ∨ 𝑘 = 𝑗 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( ! ‘ 𝑁 ) + 1 ) = ( ( ! ‘ 𝑁 ) + 1 )
2	1	infpnlem2	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑗 ∈ ℕ ( 𝑁 < 𝑗 ∧ ∀ 𝑘 ∈ ℕ ( ( 𝑗 / 𝑘 ) ∈ ℕ → ( 𝑘 = 1 ∨ 𝑘 = 𝑗 ) ) ) )