---

Step * 2 1 1 1 1 of Lemma num-digits_wf


1. k : ℕ
2. ¬k < 10
3. ∀k:ℕk. (num-digits(k) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
4. k = (((k ÷ 10) * 10) + (k rem 10)) ∈ ℤ
5. (0 ≤ (k rem 10)) ∧ k rem 10 < 10
6. v : ℕ+
7. (10^v - 1 ≤ (k ÷ 10)) ∨ ((k ÷ 10) = 0 ∈ ℤ)
8. k ÷ 10 < 10^v
⊢ ((10^v ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^1 + v
BY
{ (Subst' 10^1 + v ~ 10 * 10^v 0 THEN Auto) }

1
1. k : ℕ
2. ¬k < 10
3. ∀k:ℕk. (num-digits(k) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
4. k = (((k ÷ 10) * 10) + (k rem 10)) ∈ ℤ
5. 0 ≤ (k rem 10)
6. k rem 10 < 10
7. v : ℕ+
8. (10^v - 1 ≤ (k ÷ 10)) ∨ ((k ÷ 10) = 0 ∈ ℤ)
9. k ÷ 10 < 10^v
⊢ (10^v ≤ k) ∨ (k = 0 ∈ ℤ)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  \mneg{}k  <  10
3.  \mforall{}k:\mBbbN{}k.  (num-digits(k)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\}  )
4.  k  =  (((k  \mdiv{}  10)  *  10)  +  (k  rem  10))
5.  (0  \mleq{}  (k  rem  10))  \mwedge{}  k  rem  10  <  10
6.  v  :  \mBbbN{}\msupplus{}
7.  (10\^{}v  -  1  \mleq{}  (k  \mdiv{}  10))  \mvee{}  ((k  \mdiv{}  10)  =  0)
8.  k  \mdiv{}  10  <  10\^{}v
\mvdash{}  ((10\^{}v  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}1  +  v


By

---

Latex:
(Subst'  10\^{}1  +  v  \msim{}  10  *  10\^{}v  0  THEN  Auto)

---

Home Index