Step
*
1
of Lemma
prime_elim
1. p : ℤ
2. prime(p)
3. ¬(p = 0 ∈ ℤ)
4. ¬(p ~ 1)
5. ¬reducible(p)
6. a : ℤ
7. a | p
⊢ (a ~ 1) ∨ (a ~ p)
BY
{ (% Rather unfortunate that exists is soft abstraction.
If order of rewrite rules is reversed, we get ands
rewritten by not_over_exists! %
((Unfold `reducible` 5 THENM RWW "not_over_and not_over_exists dneg_elim_a" 5) THENA Auto)) }
1
1. p : ℤ
2. prime(p)
3. ¬(p = 0 ∈ ℤ)
4. ¬(p ~ 1)
5. ∀b,c:ℤ-o. ((b ~ 1) ∨ (c ~ 1) ∨ (¬(p = (b * c) ∈ ℤ)))
6. a : ℤ
7. a | p
⊢ (a ~ 1) ∨ (a ~ p)
Latex:
Latex:
1. p : \mBbbZ{}
2. prime(p)
3. \mneg{}(p = 0)
4. \mneg{}(p \msim{} 1)
5. \mneg{}reducible(p)
6. a : \mBbbZ{}
7. a | p
\mvdash{} (a \msim{} 1) \mvee{} (a \msim{} p)
By
Latex:
(\% Rather unfortunate that exists is soft abstraction.
If order of rewrite rules is reversed, we get ands
rewritten by not\_over\_exists! \%
((Unfold `reducible` 5 THENM RWW "not\_over\_and not\_over\_exists dneg\_elim\_a" 5) THENA Auto))
Home
Index