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 )