Metamath Proof Explorer

Theorem isprm2

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only positive divisors are 1 and itself. Definition in ApostolNT p. 16. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion isprm2 
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )

Proof

Step Hyp Ref Expression
1 1nprm 
 |-  -. 1 e. Prime
2 eleq1 
 |-  ( P = 1 -> ( P e. Prime <-> 1 e. Prime ) )
3 2 biimpcd 
 |-  ( P e. Prime -> ( P = 1 -> 1 e. Prime ) )
4 1 3 mtoi 
 |-  ( P e. Prime -> -. P = 1 )
5 4 neqned 
 |-  ( P e. Prime -> P =/= 1 )
6 5 pm4.71i 
 |-  ( P e. Prime <-> ( P e. Prime /\ P =/= 1 ) )
7 isprm 
 |-  ( P e. Prime <-> ( P e. NN /\ { n e. NN | n || P } ~~ 2o ) )
8 isprm2lem 
 |-  ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } ~~ 2o <-> { n e. NN | n || P } = { 1 , P } ) )
9 eqss 
 |-  ( { n e. NN | n || P } = { 1 , P } <-> ( { n e. NN | n || P } C_ { 1 , P } /\ { 1 , P } C_ { n e. NN | n || P } ) )
10 9 imbi2i 
 |-  ( ( P e. NN -> { n e. NN | n || P } = { 1 , P } ) <-> ( P e. NN -> ( { n e. NN | n || P } C_ { 1 , P } /\ { 1 , P } C_ { n e. NN | n || P } ) ) )
11 1idssfct 
 |-  ( P e. NN -> { 1 , P } C_ { n e. NN | n || P } )
12 jcab 
 |-  ( ( P e. NN -> ( { n e. NN | n || P } C_ { 1 , P } /\ { 1 , P } C_ { n e. NN | n || P } ) ) <-> ( ( P e. NN -> { n e. NN | n || P } C_ { 1 , P } ) /\ ( P e. NN -> { 1 , P } C_ { n e. NN | n || P } ) ) )
13 11 12 mpbiran2 
 |-  ( ( P e. NN -> ( { n e. NN | n || P } C_ { 1 , P } /\ { 1 , P } C_ { n e. NN | n || P } ) ) <-> ( P e. NN -> { n e. NN | n || P } C_ { 1 , P } ) )
14 10 13 bitri 
 |-  ( ( P e. NN -> { n e. NN | n || P } = { 1 , P } ) <-> ( P e. NN -> { n e. NN | n || P } C_ { 1 , P } ) )
15 14 pm5.74ri 
 |-  ( P e. NN -> ( { n e. NN | n || P } = { 1 , P } <-> { n e. NN | n || P } C_ { 1 , P } ) )
16 15 adantr 
 |-  ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } = { 1 , P } <-> { n e. NN | n || P } C_ { 1 , P } ) )
17 8 16 bitrd 
 |-  ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } ~~ 2o <-> { n e. NN | n || P } C_ { 1 , P } ) )
18 17 expcom 
 |-  ( P =/= 1 -> ( P e. NN -> ( { n e. NN | n || P } ~~ 2o <-> { n e. NN | n || P } C_ { 1 , P } ) ) )
19 18 pm5.32d 
 |-  ( P =/= 1 -> ( ( P e. NN /\ { n e. NN | n || P } ~~ 2o ) <-> ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) ) )
20 7 19 syl5bb 
 |-  ( P =/= 1 -> ( P e. Prime <-> ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) ) )
21 20 pm5.32ri 
 |-  ( ( P e. Prime /\ P =/= 1 ) <-> ( ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) /\ P =/= 1 ) )
22 ancom 
 |-  ( ( ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) /\ P =/= 1 ) <-> ( P =/= 1 /\ ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) ) )
23 anass 
 |-  ( ( ( P =/= 1 /\ P e. NN ) /\ { n e. NN | n || P } C_ { 1 , P } ) <-> ( P =/= 1 /\ ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) ) )
24 22 23 bitr4i 
 |-  ( ( ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) /\ P =/= 1 ) <-> ( ( P =/= 1 /\ P e. NN ) /\ { n e. NN | n || P } C_ { 1 , P } ) )
25 ancom 
 |-  ( ( P =/= 1 /\ P e. NN ) <-> ( P e. NN /\ P =/= 1 ) )
26 eluz2b3 
 |-  ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ P =/= 1 ) )
27 25 26 bitr4i 
 |-  ( ( P =/= 1 /\ P e. NN ) <-> P e. ( ZZ>= ` 2 ) )
28 27 anbi1i 
 |-  ( ( ( P =/= 1 /\ P e. NN ) /\ { n e. NN | n || P } C_ { 1 , P } ) <-> ( P e. ( ZZ>= ` 2 ) /\ { n e. NN | n || P } C_ { 1 , P } ) )
29 dfss2 
 |-  ( { n e. NN | n || P } C_ { 1 , P } <-> A. z ( z e. { n e. NN | n || P } -> z e. { 1 , P } ) )
30 breq1 
 |-  ( n = z -> ( n || P <-> z || P ) )
31 30 elrab 
 |-  ( z e. { n e. NN | n || P } <-> ( z e. NN /\ z || P ) )
32 vex 
 |-  z e. _V
33 32 elpr 
 |-  ( z e. { 1 , P } <-> ( z = 1 \/ z = P ) )
34 31 33 imbi12i 
 |-  ( ( z e. { n e. NN | n || P } -> z e. { 1 , P } ) <-> ( ( z e. NN /\ z || P ) -> ( z = 1 \/ z = P ) ) )
35 impexp 
 |-  ( ( ( z e. NN /\ z || P ) -> ( z = 1 \/ z = P ) ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
36 34 35 bitri 
 |-  ( ( z e. { n e. NN | n || P } -> z e. { 1 , P } ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
37 36 albii 
 |-  ( A. z ( z e. { n e. NN | n || P } -> z e. { 1 , P } ) <-> A. z ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
38 df-ral 
 |-  ( A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) <-> A. z ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
39 37 38 bitr4i 
 |-  ( A. z ( z e. { n e. NN | n || P } -> z e. { 1 , P } ) <-> A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) )
40 29 39 bitri 
 |-  ( { n e. NN | n || P } C_ { 1 , P } <-> A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) )
41 40 anbi2i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ { n e. NN | n || P } C_ { 1 , P } ) <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
42 24 28 41 3bitri 
 |-  ( ( ( P e. NN /\ { n e. NN | n || P } C_ { 1 , P } ) /\ P =/= 1 ) <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
43 6 21 42 3bitri 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )