---

Step * 1 of Lemma rnexp-even-nonneg


1. n : ℕ
2. (n rem 2) = 0 ∈ ℤ
3. x : ℝ
⊢ n = (2 * (n ÷ 2)) ∈ ℕ
BY
{ (InstLemma `div_rem_sum` [⌜n⌝;⌜2⌝]⋅ THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  (n  rem  2)  =  0
3.  x  :  \mBbbR{}
\mvdash{}  n  =  (2  *  (n  \mdiv{}  2))


By

---

Latex:
(InstLemma  `div\_rem\_sum`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Auto')

---

Home Index