---

Step * 1 of Lemma ideal_of_prime


1. r : CRng@i'
2. u : |r|@i
⊢ r-Prime(u) ⇐⇒ (¬((u)r 1)) ∧ (∀a,b:|r|.  (((u)r (a * b)) ⇒ (((u)r a) ∨ ((u)r b))))
BY
{ RWH (RevLemmaC `princ_ideal_mem_cond`) 0 
THENA Auto }

1
1. r : CRng@i'
2. u : |r|@i
⊢ r-Prime(u) ⇐⇒ (¬u | 1 in r) ∧ (∀a,b:|r|.  (u | a * b in r ⇒ (u | a in r ∨ u | b in r)))

---

Latex:

---

Latex:

1.  r  :  CRng@i'
2.  u  :  |r|@i
\mvdash{}  r-Prime(u)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}((u)r  1))  \mwedge{}  (\mforall{}a,b:|r|.    (((u)r  (a  *  b))  {}\mRightarrow{}  (((u)r  a)  \mvee{}  ((u)r  b))))


By

---

Latex:
RWH  (RevLemmaC  `princ\_ideal\_mem\_cond`)  0 
THENA  Auto

---

Home Index