---

Step * of Lemma qexp_preserves_qless

∀[a,b:ℚ].  (∀[n:ℕ]. a ↑ n < b ↑ n supposing 0 < n) supposing (a < b and (0 ≤ a))
BY
{ xxx(xxxInductionOnNatxxx THEN Auto THEN RWO "exp_unroll_q" 0 THEN Auto THEN (Decide 0 < n - 1 THENA Auto))xxx }

1
1. a : ℚ
2. b : ℚ
3. 0 ≤ a
4. a < b
5. n : ℤ
6. 0 < n
7. a ↑ n - 1 < b ↑ n - 1 supposing 0 < n - 1
8. 0 < n
9. 0 < n - 1
⊢ a ↑ n - 1 * a < b ↑ n - 1 * b

2
1. a : ℚ
2. b : ℚ
3. 0 ≤ a
4. a < b
5. n : ℤ
6. 0 < n
7. a ↑ n - 1 < b ↑ n - 1 supposing 0 < n - 1
8. 0 < n
9. ¬0 < n - 1
⊢ a ↑ n - 1 * a < b ↑ n - 1 * b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    (\mforall{}[n:\mBbbN{}].  a  \muparrow{}  n  <  b  \muparrow{}  n  supposing  0  <  n)  supposing  (a  <  b  and  (0  \mleq{}  a))


By

---

Latex:
xxx(xxxInductionOnNatxxx
        THEN  Auto
        THEN  RWO  "exp\_unroll\_q"  0
        THEN  Auto
        THEN  (Decide  0  <  n  -  1  THENA  Auto))xxx

---

Home Index