Step
*
1
1
of Lemma
assoced-prime
1. q : ℤ
2. ¬((-q) = 0 ∈ ℤ)
3. ¬((-q) ~ 1)
4. ∀b,c:ℤ. (((-q) | (b * c))
⇒ (((-q) | b) ∨ ((-q) | c)))
5. ¬(q = 0 ∈ ℤ)
⊢ ¬(q ~ 1)
BY
{ ParallelOp -3 }
1
1. q : ℤ
2. ¬((-q) = 0 ∈ ℤ)
3. ∀b,c:ℤ. (((-q) | (b * c))
⇒ (((-q) | b) ∨ ((-q) | c)))
4. ¬(q = 0 ∈ ℤ)
5. q ~ 1
⊢ (-q) ~ 1
Latex:
Latex:
1. q : \mBbbZ{}
2. \mneg{}((-q) = 0)
3. \mneg{}((-q) \msim{} 1)
4. \mforall{}b,c:\mBbbZ{}. (((-q) | (b * c)) {}\mRightarrow{} (((-q) | b) \mvee{} ((-q) | c)))
5. \mneg{}(q = 0)
\mvdash{} \mneg{}(q \msim{} 1)
By
Latex:
ParallelOp -3
Home
Index