---

Step * 1 of Lemma equal_int_mod_iff_modulus


1. n : ℕ+
2. x : ℤ_n
3. y : ℤ_n
4. (x mod n) = (y mod n) ∈ ℤ
⊢ x = y ∈ ℤ_n
BY
{ (MoveToConcl (-1) THEN UseWitness ⌜λz.Ax⌝⋅ THEN RepeatFor 2 (quotD 2) THEN (EqCD THENA Auto) THEN EqCD) }

1
.....eq aux..... 
1. n : ℕ+
2. x : ℤ
3. x1 : ℤ
4. x ≡ x1 mod n
5. y : ℤ
6. y1 : ℤ
7. y ≡ y1 mod n
8. z : (x mod n) = (y mod n) ∈ ℤ
⊢ x = y ∈ ℤ_n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbZ{}\_n
3.  y  :  \mBbbZ{}\_n
4.  (x  mod  n)  =  (y  mod  n)
\mvdash{}  x  =  y


By

---

Latex:
(MoveToConcl  (-1)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}z.Ax\mkleeneclose{}\mcdot{}
  THEN  RepeatFor  2  (quotD  2)
  THEN  (EqCD  THENA  Auto)
  THEN  EqCD)

---

Home Index