:: SIN_COS4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let th be real number ;
func tan th -> Real equals :: SIN_COS4:def 1
(sin th) / (cos th);
correctness
coherence
(sin th) / (cos th) is Real;
by XREAL_0:def 1;
end;

:: deftheorem defines tan SIN_COS4:def 1 :
for th being real number holds tan th = (sin th) / (cos th);

definition
let th be real number ;
func cot th -> Real equals :: SIN_COS4:def 2
(cos th) / (sin th);
correctness
coherence
(cos th) / (sin th) is Real;
by XREAL_0:def 1;
end;

:: deftheorem defines cot SIN_COS4:def 2 :
for th being real number holds cot th = (cos th) / (sin th);

definition
let th be real number ;
func cosec th -> Real equals :: SIN_COS4:def 3
1 / (sin th);
correctness
coherence
1 / (sin th) is Real;
by XREAL_0:def 1;
end;

:: deftheorem defines cosec SIN_COS4:def 3 :
for th being real number holds cosec th = 1 / (sin th);

definition
let th be real number ;
func sec th -> Real equals :: SIN_COS4:def 4
1 / (cos th);
correctness
coherence
1 / (cos th) is Real;
by XREAL_0:def 1;
end;

:: deftheorem defines sec SIN_COS4:def 4 :
for th being real number holds sec th = 1 / (cos th);

theorem :: SIN_COS4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number holds tan th = 1 / (cot th) by XCMPLX_1:57;

theorem :: SIN_COS4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number holds tan (- th) = - (tan th)
proof end;

theorem :: SIN_COS4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number holds cosec (- th) = - (1 / (sin th))
proof end;

theorem :: SIN_COS4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number holds cot (- th) = - (cot th)
proof end;

theorem :: SIN_COS4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1 being real number st cos th1 <> 0 holds
(cos th1) * (sec th1) = 1 by XCMPLX_1:107;

theorem Th6: :: SIN_COS4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number holds (sin th) * (sin th) = 1 - ((cos th) * (cos th))
proof end;

theorem Th7: :: SIN_COS4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number holds (cos th) * (cos th) = 1 - ((sin th) * (sin th))
proof end;

theorem Th8: :: SIN_COS4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number st cos th <> 0 holds
sin th = (cos th) * (tan th)
proof end;

Lm1: for th1, th2 being real number holds sin (th1 - th2) = ((sin th1) * (cos th2)) - ((cos th1) * (sin th2))
by COMPLEX2:4;

Lm2: for th1, th2 being real number holds cos (th1 - th2) = ((cos th1) * (cos th2)) + ((sin th1) * (sin th2))
by COMPLEX2:4;

theorem :: SIN_COS4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SIN_COS4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SIN_COS4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
tan (th1 + th2) = ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2)))
proof end;

theorem :: SIN_COS4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2)))
proof end;

theorem :: SIN_COS4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1))
proof end;

theorem :: SIN_COS4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
cot (th1 - th2) = (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1))
proof end;

theorem Th15: :: SIN_COS4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))
proof end;

theorem Th16: :: SIN_COS4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
cos ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
proof end;

theorem :: SIN_COS4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
proof end;

theorem :: SIN_COS4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number st sin th1 <> 0 & sin th2 <> 0 & sin th3 <> 0 holds
cot ((th1 + th2) + th3) = ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1)
proof end;

theorem Th19: :: SIN_COS4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin th1) + (sin th2) = 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))
proof end;

theorem Th20: :: SIN_COS4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin th1) - (sin th2) = 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))
proof end;

theorem Th21: :: SIN_COS4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos th1) + (cos th2) = 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))
proof end;

theorem Th22: :: SIN_COS4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos th1) - (cos th2) = - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))))
proof end;

theorem :: SIN_COS4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(tan th1) + (tan th2) = (sin (th1 + th2)) / ((cos th1) * (cos th2))
proof end;

theorem :: SIN_COS4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2))
proof end;

theorem :: SIN_COS4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & sin th2 <> 0 holds
(tan th1) + (cot th2) = (cos (th1 - th2)) / ((cos th1) * (sin th2))
proof end;

theorem :: SIN_COS4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & sin th2 <> 0 holds
(tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2)))
proof end;

theorem :: SIN_COS4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
(cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2))
proof end;

theorem :: SIN_COS4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
(cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2)))
proof end;

theorem :: SIN_COS4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin (th1 + th2)) + (sin (th1 - th2)) = 2 * ((sin th1) * (cos th2))
proof end;

theorem :: SIN_COS4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2))
proof end;

theorem :: SIN_COS4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos (th1 + th2)) + (cos (th1 - th2)) = 2 * ((cos th1) * (cos th2))
proof end;

theorem :: SIN_COS4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2)))
proof end;

theorem Th33: :: SIN_COS4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin th1) * (sin th2) = - ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2))))
proof end;

theorem Th34: :: SIN_COS4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin th1) * (cos th2) = (1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2)))
proof end;

theorem Th35: :: SIN_COS4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos th1) * (sin th2) = (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2)))
proof end;

theorem Th36: :: SIN_COS4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos th1) * (cos th2) = (1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2)))
proof end;

theorem :: SIN_COS4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number holds ((sin th1) * (sin th2)) * (sin th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) + (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) - (sin ((th1 + th2) + th3)))
proof end;

theorem :: SIN_COS4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number holds ((sin th1) * (sin th2)) * (cos th3) = (1 / 4) * ((((- (cos ((th1 + th2) - th3))) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) - (cos ((th1 + th2) + th3)))
proof end;

theorem :: SIN_COS4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number holds ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3)))
proof end;

theorem :: SIN_COS4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2, th3 being real number holds ((cos th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((cos ((th1 + th2) - th3)) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) + (cos ((th1 + th2) + th3)))
proof end;

theorem Th41: :: SIN_COS4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2))
proof end;

theorem :: SIN_COS4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin (th1 + th2)) * (sin (th1 - th2)) = ((cos th2) * (cos th2)) - ((cos th1) * (cos th1))
proof end;

theorem Th43: :: SIN_COS4:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (sin (th1 + th2)) * (cos (th1 - th2)) = ((sin th1) * (cos th1)) + ((sin th2) * (cos th2))
proof end;

theorem :: SIN_COS4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (cos th1)) - ((sin th2) * (cos th2))
proof end;

theorem Th45: :: SIN_COS4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2))
proof end;

theorem :: SIN_COS4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th2) * (cos th2)) - ((sin th1) * (sin th1))
proof end;

theorem :: SIN_COS4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2))
proof end;

theorem :: SIN_COS4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2)))
proof end;

theorem :: SIN_COS4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds ((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2))
proof end;

theorem :: SIN_COS4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos ((th1 - th2) / 2) <> 0 holds
((sin th1) + (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 + th2) / 2)
proof end;

theorem :: SIN_COS4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st cos ((th1 + th2) / 2) <> 0 holds
((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2)
proof end;

theorem :: SIN_COS4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st sin ((th1 + th2) / 2) <> 0 holds
((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 - th2) / 2)
proof end;

theorem :: SIN_COS4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number st sin ((th1 - th2) / 2) <> 0 holds
((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2)
proof end;

theorem :: SIN_COS4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th1, th2 being real number holds ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2))
proof end;