---

Step * of Lemma cbva-intro-test3

∀x:ℤ. {y:ℤ| x * x < y} 
BY
{ ((cbvaAllIntro THENA Auto) THEN With ⌜(x * x) + 1⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  \{y:\mBbbZ{}|  x  *  x  <  y\} 


By

---

Latex:
((cbvaAllIntro  THENA  Auto)  THEN  With  \mkleeneopen{}(x  *  x)  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index