---

Step * of Lemma exp_functionality_wrt_le_1

∀[b:ℕ+]. ∀[x,y:ℕ].  b^x ≤ b^y supposing x ≤ y
BY
{ (Auto
   THEN (Subst' y ~ x + (y - x) 0 THENA Auto)
   THEN (GenConcl ⌜(y - x) = m ∈ ℕ⌝⋅ THENA Auto)
   THEN (RWO "exp_add" 0 THENA Auto)
   THEN (Assert 1 ≤ b^m BY
               Auto)
   THEN Mul ⌜b^x⌝ (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}\msupplus{}].  \mforall{}[x,y:\mBbbN{}].    b\^{}x  \mleq{}  b\^{}y  supposing  x  \mleq{}  y


By

---

Latex:
(Auto
  THEN  (Subst'  y  \msim{}  x  +  (y  -  x)  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(y  -  x)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "exp\_add"  0  THENA  Auto)
  THEN  (Assert  1  \mleq{}  b\^{}m  BY
                          Auto)
  THEN  Mul  \mkleeneopen{}b\^{}x\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index