Step
*
2
2
of Lemma
p-inv_wf
1. p : {p:{2...}| prime(p)}
2. a : {a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)}
3. p-inv(p;a) = (λn.(TERMOF{p-adic-inv-lemma:o, \\v:l} p a n)) ∈ (n:ℕ+ ⟶ (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)]))
4. p-inv(p;a) ∈ p-adics(p)
⊢ p-inv(p;a) ∈ {b:p-adics(p)| a * b = 1(p) ∈ p-adics(p)}
BY
{ (MemTypeCD THEN Auto) }
1
.....set predicate.....
1. p : {p:{2...}| prime(p)}
2. a : {a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)}
3. p-inv(p;a) = (λn.(TERMOF{p-adic-inv-lemma:o, \\v:l} p a n)) ∈ (n:ℕ+ ⟶ (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)]))
4. p-inv(p;a) ∈ p-adics(p)
⊢ a * p-inv(p;a) = 1(p) ∈ p-adics(p)
Latex:
Latex:
1. p : \{p:\{2...\}| prime(p)\}
2. a : \{a:p-adics(p)| \mneg{}((a 1) = 0)\}
3. p-inv(p;a) = (\mlambda{}n.(TERMOF\{p-adic-inv-lemma:o, \mbackslash{}\mbackslash{}v:l\} p a n))
4. p-inv(p;a) \mmember{} p-adics(p)
\mvdash{} p-inv(p;a) \mmember{} \{b:p-adics(p)| a * b = 1(p)\}
By
Latex:
(MemTypeCD THEN Auto)
Home
Index