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\in \mathbb{P}\leftrightarrow \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isprm2	$$⊢P\in \mathbb{P}\leftrightarrow \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in \mathbb{N}\left(z\parallel P\to \left(z=1\vee z=P\right)\right)\right)$$
2		eluz2b3	$$⊢z\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(z\in \mathbb{N}\wedge z\ne 1\right)$$
3	2	imbi1i	$$⊢\left(z\in {\mathbb{Z}}_{\ge 2}\to \left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(\left(z\in \mathbb{N}\wedge z\ne 1\right)\to \left(z\parallel P\to z=P\right)\right)$$
4		impexp	$$⊢\left(\left(z\in \mathbb{N}\wedge z\ne 1\right)\to \left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(z\in \mathbb{N}\to \left(z\ne 1\to \left(z\parallel P\to z=P\right)\right)\right)$$
5		bi2.04	$$⊢\left(z\ne 1\to \left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(z\parallel P\to \left(z\ne 1\to z=P\right)\right)$$
6		df-ne	$$⊢z\ne 1\leftrightarrow \neg z=1$$
7	6	imbi1i	$$⊢\left(z\ne 1\to z=P\right)\leftrightarrow \left(\neg z=1\to z=P\right)$$
8		df-or	$$⊢\left(z=1\vee z=P\right)\leftrightarrow \left(\neg z=1\to z=P\right)$$
9	7 8	bitr4i	$$⊢\left(z\ne 1\to z=P\right)\leftrightarrow \left(z=1\vee z=P\right)$$
10	9	imbi2i	$$⊢\left(z\parallel P\to \left(z\ne 1\to z=P\right)\right)\leftrightarrow \left(z\parallel P\to \left(z=1\vee z=P\right)\right)$$
11	5 10	bitri	$$⊢\left(z\ne 1\to \left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(z\parallel P\to \left(z=1\vee z=P\right)\right)$$
12	11	imbi2i	$$⊢\left(z\in \mathbb{N}\to \left(z\ne 1\to \left(z\parallel P\to z=P\right)\right)\right)\leftrightarrow \left(z\in \mathbb{N}\to \left(z\parallel P\to \left(z=1\vee z=P\right)\right)\right)$$
13	4 12	bitri	$$⊢\left(\left(z\in \mathbb{N}\wedge z\ne 1\right)\to \left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(z\in \mathbb{N}\to \left(z\parallel P\to \left(z=1\vee z=P\right)\right)\right)$$
14	3 13	bitri	$$⊢\left(z\in {\mathbb{Z}}_{\ge 2}\to \left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(z\in \mathbb{N}\to \left(z\parallel P\to \left(z=1\vee z=P\right)\right)\right)$$
15	14	ralbii2	$$⊢\forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)\leftrightarrow \forall z\in \mathbb{N}\left(z\parallel P\to \left(z=1\vee z=P\right)\right)$$
16	15	anbi2i	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)\right)\leftrightarrow \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in \mathbb{N}\left(z\parallel P\to \left(z=1\vee z=P\right)\right)\right)$$
17	1 16	bitr4i	$$⊢P\in \mathbb{P}\leftrightarrow \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)\right)$$