---

Step * 1 of Lemma pa-mul_functionality


1. p : {2...}
2. q : {2...}
3. x3 : ℕ
4. x4 : p-adics(p)
5. y3 : ℕ
6. y4 : p-adics(p)
7. x5 : ℕ
8. x6 : p-adics(p)
9. y5 : ℕ
10. y6 : p-adics(p)
11. p^y5(p) * y4 = p^y3(p) * y6 ∈ p-adics(p)
12. p^x5(p) * x4 = p^x3(p) * x6 ∈ p-adics(p)
13. p = q ∈ ℤ
⊢ p^(x5 + y5)(p) * x4 * y4 = p^(x3 + y3)(p) * x6 * y6 ∈ p-adics(p)
BY
{ (RWW "exp_add p-mul-int<" 0 THENA Auto) }

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

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  q  :  \{2...\}
3.  x3  :  \mBbbN{}
4.  x4  :  p-adics(p)
5.  y3  :  \mBbbN{}
6.  y4  :  p-adics(p)
7.  x5  :  \mBbbN{}
8.  x6  :  p-adics(p)
9.  y5  :  \mBbbN{}
10.  y6  :  p-adics(p)
11.  p\^{}y5(p)  *  y4  =  p\^{}y3(p)  *  y6
12.  p\^{}x5(p)  *  x4  =  p\^{}x3(p)  *  x6
13.  p  =  q
\mvdash{}  p\^{}(x5  +  y5)(p)  *  x4  *  y4  =  p\^{}(x3  +  y3)(p)  *  x6  *  y6


By

---

Latex:
(RWW  "exp\_add  p-mul-int<"  0  THENA  Auto)

---

Home Index