Step * of Lemma combinations_aux_linear

[n:ℕ]. ∀[b,m:ℤ].  (combinations_aux(b;n;m) (b combinations_aux(1;n;m)) ∈ ℤ)
BY
(InductionOnNat THEN RecUnfold `combinations_aux` THEN Reduce 0)⋅ }

1
1. : ℤ
⊢ ∀[b,m:ℤ].  (b (b 1) ∈ ℤ)

2
1. : ℤ
2. 0 < n
3. ∀[b,m:ℤ].  (combinations_aux(b;n 1;m) (b combinations_aux(1;n 1;m)) ∈ ℤ)
⊢ ∀[b,m:ℤ].
    (if (n =z 0) then else eval b2 in eval n2 in eval m2 in   combinations_aux(b2;n2;m2) fi 
    (b
      if (n =z 0)
        then 1
        else eval b2 in
             eval n2 in
             eval m2 in
               combinations_aux(b2;n2;m2)
        fi )
    ∈ ℤ)


Latex:


Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[b,m:\mBbbZ{}].    (combinations\_aux(b;n;m)  =  (b  *  combinations\_aux(1;n;m)))


By


Latex:
(InductionOnNat  THEN  RecUnfold  `combinations\_aux`  0  THEN  Reduce  0)\mcdot{}




Home Index