---

Step * of Lemma ratLegendre-aux_wf

∀[x:ℤ × ℕ+]. ∀[n:ℕ+]. ∀[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
{ (RepeatFor 2 (Intro)
   THEN Assert ⌜∀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))} )⌝⋅
   ) }

1
.....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))} )

2
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))} )

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \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:
(RepeatFor  2  (Intro)
  THEN  Assert  \mkleeneopen{}\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))\}  )\mkleeneclose{}\mcdot{}
  )

---

Home Index