Step
*
1
of Lemma
pa-add_functionality
1. p : {2...}
2. x3 : ℕ
3. x4 : p-adics(p)
4. y3 : ℕ
5. y4 : p-adics(p)
6. x5 : ℕ
7. x6 : p-adics(p)
8. y5 : ℕ
9. y6 : p-adics(p)
10. p^y5(p) * y4 = p^y3(p) * y6 ∈ p-adics(p)
11. p^x5(p) * x4 = p^x3(p) * x6 ∈ p-adics(p)
12. (x3 ≤ imax(x3;y3)) ∧ (y3 ≤ imax(x3;y3))
13. (x5 ≤ imax(x5;y5)) ∧ (y5 ≤ imax(x5;y5))
⊢ p^imax(x5;y5)(p) * p^imax(x3;y3) - x3(p) * x4 + p^imax(x3;y3) - y3(p) * y4
= p^imax(x3;y3)(p) * p^imax(x5;y5) - x5(p) * x6 + p^imax(x5;y5) - y5(p) * y6
∈ p-adics(p)
BY
{ (RepeatFor 2 (MoveToConcl (-1))
THEN (GenConcl ⌜imax(x5;y5) = M ∈ ℕ⌝⋅ THENA Auto)
THEN GenConcl ⌜imax(x3;y3) = N ∈ ℕ⌝⋅
THEN Auto) }
1
1. p : {2...}
2. x3 : ℕ
3. x4 : p-adics(p)
4. y3 : ℕ
5. y4 : p-adics(p)
6. x5 : ℕ
7. x6 : p-adics(p)
8. y5 : ℕ
9. y6 : p-adics(p)
10. p^y5(p) * y4 = p^y3(p) * y6 ∈ p-adics(p)
11. p^x5(p) * x4 = p^x3(p) * x6 ∈ p-adics(p)
12. M : ℕ
13. imax(x5;y5) = M ∈ ℕ
14. N : ℕ
15. imax(x3;y3) = N ∈ ℕ
16. x3 ≤ N
17. y3 ≤ N
18. x5 ≤ M
19. y5 ≤ M
⊢ p^M(p) * p^N - x3(p) * x4 + p^N - y3(p) * y4 = p^N(p) * p^M - x5(p) * x6 + p^M - y5(p) * y6 ∈ p-adics(p)
Latex:
Latex:
1. p : \{2...\}
2. x3 : \mBbbN{}
3. x4 : p-adics(p)
4. y3 : \mBbbN{}
5. y4 : p-adics(p)
6. x5 : \mBbbN{}
7. x6 : p-adics(p)
8. y5 : \mBbbN{}
9. y6 : p-adics(p)
10. p\^{}y5(p) * y4 = p\^{}y3(p) * y6
11. p\^{}x5(p) * x4 = p\^{}x3(p) * x6
12. (x3 \mleq{} imax(x3;y3)) \mwedge{} (y3 \mleq{} imax(x3;y3))
13. (x5 \mleq{} imax(x5;y5)) \mwedge{} (y5 \mleq{} imax(x5;y5))
\mvdash{} p\^{}imax(x5;y5)(p) * p\^{}imax(x3;y3) - x3(p) * x4 + p\^{}imax(x3;y3) - y3(p) * y4
= p\^{}imax(x3;y3)(p) * p\^{}imax(x5;y5) - x5(p) * x6 + p\^{}imax(x5;y5) - y5(p) * y6
By
Latex:
(RepeatFor 2 (MoveToConcl (-1))
THEN (GenConcl \mkleeneopen{}imax(x5;y5) = M\mkleeneclose{}\mcdot{} THENA Auto)
THEN GenConcl \mkleeneopen{}imax(x3;y3) = N\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index