---

Step * 1 2 of Lemma int_mod_ring_wf_field


1. p : ℕ+
2. prime(p)
3. 0 ≠ 1 ∈ ℤ_p 
4. u : ℤ_p
5. u ≠ 0 ∈ ℤ_p 
⊢ ∃c:ℤ_p. ((c * u) = 1 ∈ ℤ_p)
BY
{ (InstLemma `modulus-int_mod-nonzero` [⌜p⌝;⌜u⌝]⋅ THENA Auto) }

1
1. p : ℕ+
2. prime(p)
3. 0 ≠ 1 ∈ ℤ_p 
4. u : ℤ_p
5. u ≠ 0 ∈ ℤ_p 
6. u mod p ∈ ℕ+p
⊢ ∃c:ℤ_p. ((c * u) = 1 ∈ ℤ_p)

---

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 
\mvdash{}  \mexists{}c:\mBbbZ{}\_p.  ((c  *  u)  =  1)


By

---

Latex:
(InstLemma  `modulus-int\_mod-nonzero`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index