let r be real number ; :: thesis: ( 0 <= r & r <= 2 * PI & sin r = - 1 implies r = (3 / 2) * PI )
assume that
A1: 0 <= r and
A2: r <= 2 * PI and
A3: sin r = - 1 ; :: thesis: r = (3 / 2) * PI
A4: ( r = 2 * PI or r < 2 * PI ) by A2, XXREAL_0:1;
thus r = ((3 / 2) * PI ) + ((2 * PI ) * [\(r / (2 * PI ))/]) by A3, Th23
.= ((3 / 2) * PI ) + ((2 * PI ) * 0 ) by A1, A3, A4, Th1, SIN_COS:82
.= (3 / 2) * PI ; :: thesis: verum