Step
*
2
1
1
1
1
1
1
1
of Lemma
p-adic-property
1. p : ℕ+
2. n : ℕ+
3. x : ℤ
4. y : ℤ
5. m : ℕ
6. y mod(p^n + m) = x mod(p^n + m) ∈ ℤ
7. ∀z:ℤ. (z mod(p^n + m) ≡ z mod p^n)
8. y mod(p^n + m) ≡ y mod p^n
9. x mod(p^n + m) ≡ x mod p^n
⊢ y ≡ x mod p^n
BY
{ HypSubst' (-4) (-2) }
1
1. p : ℕ+
2. n : ℕ+
3. x : ℤ
4. y : ℤ
5. m : ℕ
6. y mod(p^n + m) = x mod(p^n + m) ∈ ℤ
7. ∀z:ℤ. (z mod(p^n + m) ≡ z mod p^n)
8. x mod(p^n + m) ≡ y mod p^n
9. x mod(p^n + m) ≡ x mod p^n
⊢ y ≡ x mod p^n
Latex:
Latex:
1.  p  :  \mBbbN{}\msupplus{}
2.  n  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  m  :  \mBbbN{}
6.  y  mod(p\^{}n  +  m)  =  x  mod(p\^{}n  +  m)
7.  \mforall{}z:\mBbbZ{}.  (z  mod(p\^{}n  +  m)  \mequiv{}  z  mod  p\^{}n)
8.  y  mod(p\^{}n  +  m)  \mequiv{}  y  mod  p\^{}n
9.  x  mod(p\^{}n  +  m)  \mequiv{}  x  mod  p\^{}n
\mvdash{}  y  \mequiv{}  x  mod  p\^{}n
By
Latex:
HypSubst'  (-4)  (-2)
Home
Index