---

Step * 2 1 2 of Lemma Moessner-theorem


1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. ∀[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)
     ∈ ℤ)
5. n : ℕ
6. k : ℕ+
7. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0)
                           then 0
                           else (λi.if (i =z 0) then n else 0 fi ) (i - 1)
                           fi ;k)[bag-rep(Σ((λi.if (i =z 0) then n else 0 fi ) i | i < k);x)]
= Π((k - i)^((λi.if (i =z 0) then n else 0 fi ) i) | i < k)
∈ ℤ
8. Π((k - x)^if (x =z 0) then n else 0 fi  | x < k)
= (Π((k - x)^if (x =z 0) then n else 0 fi  | x < 1) * Π((k - x + 1)^if (x + 1 =z 0) then n else 0 fi  | x < k - 1))
∈ ℤ
⊢ k^n = (k^n * Π((k - x + 1)^if (x + 1 =z 0) then n else 0 fi  | x < k - 1)) ∈ ℤ
BY
{ Subst ⌜Π((k - x + 1)^if (x + 1 =z 0) then n else 0 fi  | x < k - 1) ~ 1⌝ 0⋅ }

1
.....equality..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. ∀[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)
     ∈ ℤ)
5. n : ℕ
6. k : ℕ+
7. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0)
                           then 0
                           else (λi.if (i =z 0) then n else 0 fi ) (i - 1)
                           fi ;k)[bag-rep(Σ((λi.if (i =z 0) then n else 0 fi ) i | i < k);x)]
= Π((k - i)^((λi.if (i =z 0) then n else 0 fi ) i) | i < k)
∈ ℤ
8. Π((k - x)^if (x =z 0) then n else 0 fi  | x < k)
= (Π((k - x)^if (x =z 0) then n else 0 fi  | x < 1) * Π((k - x + 1)^if (x + 1 =z 0) then n else 0 fi  | x < k - 1))
∈ ℤ
⊢ Π((k - x + 1)^if (x + 1 =z 0) then n else 0 fi  | x < k - 1) ~ 1

2
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. ∀[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)
     ∈ ℤ)
5. n : ℕ
6. k : ℕ+
7. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0)
                           then 0
                           else (λi.if (i =z 0) then n else 0 fi ) (i - 1)
                           fi ;k)[bag-rep(Σ((λi.if (i =z 0) then n else 0 fi ) i | i < k);x)]
= Π((k - i)^((λi.if (i =z 0) then n else 0 fi ) i) | i < k)
∈ ℤ
8. Π((k - x)^if (x =z 0) then n else 0 fi  | x < k)
= (Π((k - x)^if (x =z 0) then n else 0 fi  | x < 1) * Π((k - x + 1)^if (x + 1 =z 0) then n else 0 fi  | x < k - 1))
∈ ℤ
⊢ k^n = (k^n * 1) ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  Atom
2.  y  :  Atom
3.  \mneg{}(x  =  y)
4.  \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))
5.  n  :  \mBbbN{}
6.  k  :  \mBbbN{}\msupplus{}
7.  Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)
                                                      then  0
                                                      else  (\mlambda{}i.if  (i  =\msubz{}  0)  then  n  else  0  fi  )  (i  -  1)
                                                      fi  ;k)[bag-rep(\mSigma{}((\mlambda{}i.if  (i  =\msubz{}  0)  then  n  else  0  fi  )  i  |  i  <  k);x)]
=  \mPi{}((k  -  i)\^{}((\mlambda{}i.if  (i  =\msubz{}  0)  then  n  else  0  fi  )  i)  |  i  <  k)
8.  \mPi{}((k  -  x)\^{}if  (x  =\msubz{}  0)  then  n  else  0  fi    |  x  <  k)
=  (\mPi{}((k  -  x)\^{}if  (x  =\msubz{}  0)  then  n  else  0  fi    |  x  <  1)
    *  \mPi{}((k  -  x  +  1)\^{}if  (x  +  1  =\msubz{}  0)  then  n  else  0  fi    |  x  <  k  -  1))
\mvdash{}  k\^{}n  =  (k\^{}n  *  \mPi{}((k  -  x  +  1)\^{}if  (x  +  1  =\msubz{}  0)  then  n  else  0  fi    |  x  <  k  -  1))


By

---

Latex:
Subst  \mkleeneopen{}\mPi{}((k  -  x  +  1)\^{}if  (x  +  1  =\msubz{}  0)  then  n  else  0  fi    |  x  <  k  -  1)  \msim{}  1\mkleeneclose{}  0\mcdot{}

---

Home Index