Theorem nprmi

Description: An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Hypotheses	nprmi.1	$$⊢A\in \mathbb{N}$$
	nprmi.2	$$⊢B\in \mathbb{N}$$
	nprmi.3	$$⊢1<A$$
	nprmi.4	$$⊢1<B$$
	nprmi.5	$$⊢AB=N$$
Assertion	nprmi	$$⊢\neg N\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		nprmi.1	$$⊢A\in \mathbb{N}$$
2		nprmi.2	$$⊢B\in \mathbb{N}$$
3		nprmi.3	$$⊢1<A$$
4		nprmi.4	$$⊢1<B$$
5		nprmi.5	$$⊢AB=N$$
6		eluz2b2	$$⊢A\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(A\in \mathbb{N}\wedge 1<A\right)$$
7		eluz2b2	$$⊢B\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(B\in \mathbb{N}\wedge 1<B\right)$$
8		nprm	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \neg AB\in \mathbb{P}$$
9	6 7 8	syl2anbr	$$⊢\left(\left(A\in \mathbb{N}\wedge 1<A\right)\wedge \left(B\in \mathbb{N}\wedge 1<B\right)\right)\to \neg AB\in \mathbb{P}$$
10	1 3 2 4 9	mp4an	$$⊢\neg AB\in \mathbb{P}$$
11	5	eleq1i	$$⊢AB\in \mathbb{P}\leftrightarrow N\in \mathbb{P}$$
12	10 11	mtbi	$$⊢\neg N\in \mathbb{P}$$