---

Step * of Lemma decidable__exists-divisor

∀n:ℕ+. ∀P:ℕ ⟶ ℙ.  ((∀d:ℕ. Dec(P[d])) ⇒ Dec(∃d:ℕ. ((d | n) ∧ P[d])))
BY
{ (Auto
   THEN (InstLemma `decidable__exists_int_seg` [⌜parm{i}⌝;⌜0⌝;⌜n + 1⌝;⌜λ2d.(d | n) ∧ P[d]⌝]⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast)) }

1
1. n : ℕ+
2. P : ℕ ⟶ ℙ
3. ∀d:ℕ. Dec(P[d])
4. d : ℤ
5. 0 ≤ d
6. d | n
7. P[d]
⊢ d < n + 1

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.    ((\mforall{}d:\mBbbN{}.  Dec(P[d]))  {}\mRightarrow{}  Dec(\mexists{}d:\mBbbN{}.  ((d  |  n)  \mwedge{}  P[d])))


By

---

Latex:
(Auto
  THEN  (InstLemma  `decidable\_\_exists\_int\_seg`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}d.(d  |  n)  \mwedge{}  P[d]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepeatFor  4  (ParallelLast))

---

Home Index