Theorem nprm

Description: A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Assertion	nprm	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \neg AB\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
2	1	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to A\in \mathbb{Z}$$
3	2	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to A\in ℝ$$
4		eluz2gt1	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to 1<B$$
5	4	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to 1<B$$
6		eluzelz	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in \mathbb{Z}$$
7	6	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to B\in \mathbb{Z}$$
8	7	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to B\in ℝ$$
9		eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$
10	9	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to A\in \mathbb{N}$$
11	10	nngt0d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to 0<A$$
12		ltmulgt11	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge 0<A\right)\to \left(1<B\leftrightarrow A<AB\right)$$
13	3 8 11 12	syl3anc	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \left(1<B\leftrightarrow A<AB\right)$$
14	5 13	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to A<AB$$
15	3 14	ltned	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to A\ne AB$$
16		dvdsmul1	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\parallel AB$$
17	1 6 16	syl2an	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to A\parallel AB$$
18		isprm4	$$⊢AB\in \mathbb{P}\leftrightarrow \left(AB\in {\mathbb{Z}}_{\ge 2}\wedge \forall x\in {\mathbb{Z}}_{\ge 2}\left(x\parallel AB\to x=AB\right)\right)$$
19	18	simprbi	$$⊢AB\in \mathbb{P}\to \forall x\in {\mathbb{Z}}_{\ge 2}\left(x\parallel AB\to x=AB\right)$$
20		breq1	$$⊢x=A\to \left(x\parallel AB\leftrightarrow A\parallel AB\right)$$
21		eqeq1	$$⊢x=A\to \left(x=AB\leftrightarrow A=AB\right)$$
22	20 21	imbi12d	$$⊢x=A\to \left(\left(x\parallel AB\to x=AB\right)\leftrightarrow \left(A\parallel AB\to A=AB\right)\right)$$
23	22	rspcv	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(\forall x\in {\mathbb{Z}}_{\ge 2}\left(x\parallel AB\to x=AB\right)\to \left(A\parallel AB\to A=AB\right)\right)$$
24	19 23	syl5	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(AB\in \mathbb{P}\to \left(A\parallel AB\to A=AB\right)\right)$$
25	24	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \left(AB\in \mathbb{P}\to \left(A\parallel AB\to A=AB\right)\right)$$
26	17 25	mpid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \left(AB\in \mathbb{P}\to A=AB\right)$$
27	26	necon3ad	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \left(A\ne AB\to \neg AB\in \mathbb{P}\right)$$
28	15 27	mpd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \neg AB\in \mathbb{P}$$