---

Step * 1 of Lemma decidable__exists-divisor


1. n : ℕ+
2. P : ℕ ⟶ ℙ
3. ∀d:ℕ. Dec(P[d])
4. d : ℤ
5. 0 ≤ d
6. d | n
7. P[d]
⊢ d < n + 1
BY
{ (FLemma `divisors_bound` [-2] THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}d:\mBbbN{}.  Dec(P[d])
4.  d  :  \mBbbZ{}
5.  0  \mleq{}  d
6.  d  |  n
7.  P[d]
\mvdash{}  d  <  n  +  1


By

---

Latex:
(FLemma  `divisors\_bound`  [-2]  THEN  Auto)

---

Home Index