This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1nprm

Description: 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Fan Zheng, 3-Jul-2016)

Ref Expression
Assertion 1nprm 
|- -. 1 e. Prime

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 eleq1 
 |-  ( z = 1 -> ( z e. NN <-> 1 e. NN ) )
3 1 2 mpbiri 
 |-  ( z = 1 -> z e. NN )
4 nnnn0 
 |-  ( z e. NN -> z e. NN0 )
5 dvds1 
 |-  ( z e. NN0 -> ( z || 1 <-> z = 1 ) )
6 4 5 syl 
 |-  ( z e. NN -> ( z || 1 <-> z = 1 ) )
7 6 bicomd 
 |-  ( z e. NN -> ( z = 1 <-> z || 1 ) )
8 3 7 biadanii 
 |-  ( z = 1 <-> ( z e. NN /\ z || 1 ) )
9 velsn 
 |-  ( z e. { 1 } <-> z = 1 )
10 breq1 
 |-  ( n = z -> ( n || 1 <-> z || 1 ) )
11 10 elrab 
 |-  ( z e. { n e. NN | n || 1 } <-> ( z e. NN /\ z || 1 ) )
12 8 9 11 3bitr4ri 
 |-  ( z e. { n e. NN | n || 1 } <-> z e. { 1 } )
13 12 eqriv 
 |-  { n e. NN | n || 1 } = { 1 }
14 1ex 
 |-  1 e. _V
15 14 ensn1 
 |-  { 1 } ~~ 1o
16 13 15 eqbrtri 
 |-  { n e. NN | n || 1 } ~~ 1o
17 1sdom2 
 |-  1o ~< 2o
18 ensdomtr 
 |-  ( ( { n e. NN | n || 1 } ~~ 1o /\ 1o ~< 2o ) -> { n e. NN | n || 1 } ~< 2o )
19 16 17 18 mp2an 
 |-  { n e. NN | n || 1 } ~< 2o
20 sdomnen 
 |-  ( { n e. NN | n || 1 } ~< 2o -> -. { n e. NN | n || 1 } ~~ 2o )
21 19 20 ax-mp 
 |-  -. { n e. NN | n || 1 } ~~ 2o
22 isprm 
 |-  ( 1 e. Prime <-> ( 1 e. NN /\ { n e. NN | n || 1 } ~~ 2o ) )
23 1 22 mpbiran 
 |-  ( 1 e. Prime <-> { n e. NN | n || 1 } ~~ 2o )
24 21 23 mtbir 
 |-  -. 1 e. Prime