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