Step * 2 1 1 1 1 1 1 of Lemma p-adic-property


1. : ℕ+
2. : ℕ+
3. : ℤ
4. : ℤ
5. : ℕ
6. mod(p^n m) mod(p^n m) ∈ ℤ
7. ∀z:ℤ(z mod(p^n m) ≡ mod p^n)
⊢ y ≡ mod p^n
BY
((InstHyp [⌜y⌝(-1)⋅ THENA Auto) THEN (InstHyp [⌜x⌝(-2)⋅ THENA Auto)) }

1
1. : ℕ+
2. : ℕ+
3. : ℤ
4. : ℤ
5. : ℕ
6. mod(p^n m) mod(p^n m) ∈ ℤ
7. ∀z:ℤ(z mod(p^n m) ≡ mod p^n)
8. mod(p^n m) ≡ mod p^n
9. mod(p^n m) ≡ mod p^n
⊢ y ≡ 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