let x be real number ; :: thesis: ( cos x <> 0 implies (sec x) ^2 = 1 + ((tan x) ^2 ) )
assume cos x <> 0 ; :: thesis: (sec x) ^2 = 1 + ((tan x) ^2 )
then A1: (cos x) ^2 <> 0 by SQUARE_1:74;
(sec x) ^2 = (1 ^2 ) / ((cos x) ^2 ) by XCMPLX_1:77
.= (((sin x) ^2 ) + ((cos x) ^2 )) / ((cos x) ^2 ) by SIN_COS:32
.= (((sin x) ^2 ) / ((cos x) ^2 )) + (((cos x) ^2 ) / ((cos x) ^2 )) by XCMPLX_1:63
.= (((sin x) ^2 ) / ((cos x) ^2 )) + 1 by A1, XCMPLX_1:60
.= (((sin x) / (cos x)) ^2 ) + 1 by XCMPLX_1:77 ;
hence (sec x) ^2 = 1 + ((tan x) ^2 ) ; :: thesis: verum