Metamath Proof Explorer

Theorem infpn2

Description: There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn , so by unben it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005)

Ref Expression
Hypothesis infpn2.1 
|- S = { n e. NN | ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) }
Assertion infpn2 
|- S ~~ NN

Proof

Step Hyp Ref Expression
1 infpn2.1 
 |-  S = { n e. NN | ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) }
2 1 ssrab3 
 |-  S C_ NN
3 infpn 
 |-  ( j e. NN -> E. k e. NN ( j < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) )
4 nnge1 
 |-  ( j e. NN -> 1 <_ j )
5 4 adantr 
 |-  ( ( j e. NN /\ k e. NN ) -> 1 <_ j )
6 1re 
 |-  1 e. RR
7 nnre 
 |-  ( j e. NN -> j e. RR )
8 nnre 
 |-  ( k e. NN -> k e. RR )
9 lelttr 
 |-  ( ( 1 e. RR /\ j e. RR /\ k e. RR ) -> ( ( 1 <_ j /\ j < k ) -> 1 < k ) )
10 6 7 8 9 mp3an3an 
 |-  ( ( j e. NN /\ k e. NN ) -> ( ( 1 <_ j /\ j < k ) -> 1 < k ) )
11 5 10 mpand 
 |-  ( ( j e. NN /\ k e. NN ) -> ( j < k -> 1 < k ) )
12 11 ancld 
 |-  ( ( j e. NN /\ k e. NN ) -> ( j < k -> ( j < k /\ 1 < k ) ) )
13 12 anim1d 
 |-  ( ( j e. NN /\ k e. NN ) -> ( ( j < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) -> ( ( j < k /\ 1 < k ) /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
14 anass 
 |-  ( ( ( j < k /\ 1 < k ) /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) <-> ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
15 13 14 syl6ib 
 |-  ( ( j e. NN /\ k e. NN ) -> ( ( j < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) -> ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) ) )
16 15 reximdva 
 |-  ( j e. NN -> ( E. k e. NN ( j < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) -> E. k e. NN ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) ) )
17 3 16 mpd 
 |-  ( j e. NN -> E. k e. NN ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
18 breq2 
 |-  ( n = k -> ( 1 < n <-> 1 < k ) )
19 oveq1 
 |-  ( n = k -> ( n / m ) = ( k / m ) )
20 19 eleq1d 
 |-  ( n = k -> ( ( n / m ) e. NN <-> ( k / m ) e. NN ) )
21 equequ2 
 |-  ( n = k -> ( m = n <-> m = k ) )
22 21 orbi2d 
 |-  ( n = k -> ( ( m = 1 \/ m = n ) <-> ( m = 1 \/ m = k ) ) )
23 20 22 imbi12d 
 |-  ( n = k -> ( ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) <-> ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) )
24 23 ralbidv 
 |-  ( n = k -> ( A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) <-> A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) )
25 18 24 anbi12d 
 |-  ( n = k -> ( ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) <-> ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
26 25 1 elrab2 
 |-  ( k e. S <-> ( k e. NN /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
27 26 anbi1i 
 |-  ( ( k e. S /\ j < k ) <-> ( ( k e. NN /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) /\ j < k ) )
28 anass 
 |-  ( ( ( k e. NN /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) /\ j < k ) <-> ( k e. NN /\ ( ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) /\ j < k ) ) )
29 ancom 
 |-  ( ( ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) /\ j < k ) <-> ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
30 29 anbi2i 
 |-  ( ( k e. NN /\ ( ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) /\ j < k ) ) <-> ( k e. NN /\ ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) ) )
31 27 28 30 3bitri 
 |-  ( ( k e. S /\ j < k ) <-> ( k e. NN /\ ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) ) )
32 31 rexbii2 
 |-  ( E. k e. S j < k <-> E. k e. NN ( j < k /\ ( 1 < k /\ A. m e. NN ( ( k / m ) e. NN -> ( m = 1 \/ m = k ) ) ) ) )
33 17 32 sylibr 
 |-  ( j e. NN -> E. k e. S j < k )
34 33 rgen 
 |-  A. j e. NN E. k e. S j < k
35 unben 
 |-  ( ( S C_ NN /\ A. j e. NN E. k e. S j < k ) -> S ~~ NN )
36 2 34 35 mp2an 
 |-  S ~~ NN