PI in ].0,4.[ by SIN_COS:def 28;
then PI > 0 by XXREAL_1:4;
then A1: PI / 2 > 0 / 2 by XREAL_1:74;
0 - (PI / 2) < 0 by XREAL_1:49;
then arctan 0 = 0 by A1, Th35, Th41;
hence ( arctan 0 = 0 & arctan . 0 = 0 ) ; :: thesis: verum