---

Step * 1 2 2 of Lemma princ_ideal_wf


1. r : Rng
2. a : |r|
3. b1 : |r|
4. 0 = (a * b1) ∈ |r|
5. a@0 : |r|@i
6. b : |r|@i
7. a@0 = (a * b) ∈ |r|
⊢ ∃b:|r|. ((-r a@0) = (a * b) ∈ |r|)
BY
{ TACTIC:(With ⌜-r b⌝ (D 0)⋅ THEN Auto THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  a  :  |r|
3.  b1  :  |r|
4.  0  =  (a  *  b1)
5.  a@0  :  |r|@i
6.  b  :  |r|@i
7.  a@0  =  (a  *  b)
\mvdash{}  \mexists{}b:|r|.  ((-r  a@0)  =  (a  *  b))


By

---

Latex:
TACTIC:(With  \mkleeneopen{}-r  b\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index