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 ⊢ 𝐾 = ( ( ! ‘ 𝑁 ) + 1 )
Assertion infpnlem2 ( 𝑁 ∈ ℕ → ∃ 𝑗 ∈ ℕ ( 𝑁 < 𝑗 ∧ ∀ 𝑘 ∈ ℕ ( ( 𝑗 / 𝑘 ) ∈ ℕ → ( 𝑘 = 1 ∨ 𝑘 = 𝑗 ) ) ) )

Proof

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