Metamath Proof Explorer


Theorem taupilem3

Description: Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019)

Ref Expression
Assertion taupilem3 A + cos -1 1 A + cos A = 1

Proof

Step Hyp Ref Expression
1 elin A + cos -1 1 A + A cos -1 1
2 cosf cos :
3 ffn cos : cos Fn
4 fniniseg cos Fn A cos -1 1 A cos A = 1
5 2 3 4 mp2b A cos -1 1 A cos A = 1
6 rpcn A + A
7 6 biantrurd A + cos A = 1 A cos A = 1
8 5 7 bitr4id A + A cos -1 1 cos A = 1
9 8 pm5.32i A + A cos -1 1 A + cos A = 1
10 1 9 bitri A + cos -1 1 A + cos A = 1