let r be Real; :: 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:77
.= (3 / 2) * PI ; :: thesis: verum