---

Step * of Lemma pi-irrational-instance

∃k:ℕ. (((r1)/k + 2 < |(r(22))/7 - 4 * MachinPi4()|) ∧ (|(r(22))/7 - 4 * MachinPi4()| < (r1)/k + 1))
BY
{ ((D 0 With ⌜789⌝  THENW Auto)
   THEN D 0
   THEN (D 0 With ⌜30000000⌝  THENA Auto)
   THEN RW (SubC (TagC (mk_tag_term 0))) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mexists{}k:\mBbbN{}.  (((r1)/k  +  2  <  |(r(22))/7  -  4  *  MachinPi4()|)  \mwedge{}  (|(r(22))/7  -  4  *  MachinPi4()|  <  (r1)/k  +  1))


By

---

Latex:
((D  0  With  \mkleeneopen{}789\mkleeneclose{}    THENW  Auto)
  THEN  D  0
  THEN  (D  0  With  \mkleeneopen{}30000000\mkleeneclose{}    THENA  Auto)
  THEN  RW  (SubC  (TagC  (mk\_tag\_term  0)))  0
  THEN  Auto)

---

Home Index