---

Step * 1 2 2 1 of Lemma primality-test


1. b : ℕ
2. ∀b:ℕb. (prime(b)) supposing ((∀p:ℕ. (prime(p) ⇒ ((p * p) ≤ b) ⇒ (¬(p | b)))) and (2 ≤ b))
3. 2 ≤ b
4. ∀p:ℕ. (prime(p) ⇒ ((p * p) ≤ b) ⇒ (¬(p | b)))
5. ¬(b ~ 1)
6. reducible(b)
7. a : {2..b-}
8. c : {2..b-}
9. b = (a * c) ∈ ℤ
⊢ False
BY
{ xxx((Assert a | b BY
             (UnfoldTopAb 0 THEN InstConcl [⌜c⌝]⋅ THEN Auto))
      THEN (InstHyp [⌜a⌝] 2⋅
            THENA (Auto' THEN (Assert ¬(p | b) BY (BackThruSomeHyp THEN Auto)) THEN ParallelLast THEN RelRST THEN Auto)
            )
      )xxx }

1
1. b : ℕ
2. ∀b:ℕb. (prime(b)) supposing ((∀p:ℕ. (prime(p) ⇒ ((p * p) ≤ b) ⇒ (¬(p | b)))) and (2 ≤ b))
3. 2 ≤ b
4. ∀p:ℕ. (prime(p) ⇒ ((p * p) ≤ b) ⇒ (¬(p | b)))
5. ¬(b ~ 1)
6. reducible(b)
7. a : {2..b-}
8. c : {2..b-}
9. b = (a * c) ∈ ℤ
10. a | b
11. prime(a)
⊢ False

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}
2.  \mforall{}b:\mBbbN{}b.  (prime(b))  supposing  ((\mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  ((p  *  p)  \mleq{}  b)  {}\mRightarrow{}  (\mneg{}(p  |  b))))  and  (2  \mleq{}  b))
3.  2  \mleq{}  b
4.  \mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  ((p  *  p)  \mleq{}  b)  {}\mRightarrow{}  (\mneg{}(p  |  b)))
5.  \mneg{}(b  \msim{}  1)
6.  reducible(b)
7.  a  :  \{2..b\msupminus{}\}
8.  c  :  \{2..b\msupminus{}\}
9.  b  =  (a  *  c)
\mvdash{}  False


By

---

Latex:
xxx((Assert  a  |  b  BY
                      (UnfoldTopAb  0  THEN  InstConcl  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto))
        THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  2\mcdot{}
                    THENA  (Auto'
                                  THEN  (Assert  \mneg{}(p  |  b)  BY
                                                          (BackThruSomeHyp  THEN  Auto))
                                  THEN  ParallelLast
                                  THEN  RelRST
                                  THEN  Auto)
                    )
        )xxx

---

Home Index