---

Step * 1 1 of Lemma Paasche-theorem2


1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℕ
5. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then 0 else (λi.(i + 1)) (i - 1) fi ;k)[bag-rep(Σ((λi.(i + 1)) i | i < k);x)]
= Π((k - i)^((λi.(i + 1)) i) | i < k)
∈ ℤ
6. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
     (Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then 0 else d (i - 1) fi ;k)[bag-rep(Σ(d i | i < k);x)]
     = Π((k - i)^(d i) | i < k)
     ∈ ℤ)
⊢ ((k * (1 + k)) ÷ 2) = Σ(i + 1 | i < k) ∈ ℕ
BY
{ ((Assert Σ(i + 1 | i < k) = ((k * (1 + k)) ÷ 2) ∈ ℤ BY
          ((InstLemma `sum_arith` [⌜k⌝;⌜1⌝;⌜1⌝]⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCD THEN Auto))
   THEN RevHypSubst' (-1) 0
   THEN Fold `member` 0
   THEN MemTypeCD
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  x  :  Atom
2.  y  :  Atom
3.  \mneg{}(x  =  y)
4.  k  :  \mBbbN{}
5.  Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)
                                                      then  0
                                                      else  (\mlambda{}i.(i  +  1))  (i  -  1)
                                                      fi  ;k)[bag-rep(\mSigma{}((\mlambda{}i.(i  +  1))  i  |  i  <  k);x)]
=  \mPi{}((k  -  i)\^{}((\mlambda{}i.(i  +  1))  i)  |  i  <  k)
6.  \mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
          (Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  d  (i  -  1)  fi  ;k)[bag-rep(\mSigma{}(d  i  |  i  <  k);x)]
          =  \mPi{}((k  -  i)\^{}(d  i)  |  i  <  k))
\mvdash{}  ((k  *  (1  +  k))  \mdiv{}  2)  =  \mSigma{}(i  +  1  |  i  <  k)


By

---

Latex:
((Assert  \mSigma{}(i  +  1  |  i  <  k)  =  ((k  *  (1  +  k))  \mdiv{}  2)  BY
                ((InstLemma  `sum\_arith`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Auto))
  THEN  RevHypSubst'  (-1)  0
  THEN  Fold  `member`  0
  THEN  MemTypeCD
  THEN  EAuto  1)

---

Home Index