Step
*
1
1
of Lemma
expfact_wf
.....truecase.....
1. m : ℕ+
2. k : ℕ
3. n : ℕ+
4. b : {b:ℕ| n * k^b < (b)!} @i
5. m ≤ b@i
6. d : ℤ
7. 0 < b@i
8. (n * k^b - 0) ≤ (b - 0)!
⊢ b - 0 ∈ {b:ℕ+| (n * k^b) ≤ (b)!}
BY
{ Auto }
Latex:
Latex:
.....truecase.....
1. m : \mBbbN{}\msupplus{}
2. k : \mBbbN{}
3. n : \mBbbN{}\msupplus{}
4. b : \{b:\mBbbN{}| n * k\^{}b < (b)!\} @i
5. m \mleq{} b@i
6. d : \mBbbZ{}
7. 0 < b@i
8. (n * k\^{}b - 0) \mleq{} (b - 0)!
\mvdash{} b - 0 \mmember{} \{b:\mBbbN{}\msupplus{}| (n * k\^{}b) \mleq{} (b)!\}
By
Latex:
Auto
Home
Index