---

Step * of Lemma qexp-non-zero

∀[n:ℕ]. ∀[r:ℚ].  ¬(r ↑ n = 0 ∈ ℚ) supposing ¬(r = 0 ∈ ℚ)
BY
{ xxx(InductionOnNat THEN Auto THEN (RWO "qexp-zero exp_unroll_q" 0 THENA Auto) THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[r:\mBbbQ{}].    \mneg{}(r  \muparrow{}  n  =  0)  supposing  \mneg{}(r  =  0)


By

---

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

---

Home Index