---

Step * 1 of Lemma eqmod_functionality_wrt_eqmod


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'
BY
{ ((RevHypSubst 7 0 THENM OnHyps [7;2] Thin) THENA Auto) }

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

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  m'  :  \mBbbZ{}
3.  a  :  \mBbbZ{}
4.  a'  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  b'  :  \mBbbZ{}
7.  m  =  m'
8.  a  \mequiv{}  a'  mod  m
9.  b  \mequiv{}  b'  mod  m
10.  a  \mequiv{}  b  mod  m
\mvdash{}  a'  \mequiv{}  b'  mod  m'


By

---

Latex:
((RevHypSubst  7  0  THENM  OnHyps  [7;2]  Thin)  THENA  Auto)

---

Home Index