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