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 | |- ( N e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( ( ! ` N ) + 1 ) = ( ( ! ` N ) + 1 ) |
|
| 2 | 1 | infpnlem2 | |- ( N e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) ) |