let x be Real; :: thesis: ( cos x <> 0 implies cosec x = (sec x) / (tan x) )

assume A1: cos x <> 0 ; :: thesis: cosec x = (sec x) / (tan x)

then (sec x) / (tan x) = ((1 / (cos x)) * (cos x)) / (((sin x) / (cos x)) * (cos x)) by XCMPLX_1:91

.= 1 / (((sin x) / (cos x)) * (cos x)) by A1, XCMPLX_1:87

.= 1 / (sin x) by A1, XCMPLX_1:87 ;

hence cosec x = (sec x) / (tan x) ; :: thesis: verum

assume A1: cos x <> 0 ; :: thesis: cosec x = (sec x) / (tan x)

then (sec x) / (tan x) = ((1 / (cos x)) * (cos x)) / (((sin x) / (cos x)) * (cos x)) by XCMPLX_1:91

.= 1 / (((sin x) / (cos x)) * (cos x)) by A1, XCMPLX_1:87

.= 1 / (sin x) by A1, XCMPLX_1:87 ;

hence cosec x = (sec x) / (tan x) ; :: thesis: verum