Step
*
2
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)
⊢ y ≡ x mod p^n
BY
{ ((InstHyp [⌜y⌝] (-1)⋅ THENA Auto) THEN (InstHyp [⌜x⌝] (-2)⋅ THENA Auto)) }
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. y 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)
\mvdash{}  y  \mequiv{}  x  mod  p\^{}n
By
Latex:
((InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))
Home
Index