---

Step * 1 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(p) * p^y5(p) * x4 * y4 = p^x3(p) * p^y3(p) * x6 * y6 ∈ p-adics(p)
BY
{ ((Assert p^x5(p) * x4 * p^y5(p) * y4 = p^x3(p) * x6 * p^y3(p) * y6 ∈ p-adics(p) BY
          (EqCD THEN Auto))
   THEN NthHypEq (-1)
   THEN EqCDA
   THEN ((RWW "p-mul-assoc" 0 THENA Auto) THEN EqCDA)
   THEN (RWW "p-mul-assoc<" 0 THENA Auto)
   THEN EqCDA
   THEN Auto) }

---

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(p)  *  p\^{}y5(p)  *  x4  *  y4  =  p\^{}x3(p)  *  p\^{}y3(p)  *  x6  *  y6


By

---

Latex:
((Assert  p\^{}x5(p)  *  x4  *  p\^{}y5(p)  *  y4  =  p\^{}x3(p)  *  x6  *  p\^{}y3(p)  *  y6  BY
                (EqCD  THEN  Auto))
  THEN  NthHypEq  (-1)
  THEN  EqCDA
  THEN  ((RWW  "p-mul-assoc"  0  THENA  Auto)  THEN  EqCDA)
  THEN  (RWW  "p-mul-assoc<"  0  THENA  Auto)
  THEN  EqCDA
  THEN  Auto)

---

Home Index