---

Step * of Lemma halfpi_wf1

π/2 ∈ {x:ℝ| x = π/2(slower)} 
BY
{ ((InstLemma `req-from-converges` 
       [⌜λ2n.fastpi(n)⌝;⌜π/2(slower)⌝;⌜TERMOF{fastpi-converges-ext:o, \\v:l}⌝]⋅
    THENA Auto
    )
   THEN Assert ⌜π/2 = cauchy-limit(n.fastpi(n);λk.(TERMOF{fastpi-converges-ext:o, \\v:l} (2 * k))) ∈ (ℕ+ ⟶ ℤ)⌝⋅
   ) }

1
.....assertion..... 
1. π/2(slower) = cauchy-limit(n.fastpi(n);λk.(TERMOF{fastpi-converges-ext:o, \\v:l} (2 * k)))
⊢ π/2 = cauchy-limit(n.fastpi(n);λk.(TERMOF{fastpi-converges-ext:o, \\v:l} (2 * k))) ∈ (ℕ+ ⟶ ℤ)

2
1. π/2(slower) = cauchy-limit(n.fastpi(n);λk.(TERMOF{fastpi-converges-ext:o, \\v:l} (2 * k)))
2. π/2 = cauchy-limit(n.fastpi(n);λk.(TERMOF{fastpi-converges-ext:o, \\v:l} (2 * k))) ∈ (ℕ+ ⟶ ℤ)
⊢ π/2 ∈ {x:ℝ| x = π/2(slower)} 

---

Latex:

---

Latex:
\mpi{}/2  \mmember{}  \{x:\mBbbR{}|  x  =  \mpi{}/2(slower)\} 


By

---

Latex:
((InstLemma  `req-from-converges` 
          [\mkleeneopen{}\mlambda{}\msubtwo{}n.fastpi(n)\mkleeneclose{};\mkleeneopen{}\mpi{}/2(slower)\mkleeneclose{};\mkleeneopen{}TERMOF\{fastpi-converges-ext:o,  \mbackslash{}\mbackslash{}v:l\}\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Assert  \mkleeneopen{}\mpi{}/2  =  cauchy-limit(n.fastpi(n);\mlambda{}k.(TERMOF\{fastpi-converges-ext:o,  \mbackslash{}\mbackslash{}v:l\}  (2  *  k)))\mkleeneclose{}\mcdot{}
  )

---

Home Index