Metamath Proof Explorer

Theorem tan4thpi

Description: The tangent of _pi / 4 . (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion tan4thpi 
|- ( tan ` ( _pi / 4 ) ) = 1

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 4nn 
 |-  4 e. NN
3 nndivre 
 |-  ( ( _pi e. RR /\ 4 e. NN ) -> ( _pi / 4 ) e. RR )
4 1 2 3 mp2an 
 |-  ( _pi / 4 ) e. RR
5 4 recni 
 |-  ( _pi / 4 ) e. CC
6 sincos4thpi 
 |-  ( ( sin ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) ) /\ ( cos ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) ) )
7 6 simpri 
 |-  ( cos ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) )
8 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
9 8 recni 
 |-  ( sqrt ` 2 ) e. CC
10 2re 
 |-  2 e. RR
11 0le2 
 |-  0 <_ 2
12 resqrtth 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( ( sqrt ` 2 ) ^ 2 ) = 2 )
13 10 11 12 mp2an 
 |-  ( ( sqrt ` 2 ) ^ 2 ) = 2
14 2ne0 
 |-  2 =/= 0
15 13 14 eqnetri 
 |-  ( ( sqrt ` 2 ) ^ 2 ) =/= 0
16 sqne0 
 |-  ( ( sqrt ` 2 ) e. CC -> ( ( ( sqrt ` 2 ) ^ 2 ) =/= 0 <-> ( sqrt ` 2 ) =/= 0 ) )
17 9 16 ax-mp 
 |-  ( ( ( sqrt ` 2 ) ^ 2 ) =/= 0 <-> ( sqrt ` 2 ) =/= 0 )
18 15 17 mpbi 
 |-  ( sqrt ` 2 ) =/= 0
19 recne0 
 |-  ( ( ( sqrt ` 2 ) e. CC /\ ( sqrt ` 2 ) =/= 0 ) -> ( 1 / ( sqrt ` 2 ) ) =/= 0 )
20 9 18 19 mp2an 
 |-  ( 1 / ( sqrt ` 2 ) ) =/= 0
21 7 20 eqnetri 
 |-  ( cos ` ( _pi / 4 ) ) =/= 0
22 tanval 
 |-  ( ( ( _pi / 4 ) e. CC /\ ( cos ` ( _pi / 4 ) ) =/= 0 ) -> ( tan ` ( _pi / 4 ) ) = ( ( sin ` ( _pi / 4 ) ) / ( cos ` ( _pi / 4 ) ) ) )
23 5 21 22 mp2an 
 |-  ( tan ` ( _pi / 4 ) ) = ( ( sin ` ( _pi / 4 ) ) / ( cos ` ( _pi / 4 ) ) )
24 6 simpli 
 |-  ( sin ` ( _pi / 4 ) ) = ( 1 / ( sqrt ` 2 ) )
25 24 7 oveq12i 
 |-  ( ( sin ` ( _pi / 4 ) ) / ( cos ` ( _pi / 4 ) ) ) = ( ( 1 / ( sqrt ` 2 ) ) / ( 1 / ( sqrt ` 2 ) ) )
26 9 18 reccli 
 |-  ( 1 / ( sqrt ` 2 ) ) e. CC
27 26 20 dividi 
 |-  ( ( 1 / ( sqrt ` 2 ) ) / ( 1 / ( sqrt ` 2 ) ) ) = 1
28 23 25 27 3eqtri 
 |-  ( tan ` ( _pi / 4 ) ) = 1