Step
*
1
2
1
1
of Lemma
int_mod_ring_wf
1. n : ℕ+
2. x : ℤ_n
3. y : ℤ_n
⊢ uiff((x mod n) = (y mod n) ∈ ℤ;x = y ∈ ℤ_n)
BY
{ (RWO "equal_int_mod_iff_modulus" 0 THEN Try (Complete (Auto))) }
1
.....wf..... 
1. n : ℕ+
2. x : ℤ_n
3. y : ℤ_n
4. x = y ∈ ℤ_n supposing x = 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