---

Step * of Lemma rng_prod_unroll_hi

∀[r:CRng]. ∀[n:ℕ+]. ∀[F:ℕn ⟶ |r|].  ((Π(r) 0 ≤ i < n. F[i]) = ((Π(r) 0 ≤ i < n - 1. F[i]) * F[n - 1]) ∈ |r|)
BY
{ (Intros THEN CaseNat 1 `n') }

1
1. r : CRng
2. n : ℕ+
3. F : ℕn ⟶ |r|
4. n = 1 ∈ ℤ
⊢ (Π(r) 0 ≤ i < 1. F[i]) = ((Π(r) 0 ≤ i < 1 - 1. F[i]) * F[1 - 1]) ∈ |r|

2
1. r : CRng
2. n : ℕ+
3. F : ℕn ⟶ |r|
4. ¬(n = 1 ∈ ℤ)
⊢ (Π(r) 0 ≤ i < n. F[i]) = ((Π(r) 0 ≤ i < n - 1. F[i]) * F[n - 1]) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[F:\mBbbN{}n  {}\mrightarrow{}  |r|].
    ((\mPi{}(r)  0  \mleq{}  i  <  n.  F[i])  =  ((\mPi{}(r)  0  \mleq{}  i  <  n  -  1.  F[i])  *  F[n  -  1]))


By

---

Latex:
(Intros  THEN  CaseNat  1  `n')

---

Home Index