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 ` ( _pi / 4 ) ) = 1

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 4cn 
 |-  4 e. CC
3 4ne0 
 |-  4 =/= 0
4 1 2 3 divcli 
 |-  ( _pi / 4 ) e. CC
5 sincos4thpi 
 |-  ( ( sin ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) ) /\ ( cos ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) ) )
6 5 simpri 
 |-  ( cos ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) )
7 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
8 7 recni 
 |-  ( sqrt ` 2 ) e. CC
9 2re 
 |-  2 e. RR
10 2pos 
 |-  0 < 2
11 9 10 sqrtgt0ii 
 |-  0 < ( sqrt ` 2 )
12 7 11 gt0ne0ii 
 |-  ( sqrt ` 2 ) =/= 0
13 recne0 
 |-  ( ( ( sqrt ` 2 ) e. CC /\ ( sqrt ` 2 ) =/= 0 ) -> ( 1 / ( sqrt ` 2 ) ) =/= 0 )
14 8 12 13 mp2an 
 |-  ( 1 / ( sqrt ` 2 ) ) =/= 0
15 6 14 eqnetri 
 |-  ( cos ` ( _pi / 4 ) ) =/= 0
16 tanval 
 |-  ( ( ( _pi / 4 ) e. CC /\ ( cos ` ( _pi / 4 ) ) =/= 0 ) -> ( tan ` ( _pi / 4 ) ) = ( ( sin ` ( _pi / 4 ) ) / ( cos ` ( _pi / 4 ) ) ) )
17 4 15 16 mp2an 
 |-  ( tan ` ( _pi / 4 ) ) = ( ( sin ` ( _pi / 4 ) ) / ( cos ` ( _pi / 4 ) ) )
18 5 simpli 
 |-  ( sin ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) )
19 18 6 oveq12i 
 |-  ( ( sin ` ( _pi / 4 ) ) / ( cos ` ( _pi / 4 ) ) ) = ( ( 1 / ( sqrt ` 2 ) ) / ( 1 / ( sqrt ` 2 ) ) )
20 8 12 reccli 
 |-  ( 1 / ( sqrt ` 2 ) ) e. CC
21 20 14 dividi 
 |-  ( ( 1 / ( sqrt ` 2 ) ) / ( 1 / ( sqrt ` 2 ) ) ) = 1
22 17 19 21 3eqtri 
 |-  ( tan ` ( _pi / 4 ) ) = 1