Step
*
1
2
of Lemma
expfact_wf
.....falsecase.....
1. m : ℕ+
2. k : ℕ
3. n : ℕ+
4. b : {b:ℕ| n * k^b < (b)!}
5. m ≤ b
6. d : ℤ
7. 0 < b
8. (b - 0)! < n * k^(b - 0)
⊢ eval n' = (b - 0) + 1 in
eval p' = k * n * k^(b - 0) in
eval b' = n' * (b - 0)! in
expfact(n';k;p';b') ∈ {b:ℕ+| (n * k^b) ≤ (b)!}
BY
{ (RW IntNormC (-1) THEN Auto) }
Latex:
Latex:
.....falsecase.....
1. m : \mBbbN{}\msupplus{}
2. k : \mBbbN{}
3. n : \mBbbN{}\msupplus{}
4. b : \{b:\mBbbN{}| n * k\^{}b < (b)!\}
5. m \mleq{} b
6. d : \mBbbZ{}
7. 0 < b
8. (b - 0)! < n * k\^{}(b - 0)
\mvdash{} eval n' = (b - 0) + 1 in
eval p' = k * n * k\^{}(b - 0) in
eval b' = n' * (b - 0)! in
expfact(n';k;p';b') \mmember{} \{b:\mBbbN{}\msupplus{}| (n * k\^{}b) \mleq{} (b)!\}
By
Latex:
(RW IntNormC (-1) THEN Auto)
Home
Index