Metamath Proof Explorer

Theorem ppiublem1

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

Ref Expression
Hypotheses ppiublem1.1 ⊢N≤6∧P∈ℙ∧4≤P→Pmod6∈N…5→Pmod6∈15
ppiublem1.2 ⊢M∈ℕ0
ppiublem1.3 ⊢N=M+1
ppiublem1.4 ⊢2∥M∨3∥M∨M∈15
Assertion ppiublem1 ⊢M≤6∧P∈ℙ∧4≤P→Pmod6∈M…5→Pmod6∈15

Proof

Step Hyp Ref Expression
1 ppiublem1.1 ⊢N≤6∧P∈ℙ∧4≤P→Pmod6∈N…5→Pmod6∈15
2 ppiublem1.2 ⊢M∈ℕ0
3 ppiublem1.3 ⊢N=M+1
4 ppiublem1.4 ⊢2∥M∨3∥M∨M∈15
5 1 simpli ⊢N≤6
6 df-6 ⊢6=5+1
7 5 3 6 3brtr3i ⊢M+1≤5+1
8 2 nn0rei ⊢M∈ℝ
9 5re ⊢5∈ℝ
10 1re ⊢1∈ℝ
11 8 9 10 leadd1i ⊢M≤5↔M+1≤5+1
12 7 11 mpbir ⊢M≤5
13 6re ⊢6∈ℝ
14 5lt6 ⊢5<6
15 9 13 14 ltleii ⊢5≤6
16 8 9 13 letri ⊢M≤5∧5≤6→M≤6
17 12 15 16 mp2an ⊢M≤6
18 2 nn0zi ⊢M∈ℤ
19 5nn ⊢5∈ℕ
20 19 nnzi ⊢5∈ℤ
21 eluz2 ⊢5∈ℤ≥M↔M∈ℤ∧5∈ℤ∧M≤5
22 18 20 12 21 mpbir3an ⊢5∈ℤ≥M
23 elfzp12 ⊢5∈ℤ≥M→Pmod6∈M…5↔Pmod6=M∨Pmod6∈M+1…5
24 22 23 ax-mp ⊢Pmod6∈M…5↔Pmod6=M∨Pmod6∈M+1…5
25 2nn ⊢2∈ℕ
26 6nn ⊢6∈ℕ
27 prmz ⊢P∈ℙ→P∈ℤ
28 27 adantr ⊢P∈ℙ∧4≤P→P∈ℤ
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∈ℕ∧P∈ℤ∧2∥6→2∥Pmod6↔2∥P
36 34 35 mpan2 ⊢2∈ℕ∧6∈ℕ∧P∈ℤ→2∥Pmod6↔2∥P
37 25 26 28 36 mp3an12i ⊢P∈ℙ∧4≤P→2∥Pmod6↔2∥P
38 uzid ⊢2∈ℤ→2∈ℤ≥2
39 30 38 ax-mp ⊢2∈ℤ≥2
40 simpl ⊢P∈ℙ∧4≤P→P∈ℙ
41 dvdsprm ⊢2∈ℤ≥2∧P∈ℙ→2∥P↔2=P
42 39 40 41 sylancr ⊢P∈ℙ∧4≤P→2∥P↔2=P
43 37 42 bitrd ⊢P∈ℙ∧4≤P→2∥Pmod6↔2=P
44 simpr ⊢P∈ℙ∧4≤P→4≤P
45 breq2 ⊢2=P→4≤2↔4≤P
46 44 45 syl5ibrcom ⊢P∈ℙ∧4≤P→2=P→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→Pmod6∈15
53 46 52 syl6 ⊢P∈ℙ∧4≤P→2=P→Pmod6∈15
54 43 53 sylbid ⊢P∈ℙ∧4≤P→2∥Pmod6→Pmod6∈15
55 breq2 ⊢Pmod6=M→2∥Pmod6↔2∥M
56 55 imbi1d ⊢Pmod6=M→2∥Pmod6→Pmod6∈15↔2∥M→Pmod6∈15
57 54 56 syl5ibcom ⊢P∈ℙ∧4≤P→Pmod6=M→2∥M→Pmod6∈15
58 57 com3r ⊢2∥M→P∈ℙ∧4≤P→Pmod6=M→Pmod6∈15
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∈ℕ∧P∈ℤ∧3∥6→3∥Pmod6↔3∥P
64 62 63 mpan2 ⊢3∈ℕ∧6∈ℕ∧P∈ℤ→3∥Pmod6↔3∥P
65 59 26 28 64 mp3an12i ⊢P∈ℙ∧4≤P→3∥Pmod6↔3∥P
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∧P∈ℙ→3∥P↔3=P
71 69 40 70 sylancr ⊢P∈ℙ∧4≤P→3∥P↔3=P
72 65 71 bitrd ⊢P∈ℙ∧4≤P→3∥Pmod6↔3=P
73 breq2 ⊢3=P→4≤3↔4≤P
74 44 73 syl5ibrcom ⊢P∈ℙ∧4≤P→3=P→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→Pmod6∈15
80 74 79 syl6 ⊢P∈ℙ∧4≤P→3=P→Pmod6∈15
81 72 80 sylbid ⊢P∈ℙ∧4≤P→3∥Pmod6→Pmod6∈15
82 breq2 ⊢Pmod6=M→3∥Pmod6↔3∥M
83 82 imbi1d ⊢Pmod6=M→3∥Pmod6→Pmod6∈15↔3∥M→Pmod6∈15
84 81 83 syl5ibcom ⊢P∈ℙ∧4≤P→Pmod6=M→3∥M→Pmod6∈15
85 84 com3r ⊢3∥M→P∈ℙ∧4≤P→Pmod6=M→Pmod6∈15
86 eleq1a ⊢M∈15→Pmod6=M→Pmod6∈15
87 86 a1d ⊢M∈15→P∈ℙ∧4≤P→Pmod6=M→Pmod6∈15
88 58 85 87 3jaoi ⊢2∥M∨3∥M∨M∈15→P∈ℙ∧4≤P→Pmod6=M→Pmod6∈15
89 4 88 ax-mp ⊢P∈ℙ∧4≤P→Pmod6=M→Pmod6∈15
90 3 oveq1i ⊢N…5=M+1…5
91 90 eleq2i ⊢Pmod6∈N…5↔Pmod6∈M+1…5
92 1 simpri ⊢P∈ℙ∧4≤P→Pmod6∈N…5→Pmod6∈15
93 91 92 biimtrrid ⊢P∈ℙ∧4≤P→Pmod6∈M+1…5→Pmod6∈15
94 89 93 jaod ⊢P∈ℙ∧4≤P→Pmod6=M∨Pmod6∈M+1…5→Pmod6∈15
95 24 94 biimtrid ⊢P∈ℙ∧4≤P→Pmod6∈M…5→Pmod6∈15
96 17 95 pm3.2i ⊢M≤6∧P∈ℙ∧4≤P→Pmod6∈M…5→Pmod6∈15