---

Step * 2 1 1 of Lemma equipollent-int_mod


1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
3. a1 : ℤ_m
4. a2 : ℤ_m
5. (a1 mod m) = (a2 mod m) ∈ ℕm
⊢ a1 = a2 ∈ ℤ_m
BY
{ ((newQuotD (-3) THENA (Auto THEN RelRST THEN Auto)) THEN (newQuotD (-2) THENA Auto) THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
3. istype(ℤ)
4. ∀x,y:ℤ.  istype(x ≡ y mod m)
5. ∀x:ℤ. (x ≡ x mod m)
6. a : Base
7. b : Base
8. c : a = b ∈ (x,y:ℤ//(x ≡ y mod m))
9. a ∈ ℤ
10. b ∈ ℤ
11. a ≡ b mod m
12. istype(ℤ)
13. ∀x,y:ℤ.  istype(x ≡ y mod m)
14. ∀x:ℤ. (x ≡ x mod m)
15. a3 : Base
16. b1 : Base
17. c1 : a3 = b1 ∈ (x,y:ℤ//(x ≡ y mod m))
18. a3 ∈ ℤ
19. b1 ∈ ℤ
20. a3 ≡ b1 mod m
21. (a mod m) = (a3 mod m) ∈ ℕm
⊢ a ≡ a3 mod m

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  \mforall{}x:\mBbbZ{}\_m.  (x  mod  m  \mmember{}  \mBbbN{}m)
3.  a1  :  \mBbbZ{}\_m
4.  a2  :  \mBbbZ{}\_m
5.  (a1  mod  m)  =  (a2  mod  m)
\mvdash{}  a1  =  a2


By

---

Latex:
((newQuotD  (-3)  THENA  (Auto  THEN  RelRST  THEN  Auto))
  THEN  (newQuotD  (-2)  THENA  Auto)
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index