---

Step * 1 of Lemma Legendre-1


1. n : {1...}
2. ∀n:ℕn. (Legendre(n;r1) = r1)
3. ¬(n = 0 ∈ ℤ)
4. ¬(n = 1 ∈ ℤ)
⊢ ((2 * n) - 1 * r1 * r1 - n - 1 * r1)/n = r1
BY
{ ((RWO "int-rdiv-req" 0 THENA Auto) THEN (RWO "int-rmul-req" 0 THENA Auto) THEN nRMul ⌜r(n)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  \mforall{}n:\mBbbN{}n.  (Legendre(n;r1)  =  r1)
3.  \mneg{}(n  =  0)
4.  \mneg{}(n  =  1)
\mvdash{}  ((2  *  n)  -  1  *  r1  *  r1  -  n  -  1  *  r1)/n  =  r1


By

---

Latex:
((RWO  "int-rdiv-req"  0  THENA  Auto)
  THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
  THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index