---

Step * 1 2 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
⊢ ∃c:ℤ_p. ((c * u) = 1 ∈ ℤ_p)
BY
{ ((InstLemma `gcd-reduce-prime` [⌜p⌝;⌜u mod p⌝]⋅ THENA Auto) THEN ExRepD) }

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)
⊢ ¬(p | (u mod p))

2
1. p : ℕ+
2. prime(p)
3. 0 ≠ 1 ∈ ℤ_p 
4. u : ℤ_p
5. u ≠ 0 ∈ ℤ_p 
6. u mod p ∈ ℕ+p
7. x : ℤ
8. y : ℤ
9. ((x * p) + (y * (u mod p))) = 1 ∈ ℤ
⊢ ∃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 
6.  u  mod  p  \mmember{}  \mBbbN{}\msupplus{}p
\mvdash{}  \mexists{}c:\mBbbZ{}\_p.  ((c  *  u)  =  1)


By

---

Latex:
((InstLemma  `gcd-reduce-prime`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}u  mod  p\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index