Metamath Proof Explorer

Theorem infpnlem2

Description: Lemma for infpn . For any positive integer N , there exists a prime number j greater than N . (Contributed by NM, 5-May-2005)

Ref Expression
Hypothesis infpnlem.1 ⊢ K = N ! + 1
Assertion infpnlem2 ⊢ N ∈ ℕ → ∃ j ∈ ℕ N < j ∧ ∀ k ∈ ℕ j k ∈ ℕ → k = 1 ∨ k = j

Proof

Step Hyp Ref Expression
1 infpnlem.1 ⊢ K = N ! + 1
2 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
3 2 faccld ⊢ N ∈ ℕ → N ! ∈ ℕ
4 3 peano2nnd ⊢ N ∈ ℕ → N ! + 1 ∈ ℕ
5 1 4 eqeltrid ⊢ N ∈ ℕ → K ∈ ℕ
6 3 nnge1d ⊢ N ∈ ℕ → 1 ≤ N !
7 1nn ⊢ 1 ∈ ℕ
8 nnleltp1 ⊢ 1 ∈ ℕ ∧ N ! ∈ ℕ → 1 ≤ N ! ↔ 1 < N ! + 1
9 7 3 8 sylancr ⊢ N ∈ ℕ → 1 ≤ N ! ↔ 1 < N ! + 1
10 6 9 mpbid ⊢ N ∈ ℕ → 1 < N ! + 1
11 10 1 breqtrrdi ⊢ N ∈ ℕ → 1 < K
12 nncn ⊢ K ∈ ℕ → K ∈ ℂ
13 nnne0 ⊢ K ∈ ℕ → K ≠ 0
14 12 13 jca ⊢ K ∈ ℕ → K ∈ ℂ ∧ K ≠ 0
15 divid ⊢ K ∈ ℂ ∧ K ≠ 0 → K K = 1
16 5 14 15 3syl ⊢ N ∈ ℕ → K K = 1
17 16 7 eqeltrdi ⊢ N ∈ ℕ → K K ∈ ℕ
18 breq2 ⊢ j = K → 1 < j ↔ 1 < K
19 oveq2 ⊢ j = K → K j = K K
20 19 eleq1d ⊢ j = K → K j ∈ ℕ ↔ K K ∈ ℕ
21 18 20 anbi12d ⊢ j = K → 1 < j ∧ K j ∈ ℕ ↔ 1 < K ∧ K K ∈ ℕ
22 21 rspcev ⊢ K ∈ ℕ ∧ 1 < K ∧ K K ∈ ℕ → ∃ j ∈ ℕ 1 < j ∧ K j ∈ ℕ
23 5 11 17 22 syl12anc ⊢ N ∈ ℕ → ∃ j ∈ ℕ 1 < j ∧ K j ∈ ℕ
24 breq2 ⊢ j = k → 1 < j ↔ 1 < k
25 oveq2 ⊢ j = k → K j = K k
26 25 eleq1d ⊢ j = k → K j ∈ ℕ ↔ K k ∈ ℕ
27 24 26 anbi12d ⊢ j = k → 1 < j ∧ K j ∈ ℕ ↔ 1 < k ∧ K k ∈ ℕ
28 27 nnwos ⊢ ∃ j ∈ ℕ 1 < j ∧ K j ∈ ℕ → ∃ j ∈ ℕ 1 < j ∧ K j ∈ ℕ ∧ ∀ k ∈ ℕ 1 < k ∧ K k ∈ ℕ → j ≤ k
29 23 28 syl ⊢ N ∈ ℕ → ∃ j ∈ ℕ 1 < j ∧ K j ∈ ℕ ∧ ∀ k ∈ ℕ 1 < k ∧ K k ∈ ℕ → j ≤ k
30 1 infpnlem1 ⊢ N ∈ ℕ ∧ j ∈ ℕ → 1 < j ∧ K j ∈ ℕ ∧ ∀ k ∈ ℕ 1 < k ∧ K k ∈ ℕ → j ≤ k → N < j ∧ ∀ k ∈ ℕ j k ∈ ℕ → k = 1 ∨ k = j
31 30 reximdva ⊢ N ∈ ℕ → ∃ j ∈ ℕ 1 < j ∧ K j ∈ ℕ ∧ ∀ k ∈ ℕ 1 < k ∧ K k ∈ ℕ → j ≤ k → ∃ j ∈ ℕ N < j ∧ ∀ k ∈ ℕ j k ∈ ℕ → k = 1 ∨ k = j
32 29 31 mpd ⊢ N ∈ ℕ → ∃ j ∈ ℕ N < j ∧ ∀ k ∈ ℕ j k ∈ ℕ → k = 1 ∨ k = j