---

Step * 1 2 1 1 1 of Lemma int_mod_ring_wf_field


1. p : ℕ+
2. prime(p)
3. 0 ≠ 1 ∈ ℤ_p 
4. u : ℤ_p
5. u ≠ 0 ∈ ℤ_p 
6. u mod p ∈ ℕ+p
7. prime(p)
8. p | (u mod p)
9. p ≤ (u mod p)
⊢ False
BY
{ (MoveToConcl (-1) THEN GenConclTerm ⌜u mod p⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}\msupplus{}
2.  prime(p)
3.  0  \mneq{}  1  \mmember{}  \mBbbZ{}\_p 
4.  u  :  \mBbbZ{}\_p
5.  u  \mneq{}  0  \mmember{}  \mBbbZ{}\_p 
6.  u  mod  p  \mmember{}  \mBbbN{}\msupplus{}p
7.  prime(p)
8.  p  |  (u  mod  p)
9.  p  \mleq{}  (u  mod  p)
\mvdash{}  False


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclTerm  \mkleeneopen{}u  mod  p\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index