---

Step * 1 of Lemma princ_ideal_mem_cond


1. r : CRng
2. u : |r|
3. v : |r|
⊢ v | u in r ⇐⇒ ∃b:|r|. (u = (v * b) ∈ |r|)
BY
{ Unfold `ring_divs` 0  
THENM GenUnivCD THENA Auto }

1
1. r : CRng
2. u : |r|
3. v : |r|
4. ∃c:|r|. ((c * v) = u ∈ |r|)
⊢ ∃b:|r|. (u = (v * b) ∈ |r|)

2
1. r : CRng
2. u : |r|
3. v : |r|
4. ∃b:|r|. (u = (v * b) ∈ |r|)
⊢ ∃c:|r|. ((c * v) = u ∈ |r|)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  u  :  |r|
3.  v  :  |r|
\mvdash{}  v  |  u  in  r  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:|r|.  (u  =  (v  *  b))


By

---

Latex:
Unfold  `ring\_divs`  0   
THENM  GenUnivCD  THENA  Auto

---

Home Index