Theorem ppiublem1

Description: Lemma for ppiub . (Contributed by Mario Carneiro, 12-Mar-2014)

	Ref	Expression
Hypotheses	ppiublem1.1	⊢ ( 𝑁 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑁 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) )
	ppiublem1.2	⊢ 𝑀 ∈ ℕ0
	ppiublem1.3	⊢ 𝑁 = ( 𝑀 + 1 )
	ppiublem1.4	⊢ ( 2 ∥ 𝑀 ∨ 3 ∥ 𝑀 ∨ 𝑀 ∈ { 1 , 5 } )
Assertion	ppiublem1	⊢ ( 𝑀 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) )

Proof

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