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 e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) )

Proof

Step Hyp Ref Expression
1 infpnlem.1 
 |-  K = ( ( ! ` N ) + 1 )
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 2 faccld 
 |-  ( N e. NN -> ( ! ` N ) e. NN )
4 3 peano2nnd 
 |-  ( N e. NN -> ( ( ! ` N ) + 1 ) e. NN )
5 1 4 eqeltrid 
 |-  ( N e. NN -> K e. NN )
6 3 nnge1d 
 |-  ( N e. NN -> 1 <_ ( ! ` N ) )
7 1nn 
 |-  1 e. NN
8 nnleltp1 
 |-  ( ( 1 e. NN /\ ( ! ` N ) e. NN ) -> ( 1 <_ ( ! ` N ) <-> 1 < ( ( ! ` N ) + 1 ) ) )
9 7 3 8 sylancr 
 |-  ( N e. NN -> ( 1 <_ ( ! ` N ) <-> 1 < ( ( ! ` N ) + 1 ) ) )
10 6 9 mpbid 
 |-  ( N e. NN -> 1 < ( ( ! ` N ) + 1 ) )
11 10 1 breqtrrdi 
 |-  ( N e. NN -> 1 < K )
12 nncn 
 |-  ( K e. NN -> K e. CC )
13 nnne0 
 |-  ( K e. NN -> K =/= 0 )
14 12 13 jca 
 |-  ( K e. NN -> ( K e. CC /\ K =/= 0 ) )
15 divid 
 |-  ( ( K e. CC /\ K =/= 0 ) -> ( K / K ) = 1 )
16 5 14 15 3syl 
 |-  ( N e. NN -> ( K / K ) = 1 )
17 16 7 eqeltrdi 
 |-  ( N e. NN -> ( K / K ) e. NN )
18 breq2 
 |-  ( j = K -> ( 1 < j <-> 1 < K ) )
19 oveq2 
 |-  ( j = K -> ( K / j ) = ( K / K ) )
20 19 eleq1d 
 |-  ( j = K -> ( ( K / j ) e. NN <-> ( K / K ) e. NN ) )
21 18 20 anbi12d 
 |-  ( j = K -> ( ( 1 < j /\ ( K / j ) e. NN ) <-> ( 1 < K /\ ( K / K ) e. NN ) ) )
22 21 rspcev 
 |-  ( ( K e. NN /\ ( 1 < K /\ ( K / K ) e. NN ) ) -> E. j e. NN ( 1 < j /\ ( K / j ) e. NN ) )
23 5 11 17 22 syl12anc 
 |-  ( N e. NN -> E. j e. NN ( 1 < j /\ ( K / j ) e. NN ) )
24 breq2 
 |-  ( j = k -> ( 1 < j <-> 1 < k ) )
25 oveq2 
 |-  ( j = k -> ( K / j ) = ( K / k ) )
26 25 eleq1d 
 |-  ( j = k -> ( ( K / j ) e. NN <-> ( K / k ) e. NN ) )
27 24 26 anbi12d 
 |-  ( j = k -> ( ( 1 < j /\ ( K / j ) e. NN ) <-> ( 1 < k /\ ( K / k ) e. NN ) ) )
28 27 nnwos 
 |-  ( E. j e. NN ( 1 < j /\ ( K / j ) e. NN ) -> E. j e. NN ( ( 1 < j /\ ( K / j ) e. NN ) /\ A. k e. NN ( ( 1 < k /\ ( K / k ) e. NN ) -> j <_ k ) ) )
29 23 28 syl 
 |-  ( N e. NN -> E. j e. NN ( ( 1 < j /\ ( K / j ) e. NN ) /\ A. k e. NN ( ( 1 < k /\ ( K / k ) e. NN ) -> j <_ k ) ) )
30 1 infpnlem1 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( ( 1 < j /\ ( K / j ) e. NN ) /\ A. k e. NN ( ( 1 < k /\ ( K / k ) e. NN ) -> j <_ k ) ) -> ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) ) )
31 30 reximdva 
 |-  ( N e. NN -> ( E. j e. NN ( ( 1 < j /\ ( K / j ) e. NN ) /\ A. k e. NN ( ( 1 < k /\ ( K / k ) e. NN ) -> j <_ k ) ) -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) ) )
32 29 31 mpd 
 |-  ( N e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) )