Theorem tan4thpiOLD

Description: Obsolete version of tan4thpi as of 2-Sep-2025. (Contributed by Mario Carneiro, 5-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pire	⊢ π ∈ ℝ
2		4nn	⊢ 4 ∈ ℕ
3		nndivre	⊢ ( ( π ∈ ℝ ∧ 4 ∈ ℕ ) → ( π / 4 ) ∈ ℝ )
4	1 2 3	mp2an	⊢ ( π / 4 ) ∈ ℝ
5	4	recni	⊢ ( π / 4 ) ∈ ℂ
6		sincos4thpi	⊢ ( ( sin ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) ) ∧ ( cos ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) ) )
7	6	simpri	⊢ ( cos ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) )
8		sqrt2re	⊢ ( √ ‘ 2 ) ∈ ℝ
9	8	recni	⊢ ( √ ‘ 2 ) ∈ ℂ
10		2re	⊢ 2 ∈ ℝ
11		0le2	⊢ 0 ≤ 2
12		resqrtth	⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( ( √ ‘ 2 ) ↑ 2 ) = 2 )
13	10 11 12	mp2an	⊢ ( ( √ ‘ 2 ) ↑ 2 ) = 2
14		2ne0	⊢ 2 ≠ 0
15	13 14	eqnetri	⊢ ( ( √ ‘ 2 ) ↑ 2 ) ≠ 0
16		sqne0	⊢ ( ( √ ‘ 2 ) ∈ ℂ → ( ( ( √ ‘ 2 ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ 2 ) ≠ 0 ) )
17	9 16	ax-mp	⊢ ( ( ( √ ‘ 2 ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ 2 ) ≠ 0 )
18	15 17	mpbi	⊢ ( √ ‘ 2 ) ≠ 0
19		recne0	⊢ ( ( ( √ ‘ 2 ) ∈ ℂ ∧ ( √ ‘ 2 ) ≠ 0 ) → ( 1 / ( √ ‘ 2 ) ) ≠ 0 )
20	9 18 19	mp2an	⊢ ( 1 / ( √ ‘ 2 ) ) ≠ 0
21	7 20	eqnetri	⊢ ( cos ‘ ( π / 4 ) ) ≠ 0
22		tanval	⊢ ( ( ( π / 4 ) ∈ ℂ ∧ ( cos ‘ ( π / 4 ) ) ≠ 0 ) → ( tan ‘ ( π / 4 ) ) = ( ( sin ‘ ( π / 4 ) ) / ( cos ‘ ( π / 4 ) ) ) )
23	5 21 22	mp2an	⊢ ( tan ‘ ( π / 4 ) ) = ( ( sin ‘ ( π / 4 ) ) / ( cos ‘ ( π / 4 ) ) )
24	6	simpli	⊢ ( sin ‘ ( π / 4 ) ) = ( 1 / ( √ ‘ 2 ) )
25	24 7	oveq12i	⊢ ( ( sin ‘ ( π / 4 ) ) / ( cos ‘ ( π / 4 ) ) ) = ( ( 1 / ( √ ‘ 2 ) ) / ( 1 / ( √ ‘ 2 ) ) )
26	9 18	reccli	⊢ ( 1 / ( √ ‘ 2 ) ) ∈ ℂ
27	26 20	dividi	⊢ ( ( 1 / ( √ ‘ 2 ) ) / ( 1 / ( √ ‘ 2 ) ) ) = 1
28	23 25 27	3eqtri	⊢ ( tan ‘ ( π / 4 ) ) = 1