---

Step * 2 of Lemma prime_ideals_in_int_ring


1. i : ℕ+@i
2. prime(i)@i
⊢ ¬(∃c:ℤ. ((c * i) = 1 ∈ ℤ))
BY
{ (RepeatFor 2 (D -1) THEN ParallelOp -2) }

1
1. i : ℕ+@i
2. ¬(i = 0 ∈ ℤ)@i
3. ∀b,c:ℤ.  ((i | (b * c)) ⇒ ((i | b) ∨ (i | c)))@i
4. ∃c:ℤ. ((c * i) = 1 ∈ ℤ)@i
⊢ i ~ 1

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}\msupplus{}@i
2.  prime(i)@i
\mvdash{}  \mneg{}(\mexists{}c:\mBbbZ{}.  ((c  *  i)  =  1))


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  ParallelOp  -2)

---

Home Index