---

Step * 1 1 1 1 of Lemma ratLegendre-aux_wf


1. x : ℤ × ℕ+
2. n : ℕ+
3. d : ℤ
4. 0 < d
5. ∀[tr:k:{k:ℕ+| (k + (d - 1)) = n ∈ ℤ} 
        × {a:ℤ × ℕ+| ratreal(a) = Legendre(k;ratreal(x))} 
        × {b:ℤ × ℕ+| ratreal(b) = Legendre(k - 1;ratreal(x))} ]
     (ratLegendre-aux(n;x;tr) ∈ {y:ℤ × ℕ+| ratreal(y) = Legendre(n;ratreal(x))} )
6. k : ℕ+
7. (k + d) = n ∈ ℤ
8. t2 : ℤ × ℕ+
9. ratreal(t2) = Legendre(k;ratreal(x))
10. t3 : ℤ × ℕ+
11. ratreal(t3) = Legendre(k - 1;ratreal(x))
12. ¬(k = n ∈ ℤ)
⊢ -k * ratreal(t3) = -(k * ratreal(t3))
BY
{ (RWW "int-rmul-req rminus-int<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  n  :  \mBbbN{}\msupplus{}
3.  d  :  \mBbbZ{}
4.  0  <  d
5.  \mforall{}[tr:k:\{k:\mBbbN{}\msupplus{}|  (k  +  (d  -  1))  =  n\} 
                \mtimes{}  \{a:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(a)  =  Legendre(k;ratreal(x))\} 
                \mtimes{}  \{b:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(b)  =  Legendre(k  -  1;ratreal(x))\}  ]
          (ratLegendre-aux(n;x;tr)  \mmember{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(y)  =  Legendre(n;ratreal(x))\}  )
6.  k  :  \mBbbN{}\msupplus{}
7.  (k  +  d)  =  n
8.  t2  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
9.  ratreal(t2)  =  Legendre(k;ratreal(x))
10.  t3  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
11.  ratreal(t3)  =  Legendre(k  -  1;ratreal(x))
12.  \mneg{}(k  =  n)
\mvdash{}  -k  *  ratreal(t3)  =  -(k  *  ratreal(t3))


By

---

Latex:
(RWW  "int-rmul-req  rminus-int<"  0  THEN  Auto)

---

Home Index