isprm7

Description: One need only check prime divisors of P up to sqrt P in order to ensure primality. This version of isprm5 combines the primality and bound on z into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020)

		Ref	Expression
	Assertion	isprm7	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \neg z ∥ P)$

Proof

Step	Hyp	Ref	Expression
1		isprm5	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P))$
2		prmz	$⊢ z \in ℙ \to z \in ℤ$
3	2	zred	$⊢ z \in ℙ \to z \in ℝ$
4		0red	$⊢ z \in ℙ \to 0 \in ℝ$
5		1red	$⊢ z \in ℙ \to 1 \in ℝ$
6		0lt1	$⊢ 0 < 1$
7	6	a1i	$⊢ z \in ℙ \to 0 < 1$
8		prmgt1	$⊢ z \in ℙ \to 1 < z$
9	4 5 3 7 8	lttrd	$⊢ z \in ℙ \to 0 < z$
10	4 3 9	ltled	$⊢ z \in ℙ \to 0 \leq z$
11	3 10	jca	$⊢ z \in ℙ \to (z \in ℝ \land 0 \leq z)$
12		eluzelre	$⊢ P \in ℤ_{\geq 2} \to P \in ℝ$
13		0red	$⊢ P \in ℤ_{\geq 2} \to 0 \in ℝ$
14		2re	$⊢ 2 \in ℝ$
15	14	a1i	$⊢ P \in ℤ_{\geq 2} \to 2 \in ℝ$
16		0le2	$⊢ 0 \leq 2$
17	16	a1i	$⊢ P \in ℤ_{\geq 2} \to 0 \leq 2$
18		eluzle	$⊢ P \in ℤ_{\geq 2} \to 2 \leq P$
19	13 15 12 17 18	letrd	$⊢ P \in ℤ_{\geq 2} \to 0 \leq P$
20	12 19	jca	$⊢ P \in ℤ_{\geq 2} \to (P \in ℝ \land 0 \leq P)$
21		resqcl	$⊢ z \in ℝ \to z^{2} \in ℝ$
22		sqge0	$⊢ z \in ℝ \to 0 \leq z^{2}$
23	21 22	jca	$⊢ z \in ℝ \to (z^{2} \in ℝ \land 0 \leq z^{2})$
24	23	adantr	$⊢ (z \in ℝ \land 0 \leq z) \to (z^{2} \in ℝ \land 0 \leq z^{2})$
25		sqrtle	$⊢ ((z^{2} \in ℝ \land 0 \leq z^{2}) \land (P \in ℝ \land 0 \leq P)) \to (z^{2} \leq P \leftrightarrow \sqrt{z^{2}} \leq \sqrt{P})$
26	24 25	sylan	$⊢ ((z \in ℝ \land 0 \leq z) \land (P \in ℝ \land 0 \leq P)) \to (z^{2} \leq P \leftrightarrow \sqrt{z^{2}} \leq \sqrt{P})$
27		sqrtsq	$⊢ (z \in ℝ \land 0 \leq z) \to \sqrt{z^{2}} = z$
28	27	breq1d	$⊢ (z \in ℝ \land 0 \leq z) \to (\sqrt{z^{2}} \leq \sqrt{P} \leftrightarrow z \leq \sqrt{P})$
29	28	adantr	$⊢ ((z \in ℝ \land 0 \leq z) \land (P \in ℝ \land 0 \leq P)) \to (\sqrt{z^{2}} \leq \sqrt{P} \leftrightarrow z \leq \sqrt{P})$
30	26 29	bitrd	$⊢ ((z \in ℝ \land 0 \leq z) \land (P \in ℝ \land 0 \leq P)) \to (z^{2} \leq P \leftrightarrow z \leq \sqrt{P})$
31	11 20 30	syl2anr	$⊢ (P \in ℤ_{\geq 2} \land z \in ℙ) \to (z^{2} \leq P \leftrightarrow z \leq \sqrt{P})$
32	31	imbi1d	$⊢ (P \in ℤ_{\geq 2} \land z \in ℙ) \to ((z^{2} \leq P \to \neg z ∥ P) \leftrightarrow (z \leq \sqrt{P} \to \neg z ∥ P))$
33	32	ralbidva	$⊢ P \in ℤ_{\geq 2} \to (\forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P) \leftrightarrow \forall z \in ℙ (z \leq \sqrt{P} \to \neg z ∥ P))$
34	33	pm5.32i	$⊢ (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P)) \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z \leq \sqrt{P} \to \neg z ∥ P))$
35		impexp	$⊢ ((z \in ℙ \land z \leq \sqrt{P}) \to \neg z ∥ P) \leftrightarrow (z \in ℙ \to (z \leq \sqrt{P} \to \neg z ∥ P))$
36	12 19	resqrtcld	$⊢ P \in ℤ_{\geq 2} \to \sqrt{P} \in ℝ$
37	36	flcld	$⊢ P \in ℤ_{\geq 2} \to ⌊\sqrt{P}⌋ \in ℤ$
38	37 2	anim12i	$⊢ (P \in ℤ_{\geq 2} \land z \in ℙ) \to (⌊\sqrt{P}⌋ \in ℤ \land z \in ℤ)$
39	38	adantr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℙ) \land z \leq \sqrt{P}) \to (⌊\sqrt{P}⌋ \in ℤ \land z \in ℤ)$
40		prmuz2	$⊢ z \in ℙ \to z \in ℤ_{\geq 2}$
41		eluzle	$⊢ z \in ℤ_{\geq 2} \to 2 \leq z$
42	40 41	syl	$⊢ z \in ℙ \to 2 \leq z$
43	42	ad2antlr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℙ) \land z \leq \sqrt{P}) \to 2 \leq z$
44		flge	$⊢ (\sqrt{P} \in ℝ \land z \in ℤ) \to (z \leq \sqrt{P} \leftrightarrow z \leq ⌊\sqrt{P}⌋)$
45	36 2 44	syl2an	$⊢ (P \in ℤ_{\geq 2} \land z \in ℙ) \to (z \leq \sqrt{P} \leftrightarrow z \leq ⌊\sqrt{P}⌋)$
46	45	biimpa	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℙ) \land z \leq \sqrt{P}) \to z \leq ⌊\sqrt{P}⌋$
47		2z	$⊢ 2 \in ℤ$
48		elfz4	$⊢ ((2 \in ℤ \land ⌊\sqrt{P}⌋ \in ℤ \land z \in ℤ) \land (2 \leq z \land z \leq ⌊\sqrt{P}⌋)) \to z \in (2 \dots ⌊\sqrt{P}⌋)$
49	47 48	mp3anl1	$⊢ ((⌊\sqrt{P}⌋ \in ℤ \land z \in ℤ) \land (2 \leq z \land z \leq ⌊\sqrt{P}⌋)) \to z \in (2 \dots ⌊\sqrt{P}⌋)$
50	39 43 46 49	syl12anc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℙ) \land z \leq \sqrt{P}) \to z \in (2 \dots ⌊\sqrt{P}⌋)$
51	50	anasss	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℙ \land z \leq \sqrt{P})) \to z \in (2 \dots ⌊\sqrt{P}⌋)$
52		simprl	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℙ \land z \leq \sqrt{P})) \to z \in ℙ$
53	51 52	elind	$⊢ (P \in ℤ_{\geq 2} \land (z \in ℙ \land z \leq \sqrt{P})) \to z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ)$
54	53	ex	$⊢ P \in ℤ_{\geq 2} \to ((z \in ℙ \land z \leq \sqrt{P}) \to z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ))$
55		elin	$⊢ z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \leftrightarrow (z \in (2 \dots ⌊\sqrt{P}⌋) \land z \in ℙ)$
56		elfzelz	$⊢ z \in (2 \dots ⌊\sqrt{P}⌋) \to z \in ℤ$
57	56	zred	$⊢ z \in (2 \dots ⌊\sqrt{P}⌋) \to z \in ℝ$
58	57	adantl	$⊢ (P \in ℤ_{\geq 2} \land z \in (2 \dots ⌊\sqrt{P}⌋)) \to z \in ℝ$
59		reflcl	$⊢ \sqrt{P} \in ℝ \to ⌊\sqrt{P}⌋ \in ℝ$
60	36 59	syl	$⊢ P \in ℤ_{\geq 2} \to ⌊\sqrt{P}⌋ \in ℝ$
61	60	adantr	$⊢ (P \in ℤ_{\geq 2} \land z \in (2 \dots ⌊\sqrt{P}⌋)) \to ⌊\sqrt{P}⌋ \in ℝ$
62	36	adantr	$⊢ (P \in ℤ_{\geq 2} \land z \in (2 \dots ⌊\sqrt{P}⌋)) \to \sqrt{P} \in ℝ$
63		elfzle2	$⊢ z \in (2 \dots ⌊\sqrt{P}⌋) \to z \leq ⌊\sqrt{P}⌋$
64	63	adantl	$⊢ (P \in ℤ_{\geq 2} \land z \in (2 \dots ⌊\sqrt{P}⌋)) \to z \leq ⌊\sqrt{P}⌋$
65		flle	$⊢ \sqrt{P} \in ℝ \to ⌊\sqrt{P}⌋ \leq \sqrt{P}$
66	36 65	syl	$⊢ P \in ℤ_{\geq 2} \to ⌊\sqrt{P}⌋ \leq \sqrt{P}$
67	66	adantr	$⊢ (P \in ℤ_{\geq 2} \land z \in (2 \dots ⌊\sqrt{P}⌋)) \to ⌊\sqrt{P}⌋ \leq \sqrt{P}$
68	58 61 62 64 67	letrd	$⊢ (P \in ℤ_{\geq 2} \land z \in (2 \dots ⌊\sqrt{P}⌋)) \to z \leq \sqrt{P}$
69	68	ex	$⊢ P \in ℤ_{\geq 2} \to (z \in (2 \dots ⌊\sqrt{P}⌋) \to z \leq \sqrt{P})$
70	69	anim1d	$⊢ P \in ℤ_{\geq 2} \to ((z \in (2 \dots ⌊\sqrt{P}⌋) \land z \in ℙ) \to (z \leq \sqrt{P} \land z \in ℙ))$
71	55 70	biimtrid	$⊢ P \in ℤ_{\geq 2} \to (z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \to (z \leq \sqrt{P} \land z \in ℙ))$
72		ancom	$⊢ (z \leq \sqrt{P} \land z \in ℙ) \leftrightarrow (z \in ℙ \land z \leq \sqrt{P})$
73	71 72	imbitrdi	$⊢ P \in ℤ_{\geq 2} \to (z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \to (z \in ℙ \land z \leq \sqrt{P}))$
74	54 73	impbid	$⊢ P \in ℤ_{\geq 2} \to ((z \in ℙ \land z \leq \sqrt{P}) \leftrightarrow z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ))$
75	74	imbi1d	$⊢ P \in ℤ_{\geq 2} \to (((z \in ℙ \land z \leq \sqrt{P}) \to \neg z ∥ P) \leftrightarrow (z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \to \neg z ∥ P))$
76	35 75	bitr3id	$⊢ P \in ℤ_{\geq 2} \to ((z \in ℙ \to (z \leq \sqrt{P} \to \neg z ∥ P)) \leftrightarrow (z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \to \neg z ∥ P))$
77	76	ralbidv2	$⊢ P \in ℤ_{\geq 2} \to (\forall z \in ℙ (z \leq \sqrt{P} \to \neg z ∥ P) \leftrightarrow \forall z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \neg z ∥ P)$
78	77	pm5.32i	$⊢ (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z \leq \sqrt{P} \to \neg z ∥ P)) \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \neg z ∥ P)$
79	1 34 78	3bitri	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ((2 \dots ⌊\sqrt{P}⌋) \cap ℙ) \neg z ∥ P)$

Metamath Proof Explorer

Theorem isprm7

Proof