---

Step * 1 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