Step * of Lemma log-property

[b:{i:ℤ1 < i} ]. ∀[x:ℕ].  (b^log(b;x) ≤ x) ∧ x < b^log(b;x) supposing 0 < x
BY
CompleteInductionOnNat
THEN (D THENA Auto)
THEN RecUnfold `log` 0
THEN OldAutoSplit }

1
1. {i:ℤ1 < i} 
2. : ℕ
3. ∀x:ℕx. (b^log(b;x) ≤ x) ∧ x < b^log(b;x) supposing 0 < x
4. 0 < x
5. b ≤ x
⊢ (b^log(b;x ÷ b) 1 ≤ x) ∧ x < b^(log(b;x ÷ b) 1) 1


Latex:


Latex:
\mforall{}[b:\{i:\mBbbZ{}|  1  <  i\}  ].  \mforall{}[x:\mBbbN{}].    (b\^{}log(b;x)  \mleq{}  x)  \mwedge{}  x  <  b\^{}log(b;x)  +  1  supposing  0  <  x


By


Latex:
CompleteInductionOnNat
THEN  (D  0  THENA  Auto)
THEN  RecUnfold  `log`  0
THEN  OldAutoSplit




Home Index