---

Step * 2 1 1 1 1 of Lemma padic-ring_wf


1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
10. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12. x : padic(p)
13. y : padic(p)
14. z : padic(p)
15. X1 : ℕ
16. X2 : p-adics(p)
17. Y1 : ℕ
18. Y2 : p-adics(p)
19. Z1 : ℕ
20. Z2 : p-adics(p)
21. M : ℤ
22. imax(Y1;Z1) = M ∈ ℤ
23. (Y1 ≤ M) ∧ (Z1 ≤ M)
24. N : ℤ
25. imax(X1;Y1) = N ∈ ℤ
26. (X1 ≤ N) ∧ (Y1 ≤ N)
⊢ let n,a = eval k = imax(X1;M) in
            eval c = p^k - X1 in
            eval d = p^k - M in
              <k, c(p) * X2 + d(p) * p^M - Y1(p) * Y2 + p^M - Z1(p) * Z2> 
  in let m,b = eval k = imax(N;Z1) in
               eval c = p^k - N in
               eval d = p^k - Z1 in
                 <k, c(p) * p^N - X1(p) * X2 + p^N - Y1(p) * Y2 + d(p) * Z2> 
     in p^m(p) * a = p^n(p) * b ∈ p-adics(p)
BY
{ ((Assert (X1 ≤ imax(X1;M)) ∧ (M ≤ imax(X1;M)) BY
          Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜imax(X1;M) = K ∈ ℤ⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (Assert (N ≤ imax(N;Z1)) ∧ (Z1 ≤ imax(N;Z1)) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜imax(N;Z1) = J ∈ ℤ⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0) }

1
1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
10. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12. x : padic(p)
13. y : padic(p)
14. z : padic(p)
15. X1 : ℕ
16. X2 : p-adics(p)
17. Y1 : ℕ
18. Y2 : p-adics(p)
19. Z1 : ℕ
20. Z2 : p-adics(p)
21. M : ℤ
22. imax(Y1;Z1) = M ∈ ℤ
23. (Y1 ≤ M) ∧ (Z1 ≤ M)
24. N : ℤ
25. imax(X1;Y1) = N ∈ ℤ
26. (X1 ≤ N) ∧ (Y1 ≤ N)
27. K : ℤ
28. imax(X1;M) = K ∈ ℤ
29. (X1 ≤ K) ∧ (M ≤ K)
30. J : ℤ
31. imax(N;Z1) = J ∈ ℤ
32. (N ≤ J) ∧ (Z1 ≤ J)
⊢ p^J(p) * p^K - X1(p) * X2 + p^K - M(p) * p^M - Y1(p) * Y2 + p^M - Z1(p) * Z2
= p^K(p) * p^J - N(p) * p^N - X1(p) * X2 + p^N - Y1(p) * Y2 + p^J - Z1(p) * Z2
∈ p-adics(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  \mBbbZ{}(p)  \mmember{}  RngSig
3.  \mforall{}[x,y,z:p-adics(p)].    (x  +  y  +  z  =  x  +  y  +  z)
4.  \mforall{}[x:p-adics(p)].  ((x  +  0(p)  =  x)  \mwedge{}  (0(p)  +  x  =  x))
5.  \mforall{}[x:p-adics(p)].  ((x  +  -(x)  =  0(p))  \mwedge{}  (-(x)  +  x  =  0(p)))
6.  \mforall{}[x,y,z:p-adics(p)].    (x  *  y  *  z  =  x  *  y  *  z)
7.  \mforall{}[x:p-adics(p)].  ((x  *  1(p)  =  x)  \mwedge{}  (1(p)  *  x  =  x))
8.  \mforall{}[a,x,y:p-adics(p)].    ((a  *  x  +  y  =  a  *  x  +  a  *  y)  \mwedge{}  (x  +  y  *  a  =  x  *  a  +  y  *  a))
9.  \mforall{}[x,y:p-adics(p)].    (x  *  y  =  y  *  x)
10.  \mforall{}a,b:basic-padic(p).    bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11.  \mforall{}a,b:basic-padic(p).    bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12.  x  :  padic(p)
13.  y  :  padic(p)
14.  z  :  padic(p)
15.  X1  :  \mBbbN{}
16.  X2  :  p-adics(p)
17.  Y1  :  \mBbbN{}
18.  Y2  :  p-adics(p)
19.  Z1  :  \mBbbN{}
20.  Z2  :  p-adics(p)
21.  M  :  \mBbbZ{}
22.  imax(Y1;Z1)  =  M
23.  (Y1  \mleq{}  M)  \mwedge{}  (Z1  \mleq{}  M)
24.  N  :  \mBbbZ{}
25.  imax(X1;Y1)  =  N
26.  (X1  \mleq{}  N)  \mwedge{}  (Y1  \mleq{}  N)
\mvdash{}  let  n,a  =  eval  k  =  imax(X1;M)  in
                        eval  c  =  p\^{}k  -  X1  in
                        eval  d  =  p\^{}k  -  M  in
                            <k,  c(p)  *  X2  +  d(p)  *  p\^{}M  -  Y1(p)  *  Y2  +  p\^{}M  -  Z1(p)  *  Z2> 
    in  let  m,b  =  eval  k  =  imax(N;Z1)  in
                              eval  c  =  p\^{}k  -  N  in
                              eval  d  =  p\^{}k  -  Z1  in
                                  <k,  c(p)  *  p\^{}N  -  X1(p)  *  X2  +  p\^{}N  -  Y1(p)  *  Y2  +  d(p)  *  Z2> 
          in  p\^{}m(p)  *  a  =  p\^{}n(p)  *  b


By

---

Latex:
((Assert  (X1  \mleq{}  imax(X1;M))  \mwedge{}  (M  \mleq{}  imax(X1;M))  BY
                Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}imax(X1;M)  =  K\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  (N  \mleq{}  imax(N;Z1))  \mwedge{}  (Z1  \mleq{}  imax(N;Z1))  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}imax(N;Z1)  =  J\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0)

---

Home Index