Step * 1 of Lemma Paasche-theorem


1. Atom
2. Atom
3. ¬(x y ∈ Atom)
4. : ℕ
5. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then else i.1) (i 1) fi ;k)[bag-rep(Σ((λi.1) i < k);x)]
= Π((k i)^((λi.1) i) i < k)
∈ ℤ
6. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
     (Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then else (i 1) fi ;k)[bag-rep(Σ(d i < k);x)]
     = Π((k i)^(d i) i < k)
     ∈ ℤ)
⊢ Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then else fi ;k)[bag-rep(k;x)]
Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then else i.1) (i 1) fi ;k)[bag-rep(Σ((λi.1) i < k);x)]
∈ ℤ
BY
(RepeatFor ((EqCD THEN Auto))⋅ THEN Reduce THEN RWO "sum_constant" THEN Auto) }


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.1)  (i  -  1)  fi  ;k)[bag-rep(\mSigma{}((\mlambda{}i.1) 
                                                                                                                                                                      i  |  i  <  k);x)]
=  \mPi{}((k  -  i)\^{}((\mlambda{}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{}  Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  1  fi  ;k)[bag-rep(k;x)]
=  Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  (\mlambda{}i.1)  (i  -  1)  fi  ;k)[bag-rep(\mSigma{}((\mlambda{}i.1) 
                                                                                                                                                                    i  |  i  <  k);x)]


By


Latex:
(RepeatFor  2  ((EqCD  THEN  Auto))\mcdot{}  THEN  Reduce  0  THEN  RWO  "sum\_constant"  0  THEN  Auto)




Home Index