Theorem taupilem3

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

	Ref	Expression
Assertion	taupilem3	⊢ ( 𝐴 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝐴 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ 𝐴 ∈ ( ◡ cos “ { 1 } ) ) )
2		cosf	⊢ cos : ℂ ⟶ ℂ
3		ffn	⊢ ( cos : ℂ ⟶ ℂ → cos Fn ℂ )
4		fniniseg	⊢ ( cos Fn ℂ → ( 𝐴 ∈ ( ◡ cos “ { 1 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) = 1 ) ) )
5	2 3 4	mp2b	⊢ ( 𝐴 ∈ ( ◡ cos “ { 1 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) = 1 ) )
6		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
7	6	biantrurd	⊢ ( 𝐴 ∈ ℝ+ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) = 1 ) ) )
8	5 7	bitr4id	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ( ◡ cos “ { 1 } ) ↔ ( cos ‘ 𝐴 ) = 1 ) )
9	8	pm5.32i	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ∈ ( ◡ cos “ { 1 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) )
10	1 9	bitri	⊢ ( 𝐴 ∈ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) )