Step
*
3
of Lemma
div_anti_sym2
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
4. ¬(0 ≤ a)
5. 0 ≤ b
⊢ ((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ
BY
{ (InstLemma `div_2_to_1` [⌜a⌝;⌜b⌝]⋅ THEN Auto) }
1
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
4. ¬(0 ≤ a)
5. 0 ≤ b
6. (a ÷ b) = (-((-a) ÷ b)) ∈ ℤ
⊢ ((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ
Latex:
Latex:
1. a : \mBbbZ{}
2. b : \mBbbZ{}\msupminus{}\msupzero{}
3. -b \mneq{} 0
4. \mneg{}(0 \mleq{} a)
5. 0 \mleq{} b
\mvdash{} ((-a) \mdiv{} b) = (-(a \mdiv{} b))
By
Latex:
(InstLemma `div\_2\_to\_1` [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index