---

Step * of Lemma Legendre-zero-odd

∀n:ℕ. Legendre(n;r0) = r0 supposing (n rem 2) = 1 ∈ ℤ
BY
{ (Auto THEN InstLemma `Legendre-rminus` [⌜n⌝;⌜r0⌝]⋅ THEN Auto) }

1
1. n : ℕ
2. (n rem 2) = 1 ∈ ℤ
3. Legendre(n;-(r0)) = (r(-1)^n * Legendre(n;r0))
⊢ Legendre(n;r0) = r0

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  Legendre(n;r0)  =  r0  supposing  (n  rem  2)  =  1


By

---

Latex:
(Auto  THEN  InstLemma  `Legendre-rminus`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index