Step
*
1
2
1
2
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 ∈ ℤ
⊢ (y * u) = 1 ∈ ℤ_p
BY
{ (Assert u = (u mod p) ∈ ℤ_p BY
(All Thin THEN DVar `u' THEN EqTypeCD THEN Auto THEN RWO "-1<" 0 THEN Auto THEN Symmetry 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. x : ℤ
8. y : ℤ
9. ((x * p) + (y * (u mod p))) = 1 ∈ ℤ
10. u = (u mod p) ∈ ℤ_p
⊢ (y * 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{} (y * u) = 1
By
Latex:
(Assert u = (u mod p) BY
(All Thin
THEN DVar `u'
THEN EqTypeCD
THEN Auto
THEN RWO "-1<" 0
THEN Auto
THEN Symmetry
THEN Auto))
Home
Index