Step
*
2
5
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. IsMonoid(padic(p);λu,v. pa-mul(p;u;v);1(p))
13. a : padic(p)
14. x : padic(p)
15. y : padic(p)
⊢ bpa-equiv(p;bpa-mul(p;a;bpa-add(p;x;y));bpa-add(p;bpa-mul(p;a;x);bpa-mul(p;a;y)))
BY
{ (((GenConcl ⌜x = X ∈ basic-padic(p)⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1)
THEN ((GenConcl ⌜y = Y ∈ basic-padic(p)⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1)
THEN ((GenConcl ⌜a = Z ∈ basic-padic(p)⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1)
THEN RepUR ``bpa-equiv bpa-mul bpa-add`` 0
THEN ((Subst' imax(Z1 + X1;Z1 + Y1) ~ Z1 + imax(X1;Y1) 0
THENM ((Assert (X1 ≤ imax(X1;Y1)) ∧ (Y1 ≤ imax(X1;Y1)) BY
Auto)
THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
THEN Reduce 0)
)
THENA (Auto THEN (RWO "imax_unfold" 0 THENA Auto) THEN AutoSplit)
)
THEN MoveToConcl (-1)
THEN (GenConcl ⌜imax(X1;Y1) = M ∈ ℤ⌝⋅ THENA Auto)
THEN (RWW "p-distrib.1" 0 THENA Auto)
THEN (RWW "p-mul-assoc p-mul-int exp-fastexp< exp_add<" 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. IsMonoid(padic(p);λu,v. pa-mul(p;u;v);1(p))
13. a : padic(p)
14. x : padic(p)
15. y : padic(p)
16. X1 : ℕ
17. X2 : p-adics(p)
18. Y1 : ℕ
19. Y2 : p-adics(p)
20. Z1 : ℕ
21. Z2 : p-adics(p)
22. M : ℤ
23. imax(X1;Y1) = M ∈ ℤ
⊢ ((X1 ≤ M) ∧ (Y1 ≤ M))
⇒ (p^(Z1 + M)(p) * Z2 * p^(M - X1)(p) * X2 + p^(Z1 + M)(p) * Z2 * p^(M - Y1)(p) * Y2
= p^((Z1 + M) + ((Z1 + M) - Z1 + X1))(p) * Z2 * X2 + p^((Z1 + M) + ((Z1 + M) - Z1 + Y1))(p) * Z2 * Y2
∈ 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. IsMonoid(padic(p);\mlambda{}u,v. pa-mul(p;u;v);1(p))
13. a : padic(p)
14. x : padic(p)
15. y : padic(p)
\mvdash{} bpa-equiv(p;bpa-mul(p;a;bpa-add(p;x;y));bpa-add(p;bpa-mul(p;a;x);bpa-mul(p;a;y)))
By
Latex:
(((GenConcl \mkleeneopen{}x = X\mkleeneclose{}\mcdot{} THENA Auto) THEN Thin (-1) THEN D -1)
THEN ((GenConcl \mkleeneopen{}y = Y\mkleeneclose{}\mcdot{} THENA Auto) THEN Thin (-1) THEN D -1)
THEN ((GenConcl \mkleeneopen{}a = Z\mkleeneclose{}\mcdot{} THENA Auto) THEN Thin (-1) THEN D -1)
THEN RepUR ``bpa-equiv bpa-mul bpa-add`` 0
THEN ((Subst' imax(Z1 + X1;Z1 + Y1) \msim{} Z1 + imax(X1;Y1) 0
THENM ((Assert (X1 \mleq{} imax(X1;Y1)) \mwedge{} (Y1 \mleq{} imax(X1;Y1)) BY
Auto)
THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
THEN Reduce 0)
)
THENA (Auto THEN (RWO "imax\_unfold" 0 THENA Auto) THEN AutoSplit)
)
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}imax(X1;Y1) = M\mkleeneclose{}\mcdot{} THENA Auto)
THEN (RWW "p-distrib.1" 0 THENA Auto)
THEN (RWW "p-mul-assoc p-mul-int exp-fastexp< exp\_add<" 0 THENA Auto))
Home
Index