Step
*
of Lemma
modulus_wf
∀[a:ℤ]. ∀[n:ℤ-o]. (a mod n ∈ ℕ)
BY
{ TACTIC:(ProveWfLemma THEN Assert ⌜-|n| < a rem n⌝⋅) }
1
.....assertion.....
1. a : ℤ
2. n : ℤ-o
3. a rem n ∈ ℤ
4. 0 ∈ ℤ
5. a rem n < 0
⊢ -|n| < a rem n
2
1. a : ℤ
2. n : ℤ-o
3. a rem n ∈ ℤ
4. 0 ∈ ℤ
5. a rem n < 0
6. -|n| < a rem n
⊢ |n| + (a rem n) ∈ ℕ
Latex:
Latex:
\mforall{}[a:\mBbbZ{}]. \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}]. (a mod n \mmember{} \mBbbN{})
By
Latex:
TACTIC:(ProveWfLemma THEN Assert \mkleeneopen{}-|n| < a rem n\mkleeneclose{}\mcdot{})
Home
Index