Step * 1 2 1 1 of Lemma int_mod_ring_wf


1. : ℕ+
2. : ℤ_n
3. : ℤ_n
⊢ uiff((x mod n) (y mod n) ∈ ℤ;x y ∈ ℤ_n)
BY
(RWO "equal_int_mod_iff_modulus" THEN Try (Complete (Auto))) }

1
.....wf..... 
1. : ℕ+
2. : ℤ_n
3. : ℤ_n
4. y ∈ ℤ_n supposing y ∈ ℤ_n
⊢ istype((x mod n) (y mod n) ∈ ℤ)


Latex:


Latex:

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


By


Latex:
(RWO  "equal\_int\_mod\_iff\_modulus"  0  THEN  Try  (Complete  (Auto)))




Home Index