---

Step * 1 of Lemma pa-add_functionality


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)
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜imax(x5;y5) = M ∈ ℕ⌝⋅ THENA Auto)
   THEN GenConcl ⌜imax(x3;y3) = N ∈ ℕ⌝⋅
   THEN Auto) }

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. M : ℕ
13. imax(x5;y5) = M ∈ ℕ
14. N : ℕ
15. imax(x3;y3) = N ∈ ℕ
16. x3 ≤ N
17. y3 ≤ N
18. x5 ≤ M
19. y5 ≤ M
⊢ p^M(p) * p^N - x3(p) * x4 + p^N - y3(p) * y4 = p^N(p) * p^M - x5(p) * x6 + p^M - y5(p) * y6 ∈ p-adics(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  x3  :  \mBbbN{}
3.  x4  :  p-adics(p)
4.  y3  :  \mBbbN{}
5.  y4  :  p-adics(p)
6.  x5  :  \mBbbN{}
7.  x6  :  p-adics(p)
8.  y5  :  \mBbbN{}
9.  y6  :  p-adics(p)
10.  p\^{}y5(p)  *  y4  =  p\^{}y3(p)  *  y6
11.  p\^{}x5(p)  *  x4  =  p\^{}x3(p)  *  x6
12.  (x3  \mleq{}  imax(x3;y3))  \mwedge{}  (y3  \mleq{}  imax(x3;y3))
13.  (x5  \mleq{}  imax(x5;y5))  \mwedge{}  (y5  \mleq{}  imax(x5;y5))
\mvdash{}  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


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}imax(x5;y5)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  GenConcl  \mkleeneopen{}imax(x3;y3)  =  N\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index