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 syl5bir ( ( 𝑃 ∈ ℙ ∧ 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 syl5bi ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) )
96 17 95 pm3.2i ( 𝑀 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) )