Step
*
1
of Lemma
eqmod_fun
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
BY
{ ((FwdThruLemma `eqmod_inversion` [6] THENM Thin 6) THENA Auto) }
1
1. m : ℤ
2. a : ℤ
3. a' : ℤ
4. b : ℤ
5. b' : ℤ
6. b ≡ b' mod m
7. a ≡ b mod m
8. a' ≡ a mod m
⊢ a' ≡ b' mod m
Latex:
Latex:
1. m : \mBbbZ{}
2. a : \mBbbZ{}
3. a' : \mBbbZ{}
4. b : \mBbbZ{}
5. b' : \mBbbZ{}
6. a \mequiv{} a' mod m
7. b \mequiv{} b' mod m
8. a \mequiv{} b mod m
\mvdash{} a' \mequiv{} b' mod m
By
Latex:
((FwdThruLemma `eqmod\_inversion` [6] THENM Thin 6) THENA Auto)
Home
Index