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

Metamath Proof Explorer

Theorem isprm4

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only divisor greater than or equal to 2 is itself. (Contributed by Paul Chapman, 26-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 isprm2 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
2 eluz2b3 
 |-  ( z e. ( ZZ>= ` 2 ) <-> ( z e. NN /\ z =/= 1 ) )
3 2 imbi1i 
 |-  ( ( z e. ( ZZ>= ` 2 ) -> ( z || P -> z = P ) ) <-> ( ( z e. NN /\ z =/= 1 ) -> ( z || P -> z = P ) ) )
4 impexp 
 |-  ( ( ( z e. NN /\ z =/= 1 ) -> ( z || P -> z = P ) ) <-> ( z e. NN -> ( z =/= 1 -> ( z || P -> z = P ) ) ) )
5 bi2.04 
 |-  ( ( z =/= 1 -> ( z || P -> z = P ) ) <-> ( z || P -> ( z =/= 1 -> z = P ) ) )
6 df-ne 
 |-  ( z =/= 1 <-> -. z = 1 )
7 6 imbi1i 
 |-  ( ( z =/= 1 -> z = P ) <-> ( -. z = 1 -> z = P ) )
8 df-or 
 |-  ( ( z = 1 \/ z = P ) <-> ( -. z = 1 -> z = P ) )
9 7 8 bitr4i 
 |-  ( ( z =/= 1 -> z = P ) <-> ( z = 1 \/ z = P ) )
10 9 imbi2i 
 |-  ( ( z || P -> ( z =/= 1 -> z = P ) ) <-> ( z || P -> ( z = 1 \/ z = P ) ) )
11 5 10 bitri 
 |-  ( ( z =/= 1 -> ( z || P -> z = P ) ) <-> ( z || P -> ( z = 1 \/ z = P ) ) )
12 11 imbi2i 
 |-  ( ( z e. NN -> ( z =/= 1 -> ( z || P -> z = P ) ) ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
13 4 12 bitri 
 |-  ( ( ( z e. NN /\ z =/= 1 ) -> ( z || P -> z = P ) ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
14 3 13 bitri 
 |-  ( ( z e. ( ZZ>= ` 2 ) -> ( z || P -> z = P ) ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
15 14 ralbii2 
 |-  ( A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) <-> A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) )
16 15 anbi2i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) ) <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
17 1 16 bitr4i 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) ) )