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 ∨ 𝑘 = 𝑗 ) ) ) )