This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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