Step
*
2
1
1
of Lemma
p-mul-int-cancelation-2
1. p : {p:{2...}| prime(p)}
2. k : ℕ
3. a : p-adics(p)
4. b : p-adics(p)
5. CoPrime(k,p)
6. k(p) * a = k(p) * b ∈ p-adics(p)
7. p-inv(p;k(p)) ∈ p-adics(p)
8. k(p) * p-inv(p;k(p)) = 1(p) ∈ p-adics(p)
9. p-inv(p;k(p)) * k(p) * a = p-inv(p;k(p)) * k(p) * b ∈ p-adics(p)
⊢ a = b ∈ p-adics(p)
BY
{ ((Assert ⌜∀c:p-adics(p). (p-inv(p;k(p)) * k(p) * c = c ∈ p-adics(p))⌝⋅ THENM (RWO "-1" (-2) THEN Auto))
THEN ThinVar `a'
THEN ThinVar `b') }
1
1. p : {p:{2...}| prime(p)}
2. k : ℕ
3. CoPrime(k,p)
4. p-inv(p;k(p)) ∈ p-adics(p)
5. k(p) * p-inv(p;k(p)) = 1(p) ∈ p-adics(p)
⊢ ∀c:p-adics(p). (p-inv(p;k(p)) * k(p) * c = c ∈ p-adics(p))
Latex:
Latex:
1. p : \{p:\{2...\}| prime(p)\}
2. k : \mBbbN{}
3. a : p-adics(p)
4. b : p-adics(p)
5. CoPrime(k,p)
6. k(p) * a = k(p) * b
7. p-inv(p;k(p)) \mmember{} p-adics(p)
8. k(p) * p-inv(p;k(p)) = 1(p)
9. p-inv(p;k(p)) * k(p) * a = p-inv(p;k(p)) * k(p) * b
\mvdash{} a = b
By
Latex:
((Assert \mkleeneopen{}\mforall{}c:p-adics(p). (p-inv(p;k(p)) * k(p) * c = c)\mkleeneclose{}\mcdot{} THENM (RWO "-1" (-2) THEN Auto))
THEN ThinVar `a'
THEN ThinVar `b')
Home
Index