Step
*
1
2
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
6. u mod p ∈ ℕ+p
7. x : ℤ
8. y : ℤ
9. ((x * p) + (y * (u mod p))) = 1 ∈ ℤ
⊢ ∃c:ℤ_p. ((c * u) = 1 ∈ ℤ_p)
BY
{ D 0 With ⌜y⌝ }
1
.....wf.....
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 ∈ ℤ
⊢ y ∈ ℤ_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 ∈ ℤ
⊢ (y * u) = 1 ∈ ℤ_p
3
.....wf.....
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 ∈ ℤ
10. c : ℤ_p
⊢ istype((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
7. x : \mBbbZ{}
8. y : \mBbbZ{}
9. ((x * p) + (y * (u mod p))) = 1
\mvdash{} \mexists{}c:\mBbbZ{}\_p. ((c * u) = 1)
By
Latex:
D 0 With \mkleeneopen{}y\mkleeneclose{}
Home
Index