Step
*
2
1
2
1
1
of Lemma
small-eqmod
1. m : ℕ+
2. a : ℤ
3. ¬(0 ≤ a)
4. 0 ≥ (a rem m)
5. (a rem m) > (-m)
6. ¬(((-2) * (a rem m)) ≤ m)
7. (2 * |(a rem m) + m|) ≤ m
8. (2 * |(a rem m) + m|) ≤ m
⊢ (a + m) ≡ a mod m
BY
{ ((Assert (a + m) ≡ (a + 0) mod m BY (BLemma `add_functionality_wrt_eqmod` THEN Auto)) THEN Auto) }
Latex:
Latex:
1. m : \mBbbN{}\msupplus{}
2. a : \mBbbZ{}
3. \mneg{}(0 \mleq{} a)
4. 0 \mgeq{} (a rem m)
5. (a rem m) > (-m)
6. \mneg{}(((-2) * (a rem m)) \mleq{} m)
7. (2 * |(a rem m) + m|) \mleq{} m
8. (2 * |(a rem m) + m|) \mleq{} m
\mvdash{} (a + m) \mequiv{} a mod m
By
Latex:
((Assert (a + m) \mequiv{} (a + 0) mod m BY (BLemma `add\_functionality\_wrt\_eqmod` THEN Auto)) THEN Auto)
Home
Index