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 e. NN
	nprmi.2	|- B e. NN
	nprmi.3	|- 1 < A
	nprmi.4	|- 1 < B
	nprmi.5	|- ( A x. B ) = N
Assertion	nprmi	|- -. N e. Prime

Proof

Step	Hyp	Ref	Expression
1		nprmi.1	|- A e. NN
2		nprmi.2	|- B e. NN
3		nprmi.3	|- 1 < A
4		nprmi.4	|- 1 < B
5		nprmi.5	|- ( A x. B ) = N
6		eluz2b2	|- ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ 1 < A ) )
7		eluz2b2	|- ( B e. ( ZZ>= ` 2 ) <-> ( B e. NN /\ 1 < B ) )
8		nprm	|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> -. ( A x. B ) e. Prime )
9	6 7 8	syl2anbr	|- ( ( ( A e. NN /\ 1 < A ) /\ ( B e. NN /\ 1 < B ) ) -> -. ( A x. B ) e. Prime )
10	1 3 2 4 9	mp4an	|- -. ( A x. B ) e. Prime
11	5	eleq1i	|- ( ( A x. B ) e. Prime <-> N e. Prime )
12	10 11	mtbi	|- -. N e. Prime