---

Step * 1 2 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)
⊢ ¬(p | (u mod p))
BY
{ ((D 0 THENA Auto) THEN FLemma `divisors_bound` [-1] THEN Auto) }

1
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

---

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)
\mvdash{}  \mneg{}(p  |  (u  mod  p))


By

---

Latex:
((D  0  THENA  Auto)  THEN  FLemma  `divisors\_bound`  [-1]  THEN  Auto)

---

Home Index