---

Step * 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 ∈ ℤ)
⊢ ratreal(rat-nat-div(ratadd(int-rat-mul((2 * k) + 1;ratmul(x;t2));int-rat-mul(-k;t3));k + 1))
= ((2 * k) + 1 * ratreal(x) * Legendre(k;ratreal(x)) - k * Legendre(k - 1;ratreal(x)))/k + 1
BY
{ (RW (AddrC [1] ratreal_pushdownC) 0 THENA Auto) }

1
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 ∈ ℤ)
⊢ ((2 * k) + 1 * ratreal(x) * ratreal(t2) + -k * ratreal(t3))/k + 1
= ((2 * k) + 1 * ratreal(x) * Legendre(k;ratreal(x)) - k * Legendre(k - 1;ratreal(x)))/k + 1

---

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{}  ratreal(rat-nat-div(ratadd(int-rat-mul((2  *  k)  +  1;ratmul(x;t2));int-rat-mul(-k;t3));k  +  1))
=  ((2  *  k)  +  1  *  ratreal(x)  *  Legendre(k;ratreal(x))  -  k  *  Legendre(k  -  1;ratreal(x)))/k  +  1


By

---

Latex:
(RW  (AddrC  [1]  ratreal\_pushdownC)  0  THENA  Auto)

---

Home Index