---

Step * 1 1 1 1 1 2 1 of Lemma modulus-equal


1. x : ℤ
2. y : ℤ
3. m : ℕ+
4. a : ℤ
5. (x mod m) = a ∈ ℤ
6. b : ℤ
7. (y mod m) = b ∈ ℤ
8. 0 ≤ a
9. a < m
10. 0 ≤ b
11. b < m
12. c : ℤ
13. (x ÷↓ m) = c ∈ ℤ
14. d : ℤ
15. (y ÷↓ m) = d ∈ ℤ
16. m | (((c * m) + a) - (d * m) + b)
17. n : ℤ
18. (a - b) = (n * m) ∈ ℤ
⊢ a = b ∈ ℤ
BY
{ CaseNat 0 `n' }

1
1. x : ℤ
2. y : ℤ
3. m : ℕ+
4. a : ℤ
5. (x mod m) = a ∈ ℤ
6. b : ℤ
7. (y mod m) = b ∈ ℤ
8. 0 ≤ a
9. a < m
10. 0 ≤ b
11. b < m
12. c : ℤ
13. (x ÷↓ m) = c ∈ ℤ
14. d : ℤ
15. (y ÷↓ m) = d ∈ ℤ
16. m | (((c * m) + a) - (d * m) + b)
17. n : ℤ
18. (a - b) = (n * m) ∈ ℤ
19. n = 0 ∈ ℤ
⊢ a = b ∈ ℤ

2
1. x : ℤ
2. y : ℤ
3. m : ℕ+
4. a : ℤ
5. (x mod m) = a ∈ ℤ
6. b : ℤ
7. (y mod m) = b ∈ ℤ
8. 0 ≤ a
9. a < m
10. 0 ≤ b
11. b < m
12. c : ℤ
13. (x ÷↓ m) = c ∈ ℤ
14. d : ℤ
15. (y ÷↓ m) = d ∈ ℤ
16. m | (((c * m) + a) - (d * m) + b)
17. n : ℤ
18. (a - b) = (n * m) ∈ ℤ
19. ¬(n = 0 ∈ ℤ)
⊢ a = b ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  m  :  \mBbbN{}\msupplus{}
4.  a  :  \mBbbZ{}
5.  (x  mod  m)  =  a
6.  b  :  \mBbbZ{}
7.  (y  mod  m)  =  b
8.  0  \mleq{}  a
9.  a  <  m
10.  0  \mleq{}  b
11.  b  <  m
12.  c  :  \mBbbZ{}
13.  (x  \mdiv{}\mdownarrow{}  m)  =  c
14.  d  :  \mBbbZ{}
15.  (y  \mdiv{}\mdownarrow{}  m)  =  d
16.  m  |  (((c  *  m)  +  a)  -  (d  *  m)  +  b)
17.  n  :  \mBbbZ{}
18.  (a  -  b)  =  (n  *  m)
\mvdash{}  a  =  b


By

---

Latex:
CaseNat  0  `n'

---

Home Index