Pi/Real cosine function/Definition

Let ${\displaystyle {}s}$ denote the unique (according to fact) real zero of the cosine function in the interval ${\displaystyle {}[0,2]}$. Then the number ${\displaystyle {}\pi }$ is defined by

${\displaystyle {}\pi$ :=2s\,.}