---

Step * 2 1 1 1 of Lemma equipollent-int_mod

.....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
BY
{ (BLemma `modulus-equal-iff-eqmod` THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  m  :  \mBbbN{}\msupplus{}
2.  \mforall{}x:\mBbbZ{}\_m.  (x  mod  m  \mmember{}  \mBbbN{}m)
3.  istype(\mBbbZ{})
4.  \mforall{}x,y:\mBbbZ{}.    istype(x  \mequiv{}  y  mod  m)
5.  \mforall{}x:\mBbbZ{}.  (x  \mequiv{}  x  mod  m)
6.  a  :  Base
7.  b  :  Base
8.  c  :  a  =  b
9.  a  \mmember{}  \mBbbZ{}
10.  b  \mmember{}  \mBbbZ{}
11.  a  \mequiv{}  b  mod  m
12.  istype(\mBbbZ{})
13.  \mforall{}x,y:\mBbbZ{}.    istype(x  \mequiv{}  y  mod  m)
14.  \mforall{}x:\mBbbZ{}.  (x  \mequiv{}  x  mod  m)
15.  a3  :  Base
16.  b1  :  Base
17.  c1  :  a3  =  b1
18.  a3  \mmember{}  \mBbbZ{}
19.  b1  \mmember{}  \mBbbZ{}
20.  a3  \mequiv{}  b1  mod  m
21.  (a  mod  m)  =  (a3  mod  m)
\mvdash{}  a  \mequiv{}  a3  mod  m


By

---

Latex:
(BLemma  `modulus-equal-iff-eqmod`  THEN  Auto)

---

Home Index