---

Step * 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 ∈ ℤ)
⊢ ((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
BY
{ (Unfold `rsub` 0
   THEN (BLemma `int-rdiv_functionality` THEN Auto)
   THEN BLemma `radd_functionality`
   THEN Auto
   THEN RWO "9< 11<" 0
   THEN 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 ∈ ℤ)
⊢ -k * ratreal(t3) = -(k * ratreal(t3))

---

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{}  ((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


By

---

Latex:
(Unfold  `rsub`  0
  THEN  (BLemma  `int-rdiv\_functionality`  THEN  Auto)
  THEN  BLemma  `radd\_functionality`
  THEN  Auto
  THEN  RWO  "9<  11<"  0
  THEN  Auto)

---

Home Index