Metamath Proof Explorer

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 } ) ) )