ppiublem1

	Ref	Expression
Hypotheses	ppiublem1.1	$⊢ (N \leq 6 \land ((P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (N \dots 5) \to P \mod 6 \in \{1, 5\})))$
	ppiublem1.2	$⊢ M \in ℕ_{0}$
	ppiublem1.3	$⊢ N = M + 1$
	ppiublem1.4	$⊢ (2 ∥ M \lor 3 ∥ M \lor M \in \{1, 5\})$
Assertion	ppiublem1	$⊢ (M \leq 6 \land ((P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (M \dots 5) \to P \mod 6 \in \{1, 5\})))$

Proof

Step	Hyp	Ref	Expression
1		ppiublem1.1	$⊢ (N \leq 6 \land ((P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (N \dots 5) \to P \mod 6 \in \{1, 5\})))$
2		ppiublem1.2	$⊢ M \in ℕ_{0}$
3		ppiublem1.3	$⊢ N = M + 1$
4		ppiublem1.4	$⊢ (2 ∥ M \lor 3 ∥ M \lor M \in \{1, 5\})$
5	1	simpli	$⊢ N \leq 6$
6		df-6	$⊢ 6 = 5 + 1$
7	5 3 6	3brtr3i	$⊢ M + 1 \leq 5 + 1$
8	2	nn0rei	$⊢ M \in ℝ$
9		5re	$⊢ 5 \in ℝ$
10		1re	$⊢ 1 \in ℝ$
11	8 9 10	leadd1i	$⊢ M \leq 5 \leftrightarrow M + 1 \leq 5 + 1$
12	7 11	mpbir	$⊢ M \leq 5$
13		6re	$⊢ 6 \in ℝ$
14		5lt6	$⊢ 5 < 6$
15	9 13 14	ltleii	$⊢ 5 \leq 6$
16	8 9 13	letri	$⊢ (M \leq 5 \land 5 \leq 6) \to M \leq 6$
17	12 15 16	mp2an	$⊢ M \leq 6$
18	2	nn0zi	$⊢ M \in ℤ$
19		5nn	$⊢ 5 \in ℕ$
20	19	nnzi	$⊢ 5 \in ℤ$
21		eluz2	$⊢ 5 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land 5 \in ℤ \land M \leq 5)$
22	18 20 12 21	mpbir3an	$⊢ 5 \in ℤ_{\geq M}$
23		elfzp12	$⊢ 5 \in ℤ_{\geq M} \to (P \mod 6 \in (M \dots 5) \leftrightarrow (P \mod 6 = M \lor P \mod 6 \in (M + 1 \dots 5)))$
24	22 23	ax-mp	$⊢ P \mod 6 \in (M \dots 5) \leftrightarrow (P \mod 6 = M \lor P \mod 6 \in (M + 1 \dots 5))$
25		2nn	$⊢ 2 \in ℕ$
26		6nn	$⊢ 6 \in ℕ$
27		prmz	$⊢ P \in ℙ \to P \in ℤ$
28	27	adantr	$⊢ (P \in ℙ \land 4 \leq P) \to P \in ℤ$
29		3z	$⊢ 3 \in ℤ$
30		2z	$⊢ 2 \in ℤ$
31		dvdsmul2	$⊢ (3 \in ℤ \land 2 \in ℤ) \to 2 ∥ 3 \cdot 2$
32	29 30 31	mp2an	$⊢ 2 ∥ 3 \cdot 2$
33		3t2e6	$⊢ 3 \cdot 2 = 6$
34	32 33	breqtri	$⊢ 2 ∥ 6$
35		dvdsmod	$⊢ ((2 \in ℕ \land 6 \in ℕ \land P \in ℤ) \land 2 ∥ 6) \to (2 ∥ (P \mod 6) \leftrightarrow 2 ∥ P)$
36	34 35	mpan2	$⊢ (2 \in ℕ \land 6 \in ℕ \land P \in ℤ) \to (2 ∥ (P \mod 6) \leftrightarrow 2 ∥ P)$
37	25 26 28 36	mp3an12i	$⊢ (P \in ℙ \land 4 \leq P) \to (2 ∥ (P \mod 6) \leftrightarrow 2 ∥ P)$
38		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
39	30 38	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
40		simpl	$⊢ (P \in ℙ \land 4 \leq P) \to P \in ℙ$
41		dvdsprm	$⊢ (2 \in ℤ_{\geq 2} \land P \in ℙ) \to (2 ∥ P \leftrightarrow 2 = P)$
42	39 40 41	sylancr	$⊢ (P \in ℙ \land 4 \leq P) \to (2 ∥ P \leftrightarrow 2 = P)$
43	37 42	bitrd	$⊢ (P \in ℙ \land 4 \leq P) \to (2 ∥ (P \mod 6) \leftrightarrow 2 = P)$
44		simpr	$⊢ (P \in ℙ \land 4 \leq P) \to 4 \leq P$
45		breq2	$⊢ 2 = P \to (4 \leq 2 \leftrightarrow 4 \leq P)$
46	44 45	syl5ibrcom	$⊢ (P \in ℙ \land 4 \leq P) \to (2 = P \to 4 \leq 2)$
47		2lt4	$⊢ 2 < 4$
48		2re	$⊢ 2 \in ℝ$
49		4re	$⊢ 4 \in ℝ$
50	48 49	ltnlei	$⊢ 2 < 4 \leftrightarrow \neg 4 \leq 2$
51	47 50	mpbi	$⊢ \neg 4 \leq 2$
52	51	pm2.21i	$⊢ 4 \leq 2 \to P \mod 6 \in \{1, 5\}$
53	46 52	syl6	$⊢ (P \in ℙ \land 4 \leq P) \to (2 = P \to P \mod 6 \in \{1, 5\})$
54	43 53	sylbid	$⊢ (P \in ℙ \land 4 \leq P) \to (2 ∥ (P \mod 6) \to P \mod 6 \in \{1, 5\})$
55		breq2	$⊢ P \mod 6 = M \to (2 ∥ (P \mod 6) \leftrightarrow 2 ∥ M)$
56	55	imbi1d	$⊢ P \mod 6 = M \to ((2 ∥ (P \mod 6) \to P \mod 6 \in \{1, 5\}) \leftrightarrow (2 ∥ M \to P \mod 6 \in \{1, 5\}))$
57	54 56	syl5ibcom	$⊢ (P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to (2 ∥ M \to P \mod 6 \in \{1, 5\}))$
58	57	com3r	$⊢ 2 ∥ M \to ((P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to P \mod 6 \in \{1, 5\}))$
59		3nn	$⊢ 3 \in ℕ$
60		dvdsmul1	$⊢ (3 \in ℤ \land 2 \in ℤ) \to 3 ∥ 3 \cdot 2$
61	29 30 60	mp2an	$⊢ 3 ∥ 3 \cdot 2$
62	61 33	breqtri	$⊢ 3 ∥ 6$
63		dvdsmod	$⊢ ((3 \in ℕ \land 6 \in ℕ \land P \in ℤ) \land 3 ∥ 6) \to (3 ∥ (P \mod 6) \leftrightarrow 3 ∥ P)$
64	62 63	mpan2	$⊢ (3 \in ℕ \land 6 \in ℕ \land P \in ℤ) \to (3 ∥ (P \mod 6) \leftrightarrow 3 ∥ P)$
65	59 26 28 64	mp3an12i	$⊢ (P \in ℙ \land 4 \leq P) \to (3 ∥ (P \mod 6) \leftrightarrow 3 ∥ P)$
66		df-3	$⊢ 3 = 2 + 1$
67		peano2uz	$⊢ 2 \in ℤ_{\geq 2} \to 2 + 1 \in ℤ_{\geq 2}$
68	39 67	ax-mp	$⊢ 2 + 1 \in ℤ_{\geq 2}$
69	66 68	eqeltri	$⊢ 3 \in ℤ_{\geq 2}$
70		dvdsprm	$⊢ (3 \in ℤ_{\geq 2} \land P \in ℙ) \to (3 ∥ P \leftrightarrow 3 = P)$
71	69 40 70	sylancr	$⊢ (P \in ℙ \land 4 \leq P) \to (3 ∥ P \leftrightarrow 3 = P)$
72	65 71	bitrd	$⊢ (P \in ℙ \land 4 \leq P) \to (3 ∥ (P \mod 6) \leftrightarrow 3 = P)$
73		breq2	$⊢ 3 = P \to (4 \leq 3 \leftrightarrow 4 \leq P)$
74	44 73	syl5ibrcom	$⊢ (P \in ℙ \land 4 \leq P) \to (3 = P \to 4 \leq 3)$
75		3lt4	$⊢ 3 < 4$
76		3re	$⊢ 3 \in ℝ$
77	76 49	ltnlei	$⊢ 3 < 4 \leftrightarrow \neg 4 \leq 3$
78	75 77	mpbi	$⊢ \neg 4 \leq 3$
79	78	pm2.21i	$⊢ 4 \leq 3 \to P \mod 6 \in \{1, 5\}$
80	74 79	syl6	$⊢ (P \in ℙ \land 4 \leq P) \to (3 = P \to P \mod 6 \in \{1, 5\})$
81	72 80	sylbid	$⊢ (P \in ℙ \land 4 \leq P) \to (3 ∥ (P \mod 6) \to P \mod 6 \in \{1, 5\})$
82		breq2	$⊢ P \mod 6 = M \to (3 ∥ (P \mod 6) \leftrightarrow 3 ∥ M)$
83	82	imbi1d	$⊢ P \mod 6 = M \to ((3 ∥ (P \mod 6) \to P \mod 6 \in \{1, 5\}) \leftrightarrow (3 ∥ M \to P \mod 6 \in \{1, 5\}))$
84	81 83	syl5ibcom	$⊢ (P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to (3 ∥ M \to P \mod 6 \in \{1, 5\}))$
85	84	com3r	$⊢ 3 ∥ M \to ((P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to P \mod 6 \in \{1, 5\}))$
86		eleq1a	$⊢ M \in \{1, 5\} \to (P \mod 6 = M \to P \mod 6 \in \{1, 5\})$
87	86	a1d	$⊢ M \in \{1, 5\} \to ((P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to P \mod 6 \in \{1, 5\}))$
88	58 85 87	3jaoi	$⊢ (2 ∥ M \lor 3 ∥ M \lor M \in \{1, 5\}) \to ((P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to P \mod 6 \in \{1, 5\}))$
89	4 88	ax-mp	$⊢ (P \in ℙ \land 4 \leq P) \to (P \mod 6 = M \to P \mod 6 \in \{1, 5\})$
90	3	oveq1i	$⊢ (N \dots 5) = (M + 1 \dots 5)$
91	90	eleq2i	$⊢ P \mod 6 \in (N \dots 5) \leftrightarrow P \mod 6 \in (M + 1 \dots 5)$
92	1	simpri	$⊢ (P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (N \dots 5) \to P \mod 6 \in \{1, 5\})$
93	91 92	syl5bir	$⊢ (P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (M + 1 \dots 5) \to P \mod 6 \in \{1, 5\})$
94	89 93	jaod	$⊢ (P \in ℙ \land 4 \leq P) \to ((P \mod 6 = M \lor P \mod 6 \in (M + 1 \dots 5)) \to P \mod 6 \in \{1, 5\})$
95	24 94	syl5bi	$⊢ (P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (M \dots 5) \to P \mod 6 \in \{1, 5\})$
96	17 95	pm3.2i	$⊢ (M \leq 6 \land ((P \in ℙ \land 4 \leq P) \to (P \mod 6 \in (M \dots 5) \to P \mod 6 \in \{1, 5\})))$

Metamath Proof Explorer

Theorem ppiublem1

Proof