Theorem taupilem3

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

	Ref	Expression
Assertion	taupilem3	|- ( A e. ( RR+ i^i ( `' cos " { 1 } ) ) <-> ( A e. RR+ /\ ( cos ` A ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( A e. ( RR+ i^i ( `' cos " { 1 } ) ) <-> ( A e. RR+ /\ A e. ( `' cos " { 1 } ) ) )
2		cosf	|- cos : CC --> CC
3		ffn	|- ( cos : CC --> CC -> cos Fn CC )
4		fniniseg	|- ( cos Fn CC -> ( A e. ( `' cos " { 1 } ) <-> ( A e. CC /\ ( cos ` A ) = 1 ) ) )
5	2 3 4	mp2b	|- ( A e. ( `' cos " { 1 } ) <-> ( A e. CC /\ ( cos ` A ) = 1 ) )
6		rpcn	|- ( A e. RR+ -> A e. CC )
7	6	biantrurd	|- ( A e. RR+ -> ( ( cos ` A ) = 1 <-> ( A e. CC /\ ( cos ` A ) = 1 ) ) )
8	5 7	bitr4id	|- ( A e. RR+ -> ( A e. ( `' cos " { 1 } ) <-> ( cos ` A ) = 1 ) )
9	8	pm5.32i	|- ( ( A e. RR+ /\ A e. ( `' cos " { 1 } ) ) <-> ( A e. RR+ /\ ( cos ` A ) = 1 ) )
10	1 9	bitri	|- ( A e. ( RR+ i^i ( `' cos " { 1 } ) ) <-> ( A e. RR+ /\ ( cos ` A ) = 1 ) )