---

Step * of Lemma rng_prod_const_mul

∀[r:CRng]. ∀[c:|r|]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|].  ((Π(r) 0 ≤ i < n. F[i] * c) = ((c ↑r n) * (Π(r) 0 ≤ i < n. F[i])) ∈ |r|)
BY
{ (InductionOnNat THEN Auto) }

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

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

---

Latex:

---

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


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index