isprm6

Description: A number is prime iff it satisfies Euclid's lemma euclemma . (Contributed by Mario Carneiro, 6-Sep-2015)

		Ref	Expression
	Assertion	isprm6	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y)))$

Proof

Step	Hyp	Ref	Expression
1		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
2		euclemma	$⊢ (P \in ℙ \land x \in ℤ \land y \in ℤ) \to (P ∥ x y \leftrightarrow (P ∥ x \lor P ∥ y))$
3	2	3expb	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℤ)) \to (P ∥ x y \leftrightarrow (P ∥ x \lor P ∥ y))$
4	3	biimpd	$⊢ (P \in ℙ \land (x \in ℤ \land y \in ℤ)) \to (P ∥ x y \to (P ∥ x \lor P ∥ y))$
5	4	ralrimivva	$⊢ P \in ℙ \to \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))$
6	1 5	jca	$⊢ P \in ℙ \to (P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y)))$
7		simpl	$⊢ (P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to P \in ℤ_{\geq 2}$
8		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
9	8	adantr	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P \in ℕ$
10	9	nnzd	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P \in ℤ$
11		iddvds	$⊢ P \in ℤ \to P ∥ P$
12	10 11	syl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P ∥ P$
13		nncn	$⊢ P \in ℕ \to P \in ℂ$
14	9 13	syl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P \in ℂ$
15		nncn	$⊢ z \in ℕ \to z \in ℂ$
16	15	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to z \in ℂ$
17		nnne0	$⊢ z \in ℕ \to z \neq 0$
18	17	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to z \neq 0$
19	14 16 18	divcan1d	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (\frac{P}{z}) z = P$
20	12 19	breqtrrd	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P ∥ (\frac{P}{z}) z$
21	20	adantr	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to P ∥ (\frac{P}{z}) z$
22		simprr	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to z ∥ P$
23		simprl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to z \in ℕ$
24		nndivdvds	$⊢ (P \in ℕ \land z \in ℕ) \to (z ∥ P \leftrightarrow \frac{P}{z} \in ℕ)$
25	9 23 24	syl2anc	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (z ∥ P \leftrightarrow \frac{P}{z} \in ℕ)$
26	22 25	mpbid	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to \frac{P}{z} \in ℕ$
27	26	nnzd	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to \frac{P}{z} \in ℤ$
28		nnz	$⊢ z \in ℕ \to z \in ℤ$
29	28	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to z \in ℤ$
30	27 29	jca	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (\frac{P}{z} \in ℤ \land z \in ℤ)$
31		oveq1	$⊢ x = \frac{P}{z} \to x y = (\frac{P}{z}) y$
32	31	breq2d	$⊢ x = \frac{P}{z} \to (P ∥ x y \leftrightarrow P ∥ (\frac{P}{z}) y)$
33		breq2	$⊢ x = \frac{P}{z} \to (P ∥ x \leftrightarrow P ∥ (\frac{P}{z}))$
34	33	orbi1d	$⊢ x = \frac{P}{z} \to ((P ∥ x \lor P ∥ y) \leftrightarrow (P ∥ (\frac{P}{z}) \lor P ∥ y))$
35	32 34	imbi12d	$⊢ x = \frac{P}{z} \to ((P ∥ x y \to (P ∥ x \lor P ∥ y)) \leftrightarrow (P ∥ (\frac{P}{z}) y \to (P ∥ (\frac{P}{z}) \lor P ∥ y)))$
36		oveq2	$⊢ y = z \to (\frac{P}{z}) y = (\frac{P}{z}) z$
37	36	breq2d	$⊢ y = z \to (P ∥ (\frac{P}{z}) y \leftrightarrow P ∥ (\frac{P}{z}) z)$
38		breq2	$⊢ y = z \to (P ∥ y \leftrightarrow P ∥ z)$
39	38	orbi2d	$⊢ y = z \to ((P ∥ (\frac{P}{z}) \lor P ∥ y) \leftrightarrow (P ∥ (\frac{P}{z}) \lor P ∥ z))$
40	37 39	imbi12d	$⊢ y = z \to ((P ∥ (\frac{P}{z}) y \to (P ∥ (\frac{P}{z}) \lor P ∥ y)) \leftrightarrow (P ∥ (\frac{P}{z}) z \to (P ∥ (\frac{P}{z}) \lor P ∥ z)))$
41	35 40	rspc2va	$⊢ ((\frac{P}{z} \in ℤ \land z \in ℤ) \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to (P ∥ (\frac{P}{z}) z \to (P ∥ (\frac{P}{z}) \lor P ∥ z))$
42	30 41	sylan	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to (P ∥ (\frac{P}{z}) z \to (P ∥ (\frac{P}{z}) \lor P ∥ z))$
43	21 42	mpd	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to (P ∥ (\frac{P}{z}) \lor P ∥ z)$
44		dvdsle	$⊢ (P \in ℤ \land \frac{P}{z} \in ℕ) \to (P ∥ (\frac{P}{z}) \to P \leq \frac{P}{z})$
45	10 26 44	syl2anc	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (P ∥ (\frac{P}{z}) \to P \leq \frac{P}{z})$
46	14	div1d	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to \frac{P}{1} = P$
47	46	breq1d	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (\frac{P}{1} \leq \frac{P}{z} \leftrightarrow P \leq \frac{P}{z})$
48	45 47	sylibrd	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (P ∥ (\frac{P}{z}) \to \frac{P}{1} \leq \frac{P}{z})$
49		nnrp	$⊢ z \in ℕ \to z \in ℝ^{+}$
50	49	rpregt0d	$⊢ z \in ℕ \to (z \in ℝ \land 0 < z)$
51	50	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (z \in ℝ \land 0 < z)$
52		1rp	$⊢ 1 \in ℝ^{+}$
53		rpregt0	$⊢ 1 \in ℝ^{+} \to (1 \in ℝ \land 0 < 1)$
54	52 53	mp1i	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (1 \in ℝ \land 0 < 1)$
55		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
56	9 55	syl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P \in ℝ^{+}$
57	56	rpregt0d	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (P \in ℝ \land 0 < P)$
58		lediv2	$⊢ ((z \in ℝ \land 0 < z) \land (1 \in ℝ \land 0 < 1) \land (P \in ℝ \land 0 < P)) \to (z \leq 1 \leftrightarrow \frac{P}{1} \leq \frac{P}{z})$
59	51 54 57 58	syl3anc	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (z \leq 1 \leftrightarrow \frac{P}{1} \leq \frac{P}{z})$
60	48 59	sylibrd	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (P ∥ (\frac{P}{z}) \to z \leq 1)$
61		nnle1eq1	$⊢ z \in ℕ \to (z \leq 1 \leftrightarrow z = 1)$
62	61	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (z \leq 1 \leftrightarrow z = 1)$
63	60 62	sylibd	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (P ∥ (\frac{P}{z}) \to z = 1)$
64		nnnn0	$⊢ z \in ℕ \to z \in ℕ_{0}$
65	64	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to z \in ℕ_{0}$
66	65	adantr	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land P ∥ z) \to z \in ℕ_{0}$
67		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
68	9 67	syl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to P \in ℕ_{0}$
69	68	adantr	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land P ∥ z) \to P \in ℕ_{0}$
70		simplrr	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land P ∥ z) \to z ∥ P$
71		simpr	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land P ∥ z) \to P ∥ z$
72		dvdseq	$⊢ ((z \in ℕ_{0} \land P \in ℕ_{0}) \land (z ∥ P \land P ∥ z)) \to z = P$
73	66 69 70 71 72	syl22anc	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land P ∥ z) \to z = P$
74	73	ex	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to (P ∥ z \to z = P)$
75	63 74	orim12d	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \to ((P ∥ (\frac{P}{z}) \lor P ∥ z) \to (z = 1 \lor z = P))$
76	75	imp	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land (P ∥ (\frac{P}{z}) \lor P ∥ z)) \to (z = 1 \lor z = P)$
77	43 76	syldan	$⊢ ((P \in ℤ_{\geq 2} \land (z \in ℕ \land z ∥ P)) \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to (z = 1 \lor z = P)$
78	77	an32s	$⊢ ((P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \land (z \in ℕ \land z ∥ P)) \to (z = 1 \lor z = P)$
79	78	expr	$⊢ ((P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \land z \in ℕ) \to (z ∥ P \to (z = 1 \lor z = P))$
80	79	ralrimiva	$⊢ (P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P))$
81		isprm2	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$
82	7 80 81	sylanbrc	$⊢ (P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y))) \to P \in ℙ$
83	6 82	impbii	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (P ∥ x y \to (P ∥ x \lor P ∥ y)))$

Metamath Proof Explorer

Theorem isprm6

Proof