Metamath Proof Explorer

Theorem isprm2lem

Description: Lemma for isprm2 . (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion isprm2lem 
|- ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } ~~ 2o <-> { n e. NN | n || P } = { 1 , P } ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> P =/= 1 )
2 1 necomd 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> 1 =/= P )
3 simpr 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> { n e. NN | n || P } ~~ 2o )
4 nnz 
 |-  ( P e. NN -> P e. ZZ )
5 1dvds 
 |-  ( P e. ZZ -> 1 || P )
6 4 5 syl 
 |-  ( P e. NN -> 1 || P )
7 6 ad2antrr 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> 1 || P )
8 1nn 
 |-  1 e. NN
9 breq1 
 |-  ( n = 1 -> ( n || P <-> 1 || P ) )
10 9 elrab3 
 |-  ( 1 e. NN -> ( 1 e. { n e. NN | n || P } <-> 1 || P ) )
11 8 10 ax-mp 
 |-  ( 1 e. { n e. NN | n || P } <-> 1 || P )
12 7 11 sylibr 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> 1 e. { n e. NN | n || P } )
13 iddvds 
 |-  ( P e. ZZ -> P || P )
14 4 13 syl 
 |-  ( P e. NN -> P || P )
15 14 ad2antrr 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> P || P )
16 breq1 
 |-  ( n = P -> ( n || P <-> P || P ) )
17 16 elrab3 
 |-  ( P e. NN -> ( P e. { n e. NN | n || P } <-> P || P ) )
18 17 ad2antrr 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> ( P e. { n e. NN | n || P } <-> P || P ) )
19 15 18 mpbird 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> P e. { n e. NN | n || P } )
20 en2eqpr 
 |-  ( ( { n e. NN | n || P } ~~ 2o /\ 1 e. { n e. NN | n || P } /\ P e. { n e. NN | n || P } ) -> ( 1 =/= P -> { n e. NN | n || P } = { 1 , P } ) )
21 3 12 19 20 syl3anc 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> ( 1 =/= P -> { n e. NN | n || P } = { 1 , P } ) )
22 2 21 mpd 
 |-  ( ( ( P e. NN /\ P =/= 1 ) /\ { n e. NN | n || P } ~~ 2o ) -> { n e. NN | n || P } = { 1 , P } )
23 22 ex 
 |-  ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } ~~ 2o -> { n e. NN | n || P } = { 1 , P } ) )
24 necom 
 |-  ( 1 =/= P <-> P =/= 1 )
25 pr2ne 
 |-  ( ( 1 e. NN /\ P e. NN ) -> ( { 1 , P } ~~ 2o <-> 1 =/= P ) )
26 8 25 mpan 
 |-  ( P e. NN -> ( { 1 , P } ~~ 2o <-> 1 =/= P ) )
27 26 biimpar 
 |-  ( ( P e. NN /\ 1 =/= P ) -> { 1 , P } ~~ 2o )
28 24 27 sylan2br 
 |-  ( ( P e. NN /\ P =/= 1 ) -> { 1 , P } ~~ 2o )
29 breq1 
 |-  ( { n e. NN | n || P } = { 1 , P } -> ( { n e. NN | n || P } ~~ 2o <-> { 1 , P } ~~ 2o ) )
30 28 29 syl5ibrcom 
 |-  ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } = { 1 , P } -> { n e. NN | n || P } ~~ 2o ) )
31 23 30 impbid 
 |-  ( ( P e. NN /\ P =/= 1 ) -> ( { n e. NN | n || P } ~~ 2o <-> { n e. NN | n || P } = { 1 , P } ) )