---

Step * of Lemma pa-mul_functionality

∀[p,q:{2...}]. ∀[x1,y1,x2,y2:basic-padic(p)].
  (pa-mul(p;x1;y1) = pa-mul(q;x2;y2) ∈ padic(p)) supposing ((p = q ∈ ℤ) and bpa-equiv(p;x1;x2) and bpa-equiv(p;y1;y2))
BY
{ ((Intros THEN Eliminate ⌜q⌝⋅)
   THEN (RWO "equal-padics" 0 THENA Auto)
   THEN Unfold `pa-mul` 0
   THEN (BLemma `bpa-equiv-iff-norm` THENA Auto)
   THEN DVar  `x1'
   THEN DVar `x2'
   THEN DVar `y1'
   THEN DVar  `y2'
   THEN Reduce 0
   THEN All (RepUR  ``bpa-equiv``)) }

1
1. p : {2...}
2. q : {2...}
3. x3 : ℕ
4. x4 : p-adics(p)
5. y3 : ℕ
6. y4 : p-adics(p)
7. x5 : ℕ
8. x6 : p-adics(p)
9. y5 : ℕ
10. y6 : p-adics(p)
11. p^y5(p) * y4 = p^y3(p) * y6 ∈ p-adics(p)
12. p^x5(p) * x4 = p^x3(p) * x6 ∈ p-adics(p)
13. p = q ∈ ℤ
⊢ p^(x5 + y5)(p) * x4 * y4 = p^(x3 + y3)(p) * x6 * y6 ∈ p-adics(p)

---

Latex:

---

Latex:
\mforall{}[p,q:\{2...\}].  \mforall{}[x1,y1,x2,y2:basic-padic(p)].
    (pa-mul(p;x1;y1)  =  pa-mul(q;x2;y2))  supposing 
          ((p  =  q)  and 
          bpa-equiv(p;x1;x2)  and 
          bpa-equiv(p;y1;y2))


By

---

Latex:
((Intros  THEN  Eliminate  \mkleeneopen{}q\mkleeneclose{}\mcdot{})
  THEN  (RWO  "equal-padics"  0  THENA  Auto)
  THEN  Unfold  `pa-mul`  0
  THEN  (BLemma  `bpa-equiv-iff-norm`  THENA  Auto)
  THEN  DVar    `x1'
  THEN  DVar  `x2'
  THEN  DVar  `y1'
  THEN  DVar    `y2'
  THEN  Reduce  0
  THEN  All  (RepUR    ``bpa-equiv``))

---

Home Index