---

Step * 1 2 2 1 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) ∈ ℤ
10. a | b
11. prime(a)
⊢ False
BY
{ ((Assert c | b BY
          (UnfoldTopAb 0 THEN InstConcl [⌜a⌝]⋅ THEN Auto))
   THEN (InstHyp [⌜c⌝] 2⋅
         THENA (Auto' THEN (Assert ¬(p | b) BY (BackThruSomeHyp THEN Auto)) THEN ParallelLast THEN RelRST THEN Auto)
         )
   )⋅ }

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)
12. c | b
13. prime(c)
⊢ 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)
10.  a  |  b
11.  prime(a)
\mvdash{}  False


By

---

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

---

Home Index