---

Step * of Lemma gen_log_aux_wf

∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
  (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} )
BY
{ Assert ⌜∀d:ℕ
            ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
              ((M ≤ (d + (c * p))) ⇒ (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} \000C))⌝⋅ }

1
.....assertion..... 
∀d:ℕ
  ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
    ((M ≤ (d + (c * p))) ⇒ (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} ))

2
1. ∀d:ℕ
     ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
       ((M ≤ (d + (c * p))) ⇒ (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} ))
⊢ ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
    (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} )

---

Latex:

---

Latex:
\mforall{}[p,c:\mBbbN{}\msupplus{}].  \mforall{}[x:\{2...\}].  \mforall{}[i,n:\mBbbN{}].  \mforall{}[M:\mBbbZ{}].
    (gen\_log\_aux(p;c;x;i;n;M)  \mmember{}  \{k:\{n...\}|  M  \mleq{}  ((c  +  ((k  -  n)  *  i))  *  p  *  x\^{}(k  -  n))\}  )


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}
                    \mforall{}[p,c:\mBbbN{}\msupplus{}].  \mforall{}[x:\{2...\}].  \mforall{}[i,n:\mBbbN{}].  \mforall{}[M:\mBbbZ{}].
                        ((M  \mleq{}  (d  +  (c  *  p)))
                        {}\mRightarrow{}  (gen\_log\_aux(p;c;x;i;n;M)  \mmember{}  \{k:\{n...\}|  M  \mleq{}  ((c  +  ((k  -  n)  *  i))  *  p  *  x\^{}(k  -  n))\}  ))\mkleeneclose{}\000C\mcdot{}

---

Home Index