Step |
Hyp |
Ref |
Expression |
1 |
|
cosatan |
|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) = ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) ) |
2 |
|
ax-1cn |
|- 1 e. CC |
3 |
|
atandm4 |
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) ) |
4 |
3
|
simplbi |
|- ( A e. dom arctan -> A e. CC ) |
5 |
4
|
sqcld |
|- ( A e. dom arctan -> ( A ^ 2 ) e. CC ) |
6 |
|
addcl |
|- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 + ( A ^ 2 ) ) e. CC ) |
7 |
2 5 6
|
sylancr |
|- ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) e. CC ) |
8 |
7
|
sqrtcld |
|- ( A e. dom arctan -> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) e. CC ) |
9 |
7
|
sqsqrtd |
|- ( A e. dom arctan -> ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) = ( 1 + ( A ^ 2 ) ) ) |
10 |
3
|
simprbi |
|- ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) =/= 0 ) |
11 |
9 10
|
eqnetrd |
|- ( A e. dom arctan -> ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 ) |
12 |
|
sqne0 |
|- ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) e. CC -> ( ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) ) |
13 |
8 12
|
syl |
|- ( A e. dom arctan -> ( ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) ) |
14 |
11 13
|
mpbid |
|- ( A e. dom arctan -> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) |
15 |
8 14
|
recne0d |
|- ( A e. dom arctan -> ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) =/= 0 ) |
16 |
1 15
|
eqnetrd |
|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) =/= 0 ) |