trig
Case set df65d778fc5c
demo-eq-trig-01
Given
\(x \in \mathbb{C}\)
Claim
\(\displaystyle \left(\sin x\right)^{2} + \left(\cos x\right)^{2} = 1\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-eq-trig-01 (category trig) (var x complex) (ask (= (+ (pow (sin x) 2) (pow (cos x) 2)) 1)) (expect true))
demo-eq-trig-02
Given
\(x \in \mathbb{C}\)
Claim
\(\displaystyle 2 \, \sin x \, \cos x = \sin\left(2 \, x\right)\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-eq-trig-02 (category trig) (var x complex) (ask (= (* 2 (sin x) (cos x)) (sin (* 2 x)))) (expect true))
Case set 03f5149718d0
demo-eq-trig-01
Given
\(x \in \mathbb{C}\)
Claim
\(\displaystyle \left(\sin x\right)^{2} + \left(\cos x\right)^{2} = 1\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-eq-trig-01 (category trig) (var x complex) (ask (= (+ (pow (sin x) 2) (pow (cos x) 2)) 1)) (expect true))
demo-eq-trig-02
Given
\(x \in \mathbb{C}\)
Claim
\(\displaystyle 2 \, \sin x \, \cos x = \sin\left(2 \, x\right)\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-eq-trig-02 (category trig) (var x complex) (ask (= (* 2 (sin x) (cos x)) (sin (* 2 x)))) (expect true))
Case set d7af4def9aaa
demo-eq-trig-01
Given
\(x \in \mathbb{C}\)
Claim
\(\displaystyle \left(\sin x\right)^{2} + \left(\cos x\right)^{2} = 1\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-eq-trig-01 (category trig) (var x complex) (ask (= (+ (pow (sin x) 2) (pow (cos x) 2)) 1)) (expect true))
demo-eq-trig-02
Given
\(x \in \mathbb{C}\)
Claim
\(\displaystyle 2 \, \sin x \, \cos x = \sin\left(2 \, x\right)\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point