Theorem tan4thpi

Description: The tangent of _pi / 4 . (Contributed by Mario Carneiro, 5-Apr-2015) (Proof shortened by SN, 2-Sep-2025)

	Ref	Expression
Assertion	tan4thpi	⊢ ( tan ‘ ( π / 4 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		4cn	⊢ 4 ∈ ℂ
3		4ne0	⊢ 4 ≠ 0
4	1 2 3	divcli	⊢ ( π / 4 ) ∈ ℂ
5		sincos4thpi	⊢ ( ( sin ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) ) ∧ ( cos ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) ) )
6	5	simpri	⊢ ( cos ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) )
7		sqrt2re	⊢ ( √ ‘ 2 ) ∈ ℝ
8	7	recni	⊢ ( √ ‘ 2 ) ∈ ℂ
9		2re	⊢ 2 ∈ ℝ
10		2pos	⊢ 0 < 2
11	9 10	sqrtgt0ii	⊢ 0 < ( √ ‘ 2 )
12	7 11	gt0ne0ii	⊢ ( √ ‘ 2 ) ≠ 0
13		recne0	⊢ ( ( ( √ ‘ 2 ) ∈ ℂ ∧ ( √ ‘ 2 ) ≠ 0 ) → ( 1 / ( √ ‘ 2 ) ) ≠ 0 )
14	8 12 13	mp2an	⊢ ( 1 / ( √ ‘ 2 ) ) ≠ 0
15	6 14	eqnetri	⊢ ( cos ‘ ( π / 4 ) ) ≠ 0
16		tanval	⊢ ( ( ( π / 4 ) ∈ ℂ ∧ ( cos ‘ ( π / 4 ) ) ≠ 0 ) → ( tan ‘ ( π / 4 ) ) = ( ( sin ‘ ( π / 4 ) ) / ( cos ‘ ( π / 4 ) ) ) )
17	4 15 16	mp2an	⊢ ( tan ‘ ( π / 4 ) ) = ( ( sin ‘ ( π / 4 ) ) / ( cos ‘ ( π / 4 ) ) )
18	5	simpli	⊢ ( sin ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) )
19	18 6	oveq12i	⊢ ( ( sin ‘ ( π / 4 ) ) / ( cos ‘ ( π / 4 ) ) ) = ( ( 1 / ( √ ‘ 2 ) ) / ( 1 / ( √ ‘ 2 ) ) )
20	8 12	reccli	⊢ ( 1 / ( √ ‘ 2 ) ) ∈ ℂ
21	20 14	dividi	⊢ ( ( 1 / ( √ ‘ 2 ) ) / ( 1 / ( √ ‘ 2 ) ) ) = 1
22	17 19 21	3eqtri	⊢ ( tan ‘ ( π / 4 ) ) = 1