Metamath Proof Explorer


Theorem bndatandm

Description: A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion bndatandm A A < 1 A dom arctan

Proof

Step Hyp Ref Expression
1 simpl A A < 1 A
2 sqcl A A 2
3 2 adantr A A < 1 A 2
4 3 abscld A A < 1 A 2
5 2nn0 2 0
6 absexp A 2 0 A 2 = A 2
7 1 5 6 sylancl A A < 1 A 2 = A 2
8 simpr A A < 1 A < 1
9 abscl A A
10 9 adantr A A < 1 A
11 1red A A < 1 1
12 absge0 A 0 A
13 12 adantr A A < 1 0 A
14 0le1 0 1
15 14 a1i A A < 1 0 1
16 10 11 13 15 lt2sqd A A < 1 A < 1 A 2 < 1 2
17 8 16 mpbid A A < 1 A 2 < 1 2
18 sq1 1 2 = 1
19 17 18 breqtrdi A A < 1 A 2 < 1
20 7 19 eqbrtrd A A < 1 A 2 < 1
21 4 20 ltned A A < 1 A 2 1
22 fveq2 A 2 = 1 A 2 = 1
23 ax-1cn 1
24 23 absnegi 1 = 1
25 abs1 1 = 1
26 24 25 eqtri 1 = 1
27 22 26 syl6eq A 2 = 1 A 2 = 1
28 27 necon3i A 2 1 A 2 1
29 21 28 syl A A < 1 A 2 1
30 atandm3 A dom arctan A A 2 1
31 1 29 30 sylanbrc A A < 1 A dom arctan