---

Step * 1 2 1 of Lemma primality-test

.....assertion..... 
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)
⊢ ∃a,c:{2..b-}. (b = (a * c) ∈ ℤ)
BY
{ xxx(D -1
      THEN RenameVar `a' (-2)
      THEN ExRepD
      THEN (InstLemma `absval_assoced` [⌜a⌝]⋅ THEN Auto)
      THEN InstLemma `absval_assoced` [⌜c⌝]⋅
      THEN Auto
      THEN ((Assert ¬(|a| ~ 1) BY
                   OnMaybeHyp 7 (\h. (ParallelOp h THEN RelRST THEN Auto)))
            THEN RWO "assoced_nelim" (-1)
            THEN Auto)
      THEN (Assert ¬(|c| ~ 1) BY
                  OnMaybeHyp 7 (\h. (ParallelOp h THEN RelRST THEN Auto)))
      THEN RWO "assoced_nelim" (-1)
      THEN Auto
      THEN (Assert ¬(|a| = 0 ∈ ℤ) BY
                  (CaseNat 0 `a' THEN Auto THEN (RWO "absval_ifthenelse" 0 THENA Auto) THEN SplitOnConclITE THEN Auto'))
      THEN (Assert ¬(|c| = 0 ∈ ℤ) BY
                  (CaseNat 0 `a' THEN Auto THEN (RWO "absval_ifthenelse" 0 THENA Auto) THEN SplitOnConclITE THEN Auto'))
      THEN (Assert (a * c) = (|a| * |c|) ∈ ℤ BY
                  ((RWO "absval_ifthenelse" 0 THENA Auto)
                   THEN RepeatFor 2 ((SplitOnConclITE THEN Auto'))
                   THEN Try (Complete ((InstLemma `mul_preserves_lt` [⌜a⌝;⌜0⌝;⌜c⌝]⋅ THEN Auto')⋅))
                   THEN Try (Complete ((InstLemma `mul_preserves_lt` [⌜c⌝;⌜0⌝;⌜a⌝]⋅ THEN Auto')⋅))))
      THEN InstConcl [⌜|a|⌝;⌜|c|⌝]⋅
      THEN Auto
      THEN Auto'
      THEN SupposeNot
      THEN Try ((InstLemma `mul_preserves_lt` [⌜1⌝;⌜|c|⌝;⌜|a|⌝]⋅ THEN Complete (Auto')))
      THEN Try ((InstLemma `mul_preserves_lt` [⌜1⌝;⌜|a|⌝;⌜|c|⌝]⋅ THEN Complete (Auto'))))xxx }

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  \mexists{}a,c:\{2..b\msupminus{}\}.  (b  =  (a  *  c))


By

---

Latex:
xxx(D  -1
        THEN  RenameVar  `a'  (-2)
        THEN  ExRepD
        THEN  (InstLemma  `absval\_assoced`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto)
        THEN  InstLemma  `absval\_assoced`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  ((Assert  \mneg{}(|a|  \msim{}  1)  BY
                                  OnMaybeHyp  7  (\mbackslash{}h.  (ParallelOp  h  THEN  RelRST  THEN  Auto)))
                    THEN  RWO  "assoced\_nelim"  (-1)
                    THEN  Auto)
        THEN  (Assert  \mneg{}(|c|  \msim{}  1)  BY
                                OnMaybeHyp  7  (\mbackslash{}h.  (ParallelOp  h  THEN  RelRST  THEN  Auto)))
        THEN  RWO  "assoced\_nelim"  (-1)
        THEN  Auto
        THEN  (Assert  \mneg{}(|a|  =  0)  BY
                                (CaseNat  0  `a'
                                  THEN  Auto
                                  THEN  (RWO  "absval\_ifthenelse"  0  THENA  Auto)
                                  THEN  SplitOnConclITE
                                  THEN  Auto'))
        THEN  (Assert  \mneg{}(|c|  =  0)  BY
                                (CaseNat  0  `a'
                                  THEN  Auto
                                  THEN  (RWO  "absval\_ifthenelse"  0  THENA  Auto)
                                  THEN  SplitOnConclITE
                                  THEN  Auto'))
        THEN  (Assert  (a  *  c)  =  (|a|  *  |c|)  BY
                                ((RWO  "absval\_ifthenelse"  0  THENA  Auto)
                                  THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto'))
                                  THEN  Try  (Complete  ((InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{}))
                                  THEN  Try  (Complete  ((InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{}))))
        THEN  InstConcl  [\mkleeneopen{}|a|\mkleeneclose{};\mkleeneopen{}|c|\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  Auto'
        THEN  SupposeNot
        THEN  Try  ((InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}|c|\mkleeneclose{};\mkleeneopen{}|a|\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto')))
        THEN  Try  ((InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}|a|\mkleeneclose{};\mkleeneopen{}|c|\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto'))))xxx

---

Home Index