---

Step * 1 1 of Lemma div_rec_case


1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. ∃q:ℕ. (Div(a;n;q) ∧ ((a ÷ n) = q ∈ ℤ))
5. ∃q:ℕ. (Div(a - n;n;q) ∧ (((a - n) ÷ n) = q ∈ ℤ))
⊢ (a ÷ n) = (((a - n) ÷ n) + 1) ∈ ℤ
BY
{ (((D 5 THEN D 6) THEN DVars [`p'] 4) THEN D 5) }

1
1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. p : ℕ
5. Div(a;n;p)
6. (a ÷ n) = p ∈ ℤ
7. q : ℕ
8. Div(a - n;n;q)
9. ((a - n) ÷ n) = q ∈ ℤ
⊢ (a ÷ n) = (((a - n) ÷ n) + 1) ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  a  \mgeq{}  n 
4.  \mexists{}q:\mBbbN{}.  (Div(a;n;q)  \mwedge{}  ((a  \mdiv{}  n)  =  q))
5.  \mexists{}q:\mBbbN{}.  (Div(a  -  n;n;q)  \mwedge{}  (((a  -  n)  \mdiv{}  n)  =  q))
\mvdash{}  (a  \mdiv{}  n)  =  (((a  -  n)  \mdiv{}  n)  +  1)


By

---

Latex:
(((D  5  THEN  D  6)  THEN  DVars  [`p']  4)  THEN  D  5)

---

Home Index