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

Metamath Proof Explorer

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