---

Step * of Lemma eqmod_functionality_wrt_eqmod

∀m,m',a,a',b,b':ℤ.  (a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ (a ≡ b mod m ⇐⇒ a' ≡ b' mod m') supposing m = m' ∈ ℤ
BY
{ Auto }

1
1. m : ℤ
2. m' : ℤ
3. a : ℤ
4. a' : ℤ
5. b : ℤ
6. b' : ℤ
7. m = m' ∈ ℤ
8. a ≡ a' mod m
9. b ≡ b' mod m
10. a ≡ b mod m
⊢ a' ≡ b' mod m'

2
1. m : ℤ
2. m' : ℤ
3. a : ℤ
4. a' : ℤ
5. b : ℤ
6. b' : ℤ
7. m = m' ∈ ℤ
8. a ≡ a' mod m
9. b ≡ b' mod m
10. a' ≡ b' mod m'
⊢ a ≡ b mod m

---

Latex:

---

Latex:
\mforall{}m,m',a,a',b,b':\mBbbZ{}.
    (a  \mequiv{}  a'  mod  m)  {}\mRightarrow{}  (b  \mequiv{}  b'  mod  m)  {}\mRightarrow{}  (a  \mequiv{}  b  mod  m  \mLeftarrow{}{}\mRightarrow{}  a'  \mequiv{}  b'  mod  m')  supposing  m  =  m'


By

---

Latex:
Auto

---

Home Index