Step * 2 of Lemma eqmod_fun


1. : ℤ
2. : ℤ
3. a' : ℤ
4. : ℤ
5. b' : ℤ
6. a ≡ a' mod m
7. b ≡ b' mod m
8. a' ≡ b' mod m
⊢ a ≡ mod m
BY
((FwdThruLemma `eqmod_inversion` [7] THENM Thin 7) THENA Auto) }

1
1. : ℤ
2. : ℤ
3. a' : ℤ
4. : ℤ
5. b' : ℤ
6. a ≡ a' mod m
7. a' ≡ b' mod m
8. b' ≡ mod m
⊢ a ≡ 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`  [7]  THENM  Thin  7)  THENA  Auto)




Home Index