---

Step * of Lemma qexp-le-one

∀[a:ℚ]. ∀[n:ℕ]. (a ↑ n ≤ 1) supposing (0 ≤ a) ∧ (a ≤ 1)
BY
{ (InductionOnNat THEN (RWO "qexp-zero exp_unroll_q" 0 THENA Auto)) }

1
1. a : ℚ
2. (0 ≤ a) ∧ (a ≤ 1)
3. n : ℤ
⊢ 1 ≤ 1

2
1. a : ℚ
2. (0 ≤ a) ∧ (a ≤ 1)
3. n : ℤ
4. 0 < n
5. a ↑ n - 1 ≤ 1
⊢ (a ↑ n - 1 * a) ≤ 1

---

Latex:

---

Latex:
\mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].  (a  \muparrow{}  n  \mleq{}  1)  supposing  (0  \mleq{}  a)  \mwedge{}  (a  \mleq{}  1)


By

---

Latex:
(InductionOnNat  THEN  (RWO  "qexp-zero  exp\_unroll\_q"  0  THENA  Auto))

---

Home Index