Step * 1 1 1 2 of Lemma int-to-ring-mul


1. Rng
2. a1 : ℤ
3. a2 : ℤ
4. : ℤ
5. 0 < n
6. ∀x:ℤ(|x| <  (∀y:ℤ(int-to-ring(r;x y) (int-to-ring(r;x) int-to-ring(r;y)) ∈ |r|)))
7. : ℤ
8. |x| < n
9. : ℤ
10. ¬|x| < 1
11. (-(n 1)) ∈ ℤ
⊢ int-to-ring(r;(-(n 1)) y) (int-to-ring(r;-(n 1)) int-to-ring(r;y)) ∈ |r|
BY
(CaseNat `n'⋅ THEN Reduce 0) }

1
1. Rng
2. a1 : ℤ
3. a2 : ℤ
4. : ℤ
5. 0 < n
6. ∀x:ℤ(|x| <  (∀y:ℤ(int-to-ring(r;x y) (int-to-ring(r;x) int-to-ring(r;y)) ∈ |r|)))
7. : ℤ
8. |x| < n
9. : ℤ
10. ¬|x| < 1
11. (-(n 1)) ∈ ℤ
12. 1 ∈ ℤ
⊢ int-to-ring(r;(-0) y) (int-to-ring(r;-0) int-to-ring(r;y)) ∈ |r|

2
1. Rng
2. a1 : ℤ
3. a2 : ℤ
4. : ℤ
5. 0 < n
6. ∀x:ℤ(|x| <  (∀y:ℤ(int-to-ring(r;x y) (int-to-ring(r;x) int-to-ring(r;y)) ∈ |r|)))
7. : ℤ
8. |x| < n
9. : ℤ
10. ¬|x| < 1
11. (-(n 1)) ∈ ℤ
12. ¬(n 1 ∈ ℤ)
⊢ int-to-ring(r;(-(n 1)) y) (int-to-ring(r;-(n 1)) int-to-ring(r;y)) ∈ |r|


Latex:


Latex:

1.  r  :  Rng
2.  a1  :  \mBbbZ{}
3.  a2  :  \mBbbZ{}
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mforall{}x:\mBbbZ{}.  (|x|  <  n  -  1  {}\mRightarrow{}  (\mforall{}y:\mBbbZ{}.  (int-to-ring(r;x  *  y)  =  (int-to-ring(r;x)  *  int-to-ring(r;y)))))
7.  x  :  \mBbbZ{}
8.  |x|  <  n
9.  y  :  \mBbbZ{}
10.  \mneg{}|x|  <  n  -  1
11.  x  =  (-(n  -  1))
\mvdash{}  int-to-ring(r;(-(n  -  1))  *  y)  =  (int-to-ring(r;-(n  -  1))  *  int-to-ring(r;y))


By


Latex:
(CaseNat  1  `n'\mcdot{}  THEN  Reduce  0)




Home Index