---

Step * 1 1 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
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)
BY
{ ((RWW "p-mul-assoc p-mul-int exp_add<" (-1)⋅ THENM (NthHypEq (-1) THEN EqCD)) THEN Auto) }

---

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
20.  p\^{}((M  +  (N  -  x3))  -  x5)(p)  *  p\^{}x5(p)  *  x4  =  p\^{}((M  +  (N  -  x3))  -  x5)(p)  *  p\^{}x3(p)  *  x6
\mvdash{}  p\^{}(M  +  (N  -  x3))(p)  *  x4  =  p\^{}(N  +  (M  -  x5))(p)  *  x6


By

---

Latex:
((RWW  "p-mul-assoc  p-mul-int  exp\_add<"  (-1)\mcdot{}  THENM  (NthHypEq  (-1)  THEN  EqCD))  THEN  Auto)

---

Home Index