Metamath Proof Explorer


Theorem pilem1

Description: Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion pilem1 A+sin-10A+sinA=0

Proof

Step Hyp Ref Expression
1 elin A+sin-10A+Asin-10
2 sinf sin:
3 ffn sin:sinFn
4 fniniseg sinFnAsin-10AsinA=0
5 2 3 4 mp2b Asin-10AsinA=0
6 rpcn A+A
7 6 biantrurd A+sinA=0AsinA=0
8 5 7 bitr4id A+Asin-10sinA=0
9 8 pm5.32i A+Asin-10A+sinA=0
10 1 9 bitri A+sin-10A+sinA=0