---

Step * of Lemma sq_stable__mprime

∀g:GrpSig. ((∀a,b:|g|.  Dec(a | b)) ⇒ (∀c:|g|. SqStable(IsPrime(c))))
BY
{ Unfolds ``mprime sq_stable`` 0 THEN Auto }

1
1. g : GrpSig@i'
2. ∀a,b:|g|.  Dec(a | b)@i
3. c : |g|@i
4. ↓(¬(g-unit(c))) ∧ (∀b,c@0:|g|.  ((c | (b * c@0)) ⇒ ((c | b) ∨ (c | c@0))))@i
5. ¬(g-unit(c))
6. b : |g|@i
7. c@0 : |g|@i
8. c | (b * c@0)@i
⊢ (c | b) ∨ (c | c@0)

---

Latex:

---

Latex:
\mforall{}g:GrpSig.  ((\mforall{}a,b:|g|.    Dec(a  |  b))  {}\mRightarrow{}  (\mforall{}c:|g|.  SqStable(IsPrime(c))))


By

---

Latex:
Unfolds  ``mprime  sq\_stable``  0  THEN  Auto

---

Home Index