Step
*
2
1
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)
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)
BY
{ (RWW "p-distrib.1 p-distrib.2 p-mul-assoc p-mul-int exp-fastexp< exp_add< p-add-assoc" 0 THENA Auto) }
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 + (K - X1))(p) * X2 + p^((J + (K - M)) + (M - Y1))(p) * Y2 + p^((J + (K - M)) + (M - Z1))(p) * Z2
= p^((K + (J - N)) + (N - X1))(p) * X2 + p^((K + (J - N)) + (N - Y1))(p) * Y2 + p^(K + (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)
27. K : \mBbbZ{}
28. imax(X1;M) = K
29. (X1 \mleq{} K) \mwedge{} (M \mleq{} K)
30. J : \mBbbZ{}
31. imax(N;Z1) = J
32. (N \mleq{} J) \mwedge{} (Z1 \mleq{} J)
\mvdash{} 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
By
Latex:
(RWW "p-distrib.1 p-distrib.2 p-mul-assoc p-mul-int exp-fastexp< exp\_add< p-add-assoc" 0 THENA Auto)
Home
Index