---

Step * 2 of Lemma ratLegendre-aux_wf


1. [x] : ℤ × ℕ+
2. [n] : ℕ+
3. ∀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))} )
⊢ ∀[tr:k:ℕ+n + 1
       × {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
{ (Intro THEN Unhide THEN (D 3 With ⌜n - fst(tr)⌝  THENA Auto) THEN BHyp -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [x]  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  [n]  :  \mBbbN{}\msupplus{}
3.  \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))\}  )
\mvdash{}  \mforall{}[tr:k:\mBbbN{}\msupplus{}n  +  1
              \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:
(Intro  THEN  Unhide  THEN  (D  3  With  \mkleeneopen{}n  -  fst(tr)\mkleeneclose{}    THENA  Auto)  THEN  BHyp  -1  THEN  Auto)

---

Home Index