---

Step * 1 1 of Lemma equipollent-primes


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
BY
{ (Thin (-1)
   THEN    (SupposeNot
            THEN (Assert p | (m)! BY
                        (BLemma `divides-fact` THEN Auto))
            THEN (Assert p | (1 + (m)!) BY
                        (With ⌜Π(v) ⌝ (D 0)⋅
                         THEN Auto
                         THEN HypSubst' (-3) 0
                         THEN Unfold `mul-list` 0
                         THEN Reduce 0
                         THEN Auto))
            THEN (Assert p | 1 BY
                        ((D (-2) THEN D -1) THEN With ⌜c1 - c⌝ (D 0)⋅ 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. ¬(m ≤ p)
7. p | (m)!
8. p | (1 + (m)!)
9. p | 1
⊢ m ≤ p

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}@i
2.  p  :  \{2...\}
3.  prime(p)
4.  v  :  \{m:\{2...\}|  prime(m)\}    List
5.  (1  +  (m)!)  =  \mPi{}([p  /  v]) 
6.  prime(p)
\mvdash{}  m  \mleq{}  p


By

---

Latex:
(Thin  (-1)
  THEN        (SupposeNot
                    THEN  (Assert  p  |  (m)!  BY
                                            (BLemma  `divides-fact`  THEN  Auto))
                    THEN  (Assert  p  |  (1  +  (m)!)  BY
                                            (With  \mkleeneopen{}\mPi{}(v)  \mkleeneclose{}  (D  0)\mcdot{}
                                              THEN  Auto
                                              THEN  HypSubst'  (-3)  0
                                              THEN  Unfold  `mul-list`  0
                                              THEN  Reduce  0
                                              THEN  Auto))
                    THEN  (Assert  p  |  1  BY
                                            ((D  (-2)  THEN  D  -1)  THEN  With  \mkleeneopen{}c1  -  c\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto')))\mcdot{}
  )

---

Home Index