Step
*
1
1
of Lemma
not-pair-member-int
1. [a] : Base
2. [b] : Base
3. <a, b> ∈ ℤ
⊢ False
BY
{ (InstLemma `ispair-implies-not-isint` [⌜<a, b>⌝]⋅ THEN Auto) }
1
1. a : Base
2. b : Base
3. <a, b> ∈ ℤ
4. ¬↑isint(<a, b>)
⊢ False
Latex:
Latex:
1. [a] : Base
2. [b] : Base
3. <a, b> \mmember{} \mBbbZ{}
\mvdash{} False
By
Latex:
(InstLemma `ispair-implies-not-isint` [\mkleeneopen{}<a, b>\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index