Step |
Hyp |
Ref |
Expression |
1 |
|
recn |
|- ( A e. RR -> A e. CC ) |
2 |
|
neg1rr |
|- -u 1 e. RR |
3 |
2
|
a1i |
|- ( A e. RR -> -u 1 e. RR ) |
4 |
|
0red |
|- ( A e. RR -> 0 e. RR ) |
5 |
|
resqcl |
|- ( A e. RR -> ( A ^ 2 ) e. RR ) |
6 |
|
neg1lt0 |
|- -u 1 < 0 |
7 |
6
|
a1i |
|- ( A e. RR -> -u 1 < 0 ) |
8 |
|
sqge0 |
|- ( A e. RR -> 0 <_ ( A ^ 2 ) ) |
9 |
3 4 5 7 8
|
ltletrd |
|- ( A e. RR -> -u 1 < ( A ^ 2 ) ) |
10 |
3 9
|
gtned |
|- ( A e. RR -> ( A ^ 2 ) =/= -u 1 ) |
11 |
|
atandm3 |
|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) ) |
12 |
1 10 11
|
sylanbrc |
|- ( A e. RR -> A e. dom arctan ) |