---

Step * 1 of Lemma num-digits_wf


1. k : ℕ
2. ∀k:ℕk. (num-digits(k) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
3. k < 10
⊢ 1 ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} 
BY
{ ((MemTypeCD THEN Auto) THEN Reduce 0 THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  \mforall{}k:\mBbbN{}k.  (num-digits(k)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\}  )
3.  k  <  10
\mvdash{}  1  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\} 


By

---

Latex:
((MemTypeCD  THEN  Auto)  THEN  Reduce  0  THEN  Auto')

---

Home Index