Step
*
1
of Lemma
div_reduce_inequality
1. a : ℤ
⊢ (∀n:ℕ+. ∀x:ℤ. uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ n) + x)))
∧ (∀n:{...-1}. ∀x:ℤ. uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ (-n)) + ((-1) * x))))
BY
{ TACTIC:(BetterSplitAndConcl THEN (UnivCD THENA Auto)) }
1
1. a : ℤ
2. n : ℕ+
3. x : ℤ
⊢ uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ n) + x))
2
1. a : ℤ
2. ∀n:ℕ+. ∀x:ℤ. uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ n) + x))
3. n : {...-1}
4. x : ℤ
⊢ uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ (-n)) + ((-1) * x)))
Latex:
Latex:
1. a : \mBbbZ{}
\mvdash{} (\mforall{}n:\mBbbN{}\msupplus{}. \mforall{}x:\mBbbZ{}. uiff(0 \mleq{} (a + (n * x));0 \mleq{} ((a \mdiv{}\mdownarrow{} n) + x)))
\mwedge{} (\mforall{}n:\{...-1\}. \mforall{}x:\mBbbZ{}. uiff(0 \mleq{} (a + (n * x));0 \mleq{} ((a \mdiv{}\mdownarrow{} (-n)) + ((-1) * x))))
By
Latex:
TACTIC:(BetterSplitAndConcl THEN (UnivCD THENA Auto))
Home
Index