Step * 2 1 1 of Lemma equipollent-int_mod


1. : ℕ+
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. : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
3. istype(ℤ)
4. ∀x,y:ℤ.  istype(x ≡ mod m)
5. ∀x:ℤ(x ≡ mod m)
6. Base
7. Base
8. b ∈ (x,y:ℤ//(x ≡ mod m))
9. a ∈ ℤ
10. b ∈ ℤ
11. a ≡ mod m
12. istype(ℤ)
13. ∀x,y:ℤ.  istype(x ≡ mod m)
14. ∀x:ℤ(x ≡ mod m)
15. a3 Base
16. b1 Base
17. c1 a3 b1 ∈ (x,y:ℤ//(x ≡ 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