---

Step * of Lemma 2-MachinPi4

2 * MachinPi4() = π/2
BY
{ (GenConclTerm ⌜MachinPi4()⌝⋅ THENA Auto) }

1
1. v : {x:ℝ| x = (π/r(4))} 
2. MachinPi4() = v ∈ {x:ℝ| x = (π/r(4))} 
⊢ 2 * v = π/2

---

Latex:

---

Latex:
2  *  MachinPi4()  =  \mpi{}/2


By

---

Latex:
(GenConclTerm  \mkleeneopen{}MachinPi4()\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index