---

Step * 2 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' + (m * (-c)))
BY
{ ((BLemma `divisor_of_sum` THENM Try (BLemma `divisor_of_mul`)) THEN Auto) }

---

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'  +  (m  *  (-c)))


By

---

Latex:
((BLemma  `divisor\_of\_sum`  THENM  Try  (BLemma  `divisor\_of\_mul`))  THEN  Auto)

---

Home Index