Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ppiublem2 Structured version   Visualization version   GIF version

Theorem ppiublem2 25148
 Description: A prime greater than 3 does not divide 2 or 3, so its residue mod 6 is 1 or 5. (Contributed by Mario Carneiro, 12-Mar-2014.)
Assertion
Ref Expression
ppiublem2 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → (𝑃 mod 6) ∈ {1, 5})

Proof of Theorem ppiublem2
StepHypRef Expression
1 prmz 15595 . . . . 5 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
21adantr 466 . . . 4 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → 𝑃 ∈ ℤ)
3 6nn 11390 . . . 4 6 ∈ ℕ
4 zmodfz 12899 . . . 4 ((𝑃 ∈ ℤ ∧ 6 ∈ ℕ) → (𝑃 mod 6) ∈ (0...(6 − 1)))
52, 3, 4sylancl 566 . . 3 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → (𝑃 mod 6) ∈ (0...(6 − 1)))
6 df-6 11284 . . . . . 6 6 = (5 + 1)
76oveq1i 6802 . . . . 5 (6 − 1) = ((5 + 1) − 1)
8 5cn 11301 . . . . . 6 5 ∈ ℂ
9 ax-1cn 10195 . . . . . 6 1 ∈ ℂ
108, 9pncan3oi 10498 . . . . 5 ((5 + 1) − 1) = 5
117, 10eqtri 2792 . . . 4 (6 − 1) = 5
1211oveq2i 6803 . . 3 (0...(6 − 1)) = (0...5)
135, 12syl6eleq 2859 . 2 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → (𝑃 mod 6) ∈ (0...5))
14 6re 11302 . . . . . . . . . . 11 6 ∈ ℝ
1514leidi 10763 . . . . . . . . . 10 6 ≤ 6
16 noel 4065 . . . . . . . . . . . . 13 ¬ (𝑃 mod 6) ∈ ∅
1716pm2.21i 117 . . . . . . . . . . . 12 ((𝑃 mod 6) ∈ ∅ → (𝑃 mod 6) ∈ {1, 5})
18 5lt6 11405 . . . . . . . . . . . . 13 5 < 6
193nnzi 11602 . . . . . . . . . . . . . 14 6 ∈ ℤ
20 5nn 11389 . . . . . . . . . . . . . . 15 5 ∈ ℕ
2120nnzi 11602 . . . . . . . . . . . . . 14 5 ∈ ℤ
22 fzn 12563 . . . . . . . . . . . . . 14 ((6 ∈ ℤ ∧ 5 ∈ ℤ) → (5 < 6 ↔ (6...5) = ∅))
2319, 21, 22mp2an 664 . . . . . . . . . . . . 13 (5 < 6 ↔ (6...5) = ∅)
2418, 23mpbi 220 . . . . . . . . . . . 12 (6...5) = ∅
2517, 24eleq2s 2867 . . . . . . . . . . 11 ((𝑃 mod 6) ∈ (6...5) → (𝑃 mod 6) ∈ {1, 5})
2625a1i 11 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (6...5) → (𝑃 mod 6) ∈ {1, 5}))
2715, 26pm3.2i 447 . . . . . . . . 9 (6 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (6...5) → (𝑃 mod 6) ∈ {1, 5})))
28 5nn0 11513 . . . . . . . . 9 5 ∈ ℕ0
2920elexi 3362 . . . . . . . . . . 11 5 ∈ V
3029prid2 4432 . . . . . . . . . 10 5 ∈ {1, 5}
31303mix3i 1418 . . . . . . . . 9 (2 ∥ 5 ∨ 3 ∥ 5 ∨ 5 ∈ {1, 5})
3227, 28, 6, 31ppiublem1 25147 . . . . . . . 8 (5 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (5...5) → (𝑃 mod 6) ∈ {1, 5})))
33 4nn0 11512 . . . . . . . 8 4 ∈ ℕ0
34 df-5 11283 . . . . . . . 8 5 = (4 + 1)
35 2z 11610 . . . . . . . . . . 11 2 ∈ ℤ
36 dvdsmul1 15211 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (2 · 2))
3735, 35, 36mp2an 664 . . . . . . . . . 10 2 ∥ (2 · 2)
38 2t2e4 11378 . . . . . . . . . 10 (2 · 2) = 4
3937, 38breqtri 4809 . . . . . . . . 9 2 ∥ 4
40393mix1i 1416 . . . . . . . 8 (2 ∥ 4 ∨ 3 ∥ 4 ∨ 4 ∈ {1, 5})
4132, 33, 34, 40ppiublem1 25147 . . . . . . 7 (4 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (4...5) → (𝑃 mod 6) ∈ {1, 5})))
42 3nn0 11511 . . . . . . 7 3 ∈ ℕ0
43 df-4 11282 . . . . . . 7 4 = (3 + 1)
44 3z 11611 . . . . . . . . 9 3 ∈ ℤ
45 iddvds 15203 . . . . . . . . 9 (3 ∈ ℤ → 3 ∥ 3)
4644, 45ax-mp 5 . . . . . . . 8 3 ∥ 3
47463mix2i 1417 . . . . . . 7 (2 ∥ 3 ∨ 3 ∥ 3 ∨ 3 ∈ {1, 5})
4841, 42, 43, 47ppiublem1 25147 . . . . . 6 (3 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (3...5) → (𝑃 mod 6) ∈ {1, 5})))
49 2nn0 11510 . . . . . 6 2 ∈ ℕ0
50 df-3 11281 . . . . . 6 3 = (2 + 1)
51 iddvds 15203 . . . . . . . 8 (2 ∈ ℤ → 2 ∥ 2)
5235, 51ax-mp 5 . . . . . . 7 2 ∥ 2
53523mix1i 1416 . . . . . 6 (2 ∥ 2 ∨ 3 ∥ 2 ∨ 2 ∈ {1, 5})
5448, 49, 50, 53ppiublem1 25147 . . . . 5 (2 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (2...5) → (𝑃 mod 6) ∈ {1, 5})))
55 1nn0 11509 . . . . 5 1 ∈ ℕ0
56 df-2 11280 . . . . 5 2 = (1 + 1)
57 1ex 10236 . . . . . . 7 1 ∈ V
5857prid1 4431 . . . . . 6 1 ∈ {1, 5}
59583mix3i 1418 . . . . 5 (2 ∥ 1 ∨ 3 ∥ 1 ∨ 1 ∈ {1, 5})
6054, 55, 56, 59ppiublem1 25147 . . . 4 (1 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (1...5) → (𝑃 mod 6) ∈ {1, 5})))
61 0nn0 11508 . . . 4 0 ∈ ℕ0
62 1e0p1 11753 . . . 4 1 = (0 + 1)
63 dvds0 15205 . . . . . 6 (2 ∈ ℤ → 2 ∥ 0)
6435, 63ax-mp 5 . . . . 5 2 ∥ 0
65643mix1i 1416 . . . 4 (2 ∥ 0 ∨ 3 ∥ 0 ∨ 0 ∈ {1, 5})
6660, 61, 62, 65ppiublem1 25147 . . 3 (0 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (0...5) → (𝑃 mod 6) ∈ {1, 5})))
6766simpri 473 . 2 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) ∈ (0...5) → (𝑃 mod 6) ∈ {1, 5}))
6813, 67mpd 15 1 ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → (𝑃 mod 6) ∈ {1, 5})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1630   ∈ wcel 2144  ∅c0 4061  {cpr 4316   class class class wbr 4784  (class class class)co 6792  0cc0 10137  1c1 10138   + caddc 10140   · cmul 10142   < clt 10275   ≤ cle 10276   − cmin 10467  ℕcn 11221  2c2 11271  3c3 11272  4c4 11273  5c5 11274  6c6 11275  ℤcz 11578  ...cfz 12532   mod cmo 12875   ∥ cdvds 15188  ℙcprime 15591 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214  ax-pre-sup 10215 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-2o 7713  df-er 7895  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-sup 8503  df-inf 8504  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-3 11281  df-4 11282  df-5 11283  df-6 11284  df-n0 11494  df-z 11579  df-uz 11888  df-rp 12035  df-fz 12533  df-fl 12800  df-mod 12876  df-seq 13008  df-exp 13067  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-dvds 15189  df-prm 15592 This theorem is referenced by:  ppiub  25149
 Copyright terms: Public domain W3C validator