---

Step * 1 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. 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)
BY
{ ((RWW "p-distrib.1 p-distrib.2 p-mul-assoc p-mul-int exp-fastexp< exp_add<" 0⋅ THENM EqCD) THENA Auto) }

1
.....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)

2
.....subterm..... T:t
3: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 - y3))(p) * y4 = p^(N + (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.  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(p)  *  p\^{}N  -  x3(p)  *  x4  +  p\^{}N  -  y3(p)  *  y4  =  p\^{}N(p)  *  p\^{}M  -  x5(p)  *  x6  +  p\^{}M  -  y5(p)  *  y6


By

---

Latex:
((RWW  "p-distrib.1  p-distrib.2  p-mul-assoc  p-mul-int  exp-fastexp<  exp\_add<"  0\mcdot{}  THENM  EqCD)
  THENA  Auto
  )

---

Home Index