---

Step * 2 of Lemma coprime_functionality_wrt_eqmod


1. a : ℤ@i
2. a' : ℤ@i
3. m : ℤ@i
4. c : ℤ@i
5. (a' - a) = (m * c) ∈ ℤ@i
6. 1 | a@i
7. 1 | m@i
8. ∀z:ℤ. (((z | a) ∧ (z | m)) ⇒ (z | 1))@i
9. 1 | m
10. z : ℤ@i
11. z | a'@i
12. z | m@i
⊢ z | a
BY
{ (Subst' a = (a' + (m * (-c))) ∈ ℤ 0 THEN Auto') }

1
1. a : ℤ@i
2. a' : ℤ@i
3. m : ℤ@i
4. c : ℤ@i
5. (a' - a) = (m * c) ∈ ℤ@i
6. 1 | a@i
7. 1 | m@i
8. ∀z:ℤ. (((z | a) ∧ (z | m)) ⇒ (z | 1))@i
9. 1 | m
10. z : ℤ@i
11. z | a'@i
12. z | m@i
⊢ z | (a' + (m * (-c)))

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  a'  :  \mBbbZ{}@i
3.  m  :  \mBbbZ{}@i
4.  c  :  \mBbbZ{}@i
5.  (a'  -  a)  =  (m  *  c)@i
6.  1  |  a@i
7.  1  |  m@i
8.  \mforall{}z:\mBbbZ{}.  (((z  |  a)  \mwedge{}  (z  |  m))  {}\mRightarrow{}  (z  |  1))@i
9.  1  |  m
10.  z  :  \mBbbZ{}@i
11.  z  |  a'@i
12.  z  |  m@i
\mvdash{}  z  |  a


By

---

Latex:
(Subst'  a  =  (a'  +  (m  *  (-c)))  0  THEN  Auto')

---

Home Index