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 = π 4

Proof

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