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 ) ) )