Metamath Proof Explorer


Theorem cosatanne0

Description: The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion cosatanne0
|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) =/= 0 )

Proof

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 )