---

Step * 1 2 1 1 1 of Lemma chinese-remainder1


1. r : ℤ
2. s : ℤ
3. 1 | r
4. 1 | s
5. ∀z:ℤ. (((z | r) ∧ (z | s)) ⇒ (z | 1))
6. a : ℤ
7. b : ℤ
8. g : ℕ
9. a1 : ℤ
10. b1 : ℤ
11. x : ℤ
12. y : ℤ
13. r = (a1 * g) ∈ ℤ
14. s = (b1 * g) ∈ ℤ
15. ((x * a1) + (y * b1)) = 1 ∈ ℤ
16. ¬(g = 1 ∈ ℤ)
⊢ g | r
BY
{ (With ⌜a1⌝ (D 0)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  r  :  \mBbbZ{}
2.  s  :  \mBbbZ{}
3.  1  |  r
4.  1  |  s
5.  \mforall{}z:\mBbbZ{}.  (((z  |  r)  \mwedge{}  (z  |  s))  {}\mRightarrow{}  (z  |  1))
6.  a  :  \mBbbZ{}
7.  b  :  \mBbbZ{}
8.  g  :  \mBbbN{}
9.  a1  :  \mBbbZ{}
10.  b1  :  \mBbbZ{}
11.  x  :  \mBbbZ{}
12.  y  :  \mBbbZ{}
13.  r  =  (a1  *  g)
14.  s  =  (b1  *  g)
15.  ((x  *  a1)  +  (y  *  b1))  =  1
16.  \mneg{}(g  =  1)
\mvdash{}  g  |  r


By

---

Latex:
(With  \mkleeneopen{}a1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto')

---

Home Index