---

Step * 1 of Lemma ratLegendre-aux_wf

.....assertion..... 
1. [x] : ℤ × ℕ+
2. [n] : ℕ+
⊢ ∀d:ℕ
    ∀[tr:k:{k:ℕ+| (k + d) = 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))} )
BY
{ (InductionOnNat
   THEN Intro
   THEN Unhide
   THEN RepeatFor 2 (D -1)
   THEN DSetVars
   THEN Unfold `ratLegendre-aux` 0
   THEN Reduce 0
   THEN (((Assert ¬(k = n ∈ ℤ) BY
                 Complete (Auto))
          THEN Reduce 0
          THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
          THEN BHyp 5
          THEN (MemCD THENA Auto)
          THEN Try ((MemTypeCD THEN Auto))
          THEN MemCD
          THEN MemTypeCD
          THEN Auto
          THEN Unfold `Legendre` 0
          THEN (Subst' (k + 1 =z 0) ~ ff 0 THENA Auto)
          THEN (Subst' (k + 1 =z 1) ~ ff 0 THENA Auto)
          THEN Reduce 0
          THEN (Subst' (k + 1) - 2 ~ k - 1 0 THENA Auto)
          THEN (Subst' (k + 1) - 1 ~ k 0 THENA Auto)
          THEN (Subst' (2 * (k + 1)) - 1 ~ (2 * k) + 1 0 THENA Auto))
   ORELSE ((Assert k = n ∈ ℤ BY Auto) THEN Reduce 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 ∈ ℤ)
⊢ 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

---

Latex:

---

Latex:
.....assertion..... 
1.  [x]  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  [n]  :  \mBbbN{}\msupplus{}
\mvdash{}  \mforall{}d:\mBbbN{}
        \mforall{}[tr:k:\{k:\mBbbN{}\msupplus{}|  (k  +  d)  =  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))\}  )


By

---

Latex:
(InductionOnNat
  THEN  Intro
  THEN  Unhide
  THEN  RepeatFor  2  (D  -1)
  THEN  DSetVars
  THEN  Unfold  `ratLegendre-aux`  0
  THEN  Reduce  0
  THEN  (((Assert  \mneg{}(k  =  n)  BY
                              Complete  (Auto))
                THEN  Reduce  0
                THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                THEN  BHyp  5
                THEN  (MemCD  THENA  Auto)
                THEN  Try  ((MemTypeCD  THEN  Auto))
                THEN  MemCD
                THEN  MemTypeCD
                THEN  Auto
                THEN  Unfold  `Legendre`  0
                THEN  (Subst'  (k  +  1  =\msubz{}  0)  \msim{}  ff  0  THENA  Auto)
                THEN  (Subst'  (k  +  1  =\msubz{}  1)  \msim{}  ff  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (Subst'  (k  +  1)  -  2  \msim{}  k  -  1  0  THENA  Auto)
                THEN  (Subst'  (k  +  1)  -  1  \msim{}  k  0  THENA  Auto)
                THEN  (Subst'  (2  *  (k  +  1))  -  1  \msim{}  (2  *  k)  +  1  0  THENA  Auto))
  ORELSE  ((Assert  k  =  n  BY  Auto)  THEN  Reduce  0  THEN  Auto)
  ))

---

Home Index