prmlem0

	Ref	Expression
Hypotheses	prmlem0.1	$⊢ (\neg 2 ∥ M \land x \in ℤ_{\geq M}) \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N)$
	prmlem0.2	$⊢ K \in ℙ \to \neg K ∥ N$
	prmlem0.3	$⊢ K + 2 = M$
Assertion	prmlem0	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N)$

Proof

Step	Hyp	Ref	Expression
1		prmlem0.1	$⊢ (\neg 2 ∥ M \land x \in ℤ_{\geq M}) \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N)$
2		prmlem0.2	$⊢ K \in ℙ \to \neg K ∥ N$
3		prmlem0.3	$⊢ K + 2 = M$
4		eldifi	$⊢ x \in (ℙ ∖ \{2\}) \to x \in ℙ$
5		eleq1	$⊢ x = K \to (x \in ℙ \leftrightarrow K \in ℙ)$
6		breq1	$⊢ x = K \to (x ∥ N \leftrightarrow K ∥ N)$
7	6	notbid	$⊢ x = K \to (\neg x ∥ N \leftrightarrow \neg K ∥ N)$
8	5 7	imbi12d	$⊢ x = K \to ((x \in ℙ \to \neg x ∥ N) \leftrightarrow (K \in ℙ \to \neg K ∥ N))$
9	2 8	mpbiri	$⊢ x = K \to (x \in ℙ \to \neg x ∥ N)$
10	4 9	syl5	$⊢ x = K \to (x \in (ℙ ∖ \{2\}) \to \neg x ∥ N)$
11	10	adantrd	$⊢ x = K \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N)$
12	11	a1i	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x = K \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
13		uzp1	$⊢ x \in ℤ_{\geq (K + 1)} \to (x = K + 1 \lor x \in ℤ_{\geq (K + 1 + 1)})$
14		eleq1	$⊢ x = K + 1 \to (x \in (ℙ ∖ \{2\}) \leftrightarrow K + 1 \in (ℙ ∖ \{2\}))$
15	14	adantl	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land x = K + 1) \to (x \in (ℙ ∖ \{2\}) \leftrightarrow K + 1 \in (ℙ ∖ \{2\}))$
16		eldifsn	$⊢ K + 1 \in (ℙ ∖ \{2\}) \leftrightarrow (K + 1 \in ℙ \land K + 1 \neq 2)$
17		eluzel2	$⊢ x \in ℤ_{\geq K} \to K \in ℤ$
18	17	adantl	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to K \in ℤ$
19		simpl	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to \neg 2 ∥ K$
20		1z	$⊢ 1 \in ℤ$
21		n2dvds1	$⊢ \neg 2 ∥ 1$
22		opoe	$⊢ ((K \in ℤ \land \neg 2 ∥ K) \land (1 \in ℤ \land \neg 2 ∥ 1)) \to 2 ∥ (K + 1)$
23	20 21 22	mpanr12	$⊢ (K \in ℤ \land \neg 2 ∥ K) \to 2 ∥ (K + 1)$
24	18 19 23	syl2anc	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to 2 ∥ (K + 1)$
25	24	adantr	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land K + 1 \in ℙ) \to 2 ∥ (K + 1)$
26		2z	$⊢ 2 \in ℤ$
27		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
28	26 27	mp1i	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to 2 \in ℤ_{\geq 2}$
29		dvdsprm	$⊢ (2 \in ℤ_{\geq 2} \land K + 1 \in ℙ) \to (2 ∥ (K + 1) \leftrightarrow 2 = K + 1)$
30	28 29	sylan	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land K + 1 \in ℙ) \to (2 ∥ (K + 1) \leftrightarrow 2 = K + 1)$
31	25 30	mpbid	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land K + 1 \in ℙ) \to 2 = K + 1$
32	31	eqcomd	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land K + 1 \in ℙ) \to K + 1 = 2$
33	32	a1d	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land K + 1 \in ℙ) \to (x ∥ N \to K + 1 = 2)$
34	33	necon3ad	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land K + 1 \in ℙ) \to (K + 1 \neq 2 \to \neg x ∥ N)$
35	34	expimpd	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to ((K + 1 \in ℙ \land K + 1 \neq 2) \to \neg x ∥ N)$
36	16 35	biimtrid	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (K + 1 \in (ℙ ∖ \{2\}) \to \neg x ∥ N)$
37	36	adantr	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land x = K + 1) \to (K + 1 \in (ℙ ∖ \{2\}) \to \neg x ∥ N)$
38	15 37	sylbid	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land x = K + 1) \to (x \in (ℙ ∖ \{2\}) \to \neg x ∥ N)$
39	38	adantrd	$⊢ ((\neg 2 ∥ K \land x \in ℤ_{\geq K}) \land x = K + 1) \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N)$
40	39	ex	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x = K + 1 \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
41	18	zcnd	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to K \in ℂ$
42		ax-1cn	$⊢ 1 \in ℂ$
43		addass	$⊢ (K \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to K + 1 + 1 = K + 1 + 1$
44	42 42 43	mp3an23	$⊢ K \in ℂ \to K + 1 + 1 = K + 1 + 1$
45	41 44	syl	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to K + 1 + 1 = K + 1 + 1$
46		1p1e2	$⊢ 1 + 1 = 2$
47	46	oveq2i	$⊢ K + 1 + 1 = K + 2$
48	47 3	eqtri	$⊢ K + 1 + 1 = M$
49	45 48	eqtrdi	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to K + 1 + 1 = M$
50	49	fveq2d	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to ℤ_{\geq (K + 1 + 1)} = ℤ_{\geq M}$
51	50	eleq2d	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x \in ℤ_{\geq (K + 1 + 1)} \leftrightarrow x \in ℤ_{\geq M})$
52		dvdsaddr	$⊢ (2 \in ℤ \land K \in ℤ) \to (2 ∥ K \leftrightarrow 2 ∥ (K + 2))$
53	26 18 52	sylancr	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (2 ∥ K \leftrightarrow 2 ∥ (K + 2))$
54	3	breq2i	$⊢ 2 ∥ (K + 2) \leftrightarrow 2 ∥ M$
55	53 54	bitrdi	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (2 ∥ K \leftrightarrow 2 ∥ M)$
56	19 55	mtbid	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to \neg 2 ∥ M$
57	1	ex	$⊢ \neg 2 ∥ M \to (x \in ℤ_{\geq M} \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
58	56 57	syl	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x \in ℤ_{\geq M} \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
59	51 58	sylbid	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x \in ℤ_{\geq (K + 1 + 1)} \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
60	40 59	jaod	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to ((x = K + 1 \lor x \in ℤ_{\geq (K + 1 + 1)}) \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
61	13 60	syl5	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x \in ℤ_{\geq (K + 1)} \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N))$
62		uzp1	$⊢ x \in ℤ_{\geq K} \to (x = K \lor x \in ℤ_{\geq (K + 1)})$
63	62	adantl	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to (x = K \lor x \in ℤ_{\geq (K + 1)})$
64	12 61 63	mpjaod	$⊢ (\neg 2 ∥ K \land x \in ℤ_{\geq K}) \to ((x \in (ℙ ∖ \{2\}) \land x^{2} \leq N) \to \neg x ∥ N)$

Metamath Proof Explorer

Theorem prmlem0

Proof