Step |
Hyp |
Ref |
Expression |
1 |
|
atandm3 |
|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) ) |
2 |
|
sqcl |
|- ( A e. CC -> ( A ^ 2 ) e. CC ) |
3 |
|
neg1cn |
|- -u 1 e. CC |
4 |
|
subeq0 |
|- ( ( ( A ^ 2 ) e. CC /\ -u 1 e. CC ) -> ( ( ( A ^ 2 ) - -u 1 ) = 0 <-> ( A ^ 2 ) = -u 1 ) ) |
5 |
2 3 4
|
sylancl |
|- ( A e. CC -> ( ( ( A ^ 2 ) - -u 1 ) = 0 <-> ( A ^ 2 ) = -u 1 ) ) |
6 |
|
ax-1cn |
|- 1 e. CC |
7 |
|
subneg |
|- ( ( ( A ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( A ^ 2 ) - -u 1 ) = ( ( A ^ 2 ) + 1 ) ) |
8 |
2 6 7
|
sylancl |
|- ( A e. CC -> ( ( A ^ 2 ) - -u 1 ) = ( ( A ^ 2 ) + 1 ) ) |
9 |
|
addcom |
|- ( ( ( A ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( A ^ 2 ) + 1 ) = ( 1 + ( A ^ 2 ) ) ) |
10 |
2 6 9
|
sylancl |
|- ( A e. CC -> ( ( A ^ 2 ) + 1 ) = ( 1 + ( A ^ 2 ) ) ) |
11 |
8 10
|
eqtrd |
|- ( A e. CC -> ( ( A ^ 2 ) - -u 1 ) = ( 1 + ( A ^ 2 ) ) ) |
12 |
11
|
eqeq1d |
|- ( A e. CC -> ( ( ( A ^ 2 ) - -u 1 ) = 0 <-> ( 1 + ( A ^ 2 ) ) = 0 ) ) |
13 |
5 12
|
bitr3d |
|- ( A e. CC -> ( ( A ^ 2 ) = -u 1 <-> ( 1 + ( A ^ 2 ) ) = 0 ) ) |
14 |
13
|
necon3bid |
|- ( A e. CC -> ( ( A ^ 2 ) =/= -u 1 <-> ( 1 + ( A ^ 2 ) ) =/= 0 ) ) |
15 |
14
|
pm5.32i |
|- ( ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) ) |
16 |
1 15
|
bitri |
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) ) |