isprm5

Description: One need only check prime divisors of P up to sqrt P in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014)

		Ref	Expression
	Assertion	isprm5	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P))$

Proof

Step	Hyp	Ref	Expression
1		isprm4	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℤ_{\geq 2} (z ∥ P \to z = P))$
2		prmuz2	$⊢ z \in ℙ \to z \in ℤ_{\geq 2}$
3	2	a1i	$⊢ P \in ℤ_{\geq 2} \to (z \in ℙ \to z \in ℤ_{\geq 2})$
4		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
5		eluzelre	$⊢ P \in ℤ_{\geq 2} \to P \in ℝ$
6		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
7	6	nngt0d	$⊢ P \in ℤ_{\geq 2} \to 0 < P$
8		ltmulgt11	$⊢ (P \in ℝ \land P \in ℝ \land 0 < P) \to (1 < P \leftrightarrow P < P P)$
9	5 5 7 8	syl3anc	$⊢ P \in ℤ_{\geq 2} \to (1 < P \leftrightarrow P < P P)$
10	4 9	mpbid	$⊢ P \in ℤ_{\geq 2} \to P < P P$
11	5 5	remulcld	$⊢ P \in ℤ_{\geq 2} \to P P \in ℝ$
12	5 11	ltnled	$⊢ P \in ℤ_{\geq 2} \to (P < P P \leftrightarrow \neg P P \leq P)$
13	10 12	mpbid	$⊢ P \in ℤ_{\geq 2} \to \neg P P \leq P$
14		oveq12	$⊢ (z = P \land z = P) \to z z = P P$
15	14	anidms	$⊢ z = P \to z z = P P$
16	15	breq1d	$⊢ z = P \to (z z \leq P \leftrightarrow P P \leq P)$
17	16	notbid	$⊢ z = P \to (\neg z z \leq P \leftrightarrow \neg P P \leq P)$
18	13 17	syl5ibrcom	$⊢ P \in ℤ_{\geq 2} \to (z = P \to \neg z z \leq P)$
19	18	imim2d	$⊢ P \in ℤ_{\geq 2} \to ((z ∥ P \to z = P) \to (z ∥ P \to \neg z z \leq P))$
20		con2	$⊢ (z ∥ P \to \neg z z \leq P) \to (z z \leq P \to \neg z ∥ P)$
21	19 20	syl6	$⊢ P \in ℤ_{\geq 2} \to ((z ∥ P \to z = P) \to (z z \leq P \to \neg z ∥ P))$
22	3 21	imim12d	$⊢ P \in ℤ_{\geq 2} \to ((z \in ℤ_{\geq 2} \to (z ∥ P \to z = P)) \to (z \in ℙ \to (z z \leq P \to \neg z ∥ P)))$
23	22	ralimdv2	$⊢ P \in ℤ_{\geq 2} \to (\forall z \in ℤ_{\geq 2} (z ∥ P \to z = P) \to \forall z \in ℙ (z z \leq P \to \neg z ∥ P))$
24		annim	$⊢ (z ∥ P \land \neg z = P) \leftrightarrow \neg (z ∥ P \to z = P)$
25		oveq12	$⊢ (x = z \land x = z) \to x x = z z$
26	25	anidms	$⊢ x = z \to x x = z z$
27	26	breq1d	$⊢ x = z \to (x x \leq P \leftrightarrow z z \leq P)$
28		breq1	$⊢ x = z \to (x ∥ P \leftrightarrow z ∥ P)$
29	27 28	anbi12d	$⊢ x = z \to ((x x \leq P \land x ∥ P) \leftrightarrow (z z \leq P \land z ∥ P))$
30	29	rspcev	$⊢ (z \in ℤ_{\geq 2} \land (z z \leq P \land z ∥ P)) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P)$
31	30	ancom2s	$⊢ (z \in ℤ_{\geq 2} \land (z ∥ P \land z z \leq P)) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P)$
32	31	expr	$⊢ (z \in ℤ_{\geq 2} \land z ∥ P) \to (z z \leq P \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P))$
33	32	ad2ant2lr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (z z \leq P \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P))$
34		simprl	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z ∥ P$
35		eluzelz	$⊢ z \in ℤ_{\geq 2} \to z \in ℤ$
36	35	ad2antlr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \in ℤ$
37		eluz2nn	$⊢ z \in ℤ_{\geq 2} \to z \in ℕ$
38	37	ad2antlr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \in ℕ$
39	38	nnne0d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \neq 0$
40		eluzelz	$⊢ P \in ℤ_{\geq 2} \to P \in ℤ$
41	40	ad2antrr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P \in ℤ$
42		dvdsval2	$⊢ (z \in ℤ \land z \neq 0 \land P \in ℤ) \to (z ∥ P \leftrightarrow \frac{P}{z} \in ℤ)$
43	36 39 41 42	syl3anc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (z ∥ P \leftrightarrow \frac{P}{z} \in ℤ)$
44	34 43	mpbid	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to \frac{P}{z} \in ℤ$
45		eluzelre	$⊢ z \in ℤ_{\geq 2} \to z \in ℝ$
46	45	ad2antlr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \in ℝ$
47	46	recnd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \in ℂ$
48	47	mulid2d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to 1 z = z$
49	5	ad2antrr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P \in ℝ$
50	6	ad2antrr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P \in ℕ$
51		dvdsle	$⊢ (z \in ℤ \land P \in ℕ) \to (z ∥ P \to z \leq P)$
52	51	imp	$⊢ ((z \in ℤ \land P \in ℕ) \land z ∥ P) \to z \leq P$
53	36 50 34 52	syl21anc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \leq P$
54		simprr	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to \neg z = P$
55	54	neqned	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z \neq P$
56	55	necomd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P \neq z$
57	46 49 53 56	leneltd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z < P$
58	48 57	eqbrtrd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to 1 z < P$
59		1red	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to 1 \in ℝ$
60	41	zred	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P \in ℝ$
61		nnre	$⊢ z \in ℕ \to z \in ℝ$
62		nngt0	$⊢ z \in ℕ \to 0 < z$
63	61 62	jca	$⊢ z \in ℕ \to (z \in ℝ \land 0 < z)$
64	38 63	syl	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (z \in ℝ \land 0 < z)$
65		ltmuldiv	$⊢ (1 \in ℝ \land P \in ℝ \land (z \in ℝ \land 0 < z)) \to (1 z < P \leftrightarrow 1 < \frac{P}{z})$
66	59 60 64 65	syl3anc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (1 z < P \leftrightarrow 1 < \frac{P}{z})$
67	58 66	mpbid	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to 1 < \frac{P}{z}$
68		eluz2b1	$⊢ \frac{P}{z} \in ℤ_{\geq 2} \leftrightarrow (\frac{P}{z} \in ℤ \land 1 < \frac{P}{z})$
69	44 67 68	sylanbrc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to \frac{P}{z} \in ℤ_{\geq 2}$
70	46 46	remulcld	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z z \in ℝ$
71	38 38	nnmulcld	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z z \in ℕ$
72		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
73		nnrp	$⊢ z z \in ℕ \to z z \in ℝ^{+}$
74		rpdivcl	$⊢ (P \in ℝ^{+} \land z z \in ℝ^{+}) \to \frac{P}{z z} \in ℝ^{+}$
75	72 73 74	syl2an	$⊢ (P \in ℕ \land z z \in ℕ) \to \frac{P}{z z} \in ℝ^{+}$
76	50 71 75	syl2anc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to \frac{P}{z z} \in ℝ^{+}$
77	49 70 76	lemul1d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (P \leq z z \leftrightarrow P (\frac{P}{z z}) \leq z z (\frac{P}{z z}))$
78	49	recnd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P \in ℂ$
79	78 47 78 47 39 39	divmuldivd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (\frac{P}{z}) (\frac{P}{z}) = \frac{P P}{z z}$
80	71	nncnd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z z \in ℂ$
81	71	nnne0d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z z \neq 0$
82	78 78 80 81	divassd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to \frac{P P}{z z} = P (\frac{P}{z z})$
83	79 82	eqtrd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (\frac{P}{z}) (\frac{P}{z}) = P (\frac{P}{z z})$
84	78 80 81	divcan2d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z z (\frac{P}{z z}) = P$
85	84	eqcomd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to P = z z (\frac{P}{z z})$
86	83 85	breq12d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to ((\frac{P}{z}) (\frac{P}{z}) \leq P \leftrightarrow P (\frac{P}{z z}) \leq z z (\frac{P}{z z}))$
87	77 86	bitr4d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (P \leq z z \leftrightarrow (\frac{P}{z}) (\frac{P}{z}) \leq P)$
88	87	biimpd	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (P \leq z z \to (\frac{P}{z}) (\frac{P}{z}) \leq P)$
89	78 47 39	divcan2d	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to z (\frac{P}{z}) = P$
90		dvds0lem	$⊢ ((z \in ℤ \land \frac{P}{z} \in ℤ \land P \in ℤ) \land z (\frac{P}{z}) = P) \to (\frac{P}{z}) ∥ P$
91	36 44 41 89 90	syl31anc	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (\frac{P}{z}) ∥ P$
92	88 91	jctird	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (P \leq z z \to ((\frac{P}{z}) (\frac{P}{z}) \leq P \land (\frac{P}{z}) ∥ P))$
93		oveq12	$⊢ (x = \frac{P}{z} \land x = \frac{P}{z}) \to x x = (\frac{P}{z}) (\frac{P}{z})$
94	93	anidms	$⊢ x = \frac{P}{z} \to x x = (\frac{P}{z}) (\frac{P}{z})$
95	94	breq1d	$⊢ x = \frac{P}{z} \to (x x \leq P \leftrightarrow (\frac{P}{z}) (\frac{P}{z}) \leq P)$
96		breq1	$⊢ x = \frac{P}{z} \to (x ∥ P \leftrightarrow (\frac{P}{z}) ∥ P)$
97	95 96	anbi12d	$⊢ x = \frac{P}{z} \to ((x x \leq P \land x ∥ P) \leftrightarrow ((\frac{P}{z}) (\frac{P}{z}) \leq P \land (\frac{P}{z}) ∥ P))$
98	97	rspcev	$⊢ (\frac{P}{z} \in ℤ_{\geq 2} \land ((\frac{P}{z}) (\frac{P}{z}) \leq P \land (\frac{P}{z}) ∥ P)) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P)$
99	69 92 98	syl6an	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (P \leq z z \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P))$
100	70 49	letrid	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to (z z \leq P \lor P \leq z z)$
101	33 99 100	mpjaod	$⊢ ((P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land (z ∥ P \land \neg z = P)) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P)$
102	101	ex	$⊢ (P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((z ∥ P \land \neg z = P) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P))$
103	24 102	syl5bir	$⊢ (P \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (\neg (z ∥ P \to z = P) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P))$
104	103	rexlimdva	$⊢ P \in ℤ_{\geq 2} \to (\exists z \in ℤ_{\geq 2} \neg (z ∥ P \to z = P) \to \exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P))$
105		prmz	$⊢ z \in ℙ \to z \in ℤ$
106	105	ad2antrl	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z \in ℤ$
107	106	zred	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z \in ℝ$
108	107 107	remulcld	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z z \in ℝ$
109		eluzelz	$⊢ x \in ℤ_{\geq 2} \to x \in ℤ$
110	109	ad3antlr	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to x \in ℤ$
111	110	zred	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to x \in ℝ$
112	111 111	remulcld	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to x x \in ℝ$
113	40	ad3antrrr	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to P \in ℤ$
114	113	zred	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to P \in ℝ$
115		eluz2nn	$⊢ x \in ℤ_{\geq 2} \to x \in ℕ$
116	115	ad3antlr	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to x \in ℕ$
117		simprr	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z ∥ x$
118		dvdsle	$⊢ (z \in ℤ \land x \in ℕ) \to (z ∥ x \to z \leq x)$
119	118	imp	$⊢ ((z \in ℤ \land x \in ℕ) \land z ∥ x) \to z \leq x$
120	106 116 117 119	syl21anc	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z \leq x$
121		eluzge2nn0	$⊢ z \in ℤ_{\geq 2} \to z \in ℕ_{0}$
122	121	nn0ge0d	$⊢ z \in ℤ_{\geq 2} \to 0 \leq z$
123	2 122	syl	$⊢ z \in ℙ \to 0 \leq z$
124	123	ad2antrl	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to 0 \leq z$
125		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
126	125	nn0ge0d	$⊢ x \in ℕ \to 0 \leq x$
127	116 126	syl	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to 0 \leq x$
128		le2msq	$⊢ ((z \in ℝ \land 0 \leq z) \land (x \in ℝ \land 0 \leq x)) \to (z \leq x \leftrightarrow z z \leq x x)$
129	107 124 111 127 128	syl22anc	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to (z \leq x \leftrightarrow z z \leq x x)$
130	120 129	mpbid	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z z \leq x x$
131		simplrl	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to x x \leq P$
132	108 112 114 130 131	letrd	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z z \leq P$
133		simplrr	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to x ∥ P$
134	106 110 113 117 133	dvdstrd	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to z ∥ P$
135	132 134	jc	$⊢ (((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \land (z \in ℙ \land z ∥ x)) \to \neg (z z \leq P \to \neg z ∥ P)$
136		exprmfct	$⊢ x \in ℤ_{\geq 2} \to \exists z \in ℙ z ∥ x$
137	136	ad2antlr	$⊢ ((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \to \exists z \in ℙ z ∥ x$
138	135 137	reximddv	$⊢ ((P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \land (x x \leq P \land x ∥ P)) \to \exists z \in ℙ \neg (z z \leq P \to \neg z ∥ P)$
139	138	ex	$⊢ (P \in ℤ_{\geq 2} \land x \in ℤ_{\geq 2}) \to ((x x \leq P \land x ∥ P) \to \exists z \in ℙ \neg (z z \leq P \to \neg z ∥ P))$
140	139	rexlimdva	$⊢ P \in ℤ_{\geq 2} \to (\exists x \in ℤ_{\geq 2} (x x \leq P \land x ∥ P) \to \exists z \in ℙ \neg (z z \leq P \to \neg z ∥ P))$
141	104 140	syld	$⊢ P \in ℤ_{\geq 2} \to (\exists z \in ℤ_{\geq 2} \neg (z ∥ P \to z = P) \to \exists z \in ℙ \neg (z z \leq P \to \neg z ∥ P))$
142		rexnal	$⊢ \exists z \in ℤ_{\geq 2} \neg (z ∥ P \to z = P) \leftrightarrow \neg \forall z \in ℤ_{\geq 2} (z ∥ P \to z = P)$
143		rexnal	$⊢ \exists z \in ℙ \neg (z z \leq P \to \neg z ∥ P) \leftrightarrow \neg \forall z \in ℙ (z z \leq P \to \neg z ∥ P)$
144	141 142 143	3imtr3g	$⊢ P \in ℤ_{\geq 2} \to (\neg \forall z \in ℤ_{\geq 2} (z ∥ P \to z = P) \to \neg \forall z \in ℙ (z z \leq P \to \neg z ∥ P))$
145	23 144	impcon4bid	$⊢ P \in ℤ_{\geq 2} \to (\forall z \in ℤ_{\geq 2} (z ∥ P \to z = P) \leftrightarrow \forall z \in ℙ (z z \leq P \to \neg z ∥ P))$
146		prmnn	$⊢ z \in ℙ \to z \in ℕ$
147	146	nncnd	$⊢ z \in ℙ \to z \in ℂ$
148	147	sqvald	$⊢ z \in ℙ \to z^{2} = z z$
149	148	breq1d	$⊢ z \in ℙ \to (z^{2} \leq P \leftrightarrow z z \leq P)$
150	149	imbi1d	$⊢ z \in ℙ \to ((z^{2} \leq P \to \neg z ∥ P) \leftrightarrow (z z \leq P \to \neg z ∥ P))$
151	150	ralbiia	$⊢ \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P) \leftrightarrow \forall z \in ℙ (z z \leq P \to \neg z ∥ P)$
152	145 151	bitr4di	$⊢ P \in ℤ_{\geq 2} \to (\forall z \in ℤ_{\geq 2} (z ∥ P \to z = P) \leftrightarrow \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P))$
153	152	pm5.32i	$⊢ (P \in ℤ_{\geq 2} \land \forall z \in ℤ_{\geq 2} (z ∥ P \to z = P)) \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P))$
154	1 153	bitri	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℙ (z^{2} \leq P \to \neg z ∥ P))$

Metamath Proof Explorer

Theorem isprm5

Proof