---

Step * of Lemma exp-ratio-property

∀a:ℕ. ∀b:{a + 1...}. ∀k:ℕ.  (exp-ratio(a;b;0;k;1) ∈ {n:ℕ| k * a^n < b^n} )
BY
{ ((UnivCD THENA Auto) THEN Assert ⌜∃m:ℕ. k * a^m < b^m⌝⋅) }

1
.....assertion..... 
1. a : ℕ@i
2. b : {a + 1...}@i
3. k : ℕ@i
⊢ ∃m:ℕ. k * a^m < b^m

2
1. a : ℕ@i
2. b : {a + 1...}@i
3. k : ℕ@i
4. ∃m:ℕ. k * a^m < b^m
⊢ exp-ratio(a;b;0;k;1) ∈ {n:ℕ| k * a^n < b^n} 

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}.  \mforall{}b:\{a  +  1...\}.  \mforall{}k:\mBbbN{}.    (exp-ratio(a;b;0;k;1)  \mmember{}  \{n:\mBbbN{}|  k  *  a\^{}n  <  b\^{}n\}  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}\mexists{}m:\mBbbN{}.  k  *  a\^{}m  <  b\^{}m\mkleeneclose{}\mcdot{})

---

Home Index