---

Step * of Lemma Paasche-theorem2

∀[x,y:Atom].  ∀[k:ℕ]. (Moessner(ℤ-rng;x;y;1;λi.i;k)[bag-rep((k * (1 + k)) ÷ 2;x)] = (k)!! ∈ ℤ) supposing ¬(x = y ∈ Atom)
BY
{ xxx(InstLemma `KozenSilva-corollary2` []
      THEN RepeatFor 2 (ParallelLast')
      THEN (D 0 THENA Auto)
      THEN (InstHyp [⌜λi.(i + 1)⌝] (-2)⋅ THENA Auto)
      THEN ParallelLast'
      THEN NthHypEq (-1)
      THEN EqCD
      THEN Auto)xxx }

1
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)
     ∈ ℤ)
⊢ Moessner(ℤ-rng;x;y;1;λi.i;k)[bag-rep((k * (1 + k)) ÷ 2;x)]
= 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)]
∈ ℤ

2
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)!! = Π((k - i)^((λi.(i + 1)) i) | i < k) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[x,y:Atom].
    \mforall{}[k:\mBbbN{}].  (Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.i;k)[bag-rep((k  *  (1  +  k))  \mdiv{}  2;x)]  =  (k)!!)  supposing  \mneg{}(x  =  y)


By

---

Latex:
xxx(InstLemma  `KozenSilva-corollary2`  []
        THEN  RepeatFor  2  (ParallelLast')
        THEN  (D  0  THENA  Auto)
        THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.(i  +  1)\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
        THEN  ParallelLast'
        THEN  NthHypEq  (-1)
        THEN  EqCD
        THEN  Auto)xxx

---

Home Index