---

Step * 1 1 1 of Lemma pa-add_functionality

.....subterm..... T:t
2:n
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 + (N - x3))(p) * x4 = p^(N + (M - x5))(p) * x6 ∈ p-adics(p)
BY
{ (Assert p^((M + (N - x3)) - x5)(p) * p^x5(p) * x4 = p^((M + (N - x3)) - x5)(p) * p^x3(p) * x6 ∈ p-adics(p) BY
         (EqCDA 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
20. p^((M + (N - x3)) - x5)(p) * p^x5(p) * x4 = p^((M + (N - x3)) - x5)(p) * p^x3(p) * x6 ∈ p-adics(p)
⊢ p^(M + (N - x3))(p) * x4 = p^(N + (M - x5))(p) * x6 ∈ p-adics(p)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.  M  :  \mBbbN{}
13.  imax(x5;y5)  =  M
14.  N  :  \mBbbN{}
15.  imax(x3;y3)  =  N
16.  x3  \mleq{}  N
17.  y3  \mleq{}  N
18.  x5  \mleq{}  M
19.  y5  \mleq{}  M
\mvdash{}  p\^{}(M  +  (N  -  x3))(p)  *  x4  =  p\^{}(N  +  (M  -  x5))(p)  *  x6


By

---

Latex:
(Assert  p\^{}((M  +  (N  -  x3))  -  x5)(p)  *  p\^{}x5(p)  *  x4  =  p\^{}((M  +  (N  -  x3))  -  x5)(p)  *  p\^{}x3(p)  *  x6  BY
              (EqCDA  THEN  Auto))

---

Home Index