---

Step * of Lemma pa-add_functionality

No Annotations
∀[p:{2...}]. ∀[x1,y1,x2,y2:basic-padic(p)].
  (pa-add(p;x1;y1) = pa-add(p;x2;y2) ∈ padic(p)) supposing (bpa-equiv(p;x1;x2) and bpa-equiv(p;y1;y2))
BY
{ (Intros
   THEN (RWO "equal-padics" 0 THENA Auto)
   THEN Unfold `pa-add` 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 bpa-add``)
   THEN (Assert (x3 ≤ imax(x3;y3)) ∧ (y3 ≤ imax(x3;y3)) BY
               Auto)
   THEN (Assert (x5 ≤ imax(x5;y5)) ∧ (y5 ≤ imax(x5;y5)) BY
               Auto)
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0) }

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

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (RWO  "equal-padics"  0  THENA  Auto)
  THEN  Unfold  `pa-add`  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  bpa-add``)
  THEN  (Assert  (x3  \mleq{}  imax(x3;y3))  \mwedge{}  (y3  \mleq{}  imax(x3;y3))  BY
                          Auto)
  THEN  (Assert  (x5  \mleq{}  imax(x5;y5))  \mwedge{}  (y5  \mleq{}  imax(x5;y5))  BY
                          Auto)
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0)

---

Home Index