---

Step * of Lemma super-fact-int-prod-exp

∀[k:ℕ]. ((k)!! = Π(k - i^i + 1 | i < k) ∈ ℤ)
BY
{ (InductionOnNat THEN Auto THEN (RWO "super-fact-unroll" 0 THENA Auto) THEN HypSubst' (-1) 0 THEN Thin (-1)) }

1
1. k : ℤ
2. 0 < k
⊢ ((k)! * Π(k - 1 - i^i + 1 | i < k - 1)) = Π(k - i^i + 1 | i < k) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  ((k)!!  =  \mPi{}(k  -  i\^{}i  +  1  |  i  <  k))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  (RWO  "super-fact-unroll"  0  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1))

---

Home Index