Metamath Proof Explorer

Theorem atan1

Description: The arctangent of 1 is _pi / 4 . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion atan1 
|- ( arctan ` 1 ) = ( _pi / 4 )

Proof

Step Hyp Ref Expression
1 tan4thpi 
 |-  ( tan ` ( _pi / 4 ) ) = 1
2 1 fveq2i 
 |-  ( arctan ` ( tan ` ( _pi / 4 ) ) ) = ( arctan ` 1 )
3 pire 
 |-  _pi e. RR
4 4nn 
 |-  4 e. NN
5 nndivre 
 |-  ( ( _pi e. RR /\ 4 e. NN ) -> ( _pi / 4 ) e. RR )
6 3 4 5 mp2an 
 |-  ( _pi / 4 ) e. RR
7 6 recni 
 |-  ( _pi / 4 ) e. CC
8 rere 
 |-  ( ( _pi / 4 ) e. RR -> ( Re ` ( _pi / 4 ) ) = ( _pi / 4 ) )
9 6 8 ax-mp 
 |-  ( Re ` ( _pi / 4 ) ) = ( _pi / 4 )
10 pirp 
 |-  _pi e. RR+
11 rphalfcl 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
12 10 11 ax-mp 
 |-  ( _pi / 2 ) e. RR+
13 rpgt0 
 |-  ( ( _pi / 2 ) e. RR+ -> 0 < ( _pi / 2 ) )
14 12 13 ax-mp 
 |-  0 < ( _pi / 2 )
15 halfpire 
 |-  ( _pi / 2 ) e. RR
16 lt0neg2 
 |-  ( ( _pi / 2 ) e. RR -> ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 ) )
17 15 16 ax-mp 
 |-  ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 )
18 14 17 mpbi 
 |-  -u ( _pi / 2 ) < 0
19 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
20 4 19 ax-mp 
 |-  4 e. RR+
21 rpdivcl 
 |-  ( ( _pi e. RR+ /\ 4 e. RR+ ) -> ( _pi / 4 ) e. RR+ )
22 10 20 21 mp2an 
 |-  ( _pi / 4 ) e. RR+
23 rpgt0 
 |-  ( ( _pi / 4 ) e. RR+ -> 0 < ( _pi / 4 ) )
24 22 23 ax-mp 
 |-  0 < ( _pi / 4 )
25 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
26 0re 
 |-  0 e. RR
27 25 26 6 lttri 
 |-  ( ( -u ( _pi / 2 ) < 0 /\ 0 < ( _pi / 4 ) ) -> -u ( _pi / 2 ) < ( _pi / 4 ) )
28 18 24 27 mp2an 
 |-  -u ( _pi / 2 ) < ( _pi / 4 )
29 3 recni 
 |-  _pi e. CC
30 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
31 divdiv1 
 |-  ( ( _pi e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( _pi / 2 ) / 2 ) = ( _pi / ( 2 x. 2 ) ) )
32 29 30 30 31 mp3an 
 |-  ( ( _pi / 2 ) / 2 ) = ( _pi / ( 2 x. 2 ) )
33 2t2e4 
 |-  ( 2 x. 2 ) = 4
34 33 oveq2i 
 |-  ( _pi / ( 2 x. 2 ) ) = ( _pi / 4 )
35 32 34 eqtri 
 |-  ( ( _pi / 2 ) / 2 ) = ( _pi / 4 )
36 rphalflt 
 |-  ( ( _pi / 2 ) e. RR+ -> ( ( _pi / 2 ) / 2 ) < ( _pi / 2 ) )
37 12 36 ax-mp 
 |-  ( ( _pi / 2 ) / 2 ) < ( _pi / 2 )
38 35 37 eqbrtrri 
 |-  ( _pi / 4 ) < ( _pi / 2 )
39 25 rexri 
 |-  -u ( _pi / 2 ) e. RR*
40 15 rexri 
 |-  ( _pi / 2 ) e. RR*
41 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( _pi / 4 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( _pi / 4 ) e. RR /\ -u ( _pi / 2 ) < ( _pi / 4 ) /\ ( _pi / 4 ) < ( _pi / 2 ) ) ) )
42 39 40 41 mp2an 
 |-  ( ( _pi / 4 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( _pi / 4 ) e. RR /\ -u ( _pi / 2 ) < ( _pi / 4 ) /\ ( _pi / 4 ) < ( _pi / 2 ) ) )
43 6 28 38 42 mpbir3an 
 |-  ( _pi / 4 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
44 9 43 eqeltri 
 |-  ( Re ` ( _pi / 4 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
45 atantan 
 |-  ( ( ( _pi / 4 ) e. CC /\ ( Re ` ( _pi / 4 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arctan ` ( tan ` ( _pi / 4 ) ) ) = ( _pi / 4 ) )
46 7 44 45 mp2an 
 |-  ( arctan ` ( tan ` ( _pi / 4 ) ) ) = ( _pi / 4 )
47 2 46 eqtr3i 
 |-  ( arctan ` 1 ) = ( _pi / 4 )