---

Step * 1 of Lemma equipollent-primes


1. m : ℕ@i
⊢ ∃p:ℕ. (prime(p) ∧ (m ≤ p))
BY
{ ((InstLemma `prime-factors` [⌜1 + (m)!⌝]⋅ THEN Auto')⋅
   THEN ExRepD
   THEN D -2
   THEN Reduce (-1)
   THEN Auto'
   THEN RenameVar `p' (-3)
   THEN With ⌜p⌝ (D 0)⋅
   THEN Auto
   THEN DVar `p'
   THEN Unhide
   THEN Auto)⋅ }

1
1. m : ℕ@i
2. p : {2...}
3. prime(p)
4. v : {m:{2...}| prime(m)}  List
5. (1 + (m)!) = Π([p / v])  ∈ ℤ
6. prime(p)
⊢ m ≤ p

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}@i
\mvdash{}  \mexists{}p:\mBbbN{}.  (prime(p)  \mwedge{}  (m  \mleq{}  p))


By

---

Latex:
((InstLemma  `prime-factors`  [\mkleeneopen{}1  +  (m)!\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{}
  THEN  ExRepD
  THEN  D  -2
  THEN  Reduce  (-1)
  THEN  Auto'
  THEN  RenameVar  `p'  (-3)
  THEN  With  \mkleeneopen{}p\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  DVar  `p'
  THEN  Unhide
  THEN  Auto)\mcdot{}

---

Home Index