---

Step * of Lemma ratLegendre_wf

∀[x:ℤ × ℕ+]. ∀[n:ℕ].  (ratLegendre(n;x) ∈ {y:ℤ × ℕ+| ratreal(y) = Legendre(n;ratreal(x))} )
BY
{ (Auto
   THEN (Assert <1, 1> ∈ {b:ℤ × ℕ+| ratreal(b) = r1}  BY
               (MemTypeCD THEN Auto THEN RWO "ratreal-req" 0 THEN Auto))
   THEN Unfold `ratLegendre` 0
   THEN AutoSplit) }

1
1. x : ℤ × ℕ+
2. n : ℕ
3. <1, 1> ∈ {b:ℤ × ℕ+| ratreal(b) = r1} 
4. n = 0 ∈ ℤ
⊢ <1, 1> ∈ {y:ℤ × ℕ+| ratreal(y) = Legendre(n;ratreal(x))} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].    (ratLegendre(n;x)  \mmember{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(y)  =  Legendre(n;ratreal(x))\}  )


By

---

Latex:
(Auto
  THEN  (Assert  ə,  1>  \mmember{}  \{b:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(b)  =  r1\}    BY
                          (MemTypeCD  THEN  Auto  THEN  RWO  "ratreal-req"  0  THEN  Auto))
  THEN  Unfold  `ratLegendre`  0
  THEN  AutoSplit)

---

Home Index