---

Step * 2 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} )
⊢ 1 + num-digits(k ÷ 10) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} 
BY
{ ((InstLemma `div_rem_sum` [⌜k⌝;⌜10⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜k⌝;⌜10⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜k ÷ 10⌝] (3)⋅ THENA 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)) ∧ k rem 10 < 10
6. num-digits(k ÷ 10) ∈ {n:ℕ+| ((10^n - 1 ≤ (k ÷ 10)) ∨ ((k ÷ 10) = 0 ∈ ℤ)) ∧ k ÷ 10 < 10^n} 
⊢ 1 + num-digits(k ÷ 10) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} 

---

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\}  )
\mvdash{}  1  +  num-digits(k  \mdiv{}  10)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\} 


By

---

Latex:
((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}10\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}10\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}k  \mdiv{}  10\mkleeneclose{}]  (3)\mcdot{}  THENA  Auto))

---

Home Index